%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CSR014+1 : TPTP v8.2.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n005.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 : Mon Jun 24 04:59:51 EDT 2024
% Result : Theorem 77.94s 78.00s
% Output : CNFRefutation 78.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : CSR014+1 : TPTP v8.2.0. Bugfixed v3.1.0.
% 0.13/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n005.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Jun 19 19:34:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.53/0.62 start to proof:theBenchmark
% 77.92/77.98 %-------------------------------------------
% 77.92/77.98 % File :CSE---1.7
% 77.92/77.98 % Problem :theBenchmark
% 77.92/77.98 % Transform :cnf
% 77.92/77.98 % Format :tptp:raw
% 77.92/77.98 % Command :java -jar mcs_scs.jar %d %s
% 77.92/77.98
% 77.92/77.98 % Result :Theorem 77.250000s
% 77.92/77.98 % Output :CNFRefutation 77.250000s
% 77.92/77.98 %-------------------------------------------
% 77.92/77.99 %--------------------------------------------------------------------------
% 77.92/77.99 % File : CSR014+1 : TPTP v8.2.0. Bugfixed v3.1.0.
% 77.92/77.99 % Domain : Commonsense Reasoning
% 77.92/77.99 % Problem : Filling is not released at time 3
% 77.92/77.99 % Version : [Mue04] axioms : Especial.
% 77.92/77.99 % English :
% 77.92/77.99
% 77.92/77.99 % Refs : [MS05] Mueller & Sutcliffe (2005), Reasoning in the Event Cal
% 77.92/77.99 % : [Mue04] Mueller (2004), A Tool for Satisfiability-based Common
% 77.92/77.99 % : [MS02] Miller & Shanahan (2002), Some Alternative Formulation
% 77.92/77.99 % Source : [MS05]
% 77.92/77.99 % Names :
% 77.92/77.99
% 77.92/77.99 % Status : Theorem
% 77.92/77.99 % Rating : 0.33 v8.2.0, 0.31 v7.5.0, 0.34 v7.4.0, 0.23 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.22 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.29 v6.2.0, 0.32 v6.1.0, 0.33 v6.0.0, 0.26 v5.5.0, 0.37 v5.4.0, 0.39 v5.3.0, 0.41 v5.2.0, 0.30 v5.1.0, 0.33 v5.0.0, 0.38 v4.1.0, 0.39 v4.0.0, 0.42 v3.7.0, 0.40 v3.5.0, 0.37 v3.3.0, 0.29 v3.2.0, 0.36 v3.1.0
% 77.92/77.99 % Syntax : Number of formulae : 55 ( 25 unt; 0 def)
% 77.92/77.99 % Number of atoms : 136 ( 40 equ)
% 77.92/77.99 % Maximal formula atoms : 11 ( 2 avg)
% 77.92/77.99 % Number of connectives : 110 ( 29 ~; 8 |; 43 &)
% 77.92/77.99 % ( 18 <=>; 12 =>; 0 <=; 0 <~>)
% 77.92/77.99 % Maximal formula depth : 12 ( 4 avg)
% 77.92/77.99 % Maximal term depth : 2 ( 1 avg)
% 77.92/77.99 % Number of predicates : 13 ( 12 usr; 0 prp; 2-4 aty)
% 77.92/77.99 % Number of functors : 17 ( 17 usr; 15 con; 0-2 aty)
% 77.92/77.99 % Number of variables : 86 ( 74 !; 12 ?)
% 77.92/77.99 % SPC : FOF_THM_RFO_SEQ
% 77.92/77.99
% 77.92/77.99 % Comments :
% 77.92/77.99 %--------------------------------------------------------------------------
% 77.92/77.99 %----Include standard discrete event calculus axioms
% 77.92/77.99 include('Axioms/CSR001+0.ax').
% 77.92/77.99 %----Include kitchen sink scenario axioms
% 77.92/77.99 include('Axioms/CSR001+1.ax').
% 77.92/77.99 %--------------------------------------------------------------------------
% 77.92/77.99 fof(plus0_0,axiom,
% 77.92/77.99 plus(n0,n0) = n0 ).
% 77.92/77.99
% 77.92/77.99 fof(plus0_1,axiom,
% 77.92/77.99 plus(n0,n1) = n1 ).
% 77.92/77.99
% 77.92/77.99 fof(plus0_2,axiom,
% 77.92/77.99 plus(n0,n2) = n2 ).
% 77.92/77.99
% 77.92/77.99 fof(plus0_3,axiom,
% 77.92/77.99 plus(n0,n3) = n3 ).
% 77.92/77.99
% 77.92/77.99 fof(plus1_1,axiom,
% 77.92/77.99 plus(n1,n1) = n2 ).
% 77.92/77.99
% 77.92/77.99 fof(plus1_2,axiom,
% 77.92/77.99 plus(n1,n2) = n3 ).
% 77.92/77.99
% 77.92/77.99 fof(plus1_3,axiom,
% 77.92/77.99 plus(n1,n3) = n4 ).
% 77.92/77.99
% 77.92/77.99 fof(plus2_2,axiom,
% 77.92/77.99 plus(n2,n2) = n4 ).
% 77.92/77.99
% 77.92/77.99 fof(plus2_3,axiom,
% 77.92/77.99 plus(n2,n3) = n5 ).
% 77.92/77.99
% 77.92/77.99 fof(plus3_3,axiom,
% 77.92/77.99 plus(n3,n3) = n6 ).
% 77.92/77.99
% 77.92/77.99 fof(symmetry_of_plus,axiom,
% 77.92/77.99 ! [X,Y] : plus(X,Y) = plus(Y,X) ).
% 77.92/77.99
% 77.92/77.99 fof(less_or_equal,axiom,
% 77.92/77.99 ! [X,Y] :
% 77.92/77.99 ( less_or_equal(X,Y)
% 77.92/77.99 <=> ( less(X,Y)
% 77.92/77.99 | X = Y ) ) ).
% 77.92/77.99
% 77.92/77.99 fof(less0,axiom,
% 77.92/77.99 ~ ? [X] : less(X,n0) ).
% 77.92/77.99
% 77.92/77.99 fof(less1,axiom,
% 77.92/77.99 ! [X] :
% 77.92/77.99 ( less(X,n1)
% 77.92/77.99 <=> less_or_equal(X,n0) ) ).
% 77.92/77.99
% 77.92/77.99 fof(less2,axiom,
% 77.92/77.99 ! [X] :
% 77.92/77.99 ( less(X,n2)
% 77.92/77.99 <=> less_or_equal(X,n1) ) ).
% 77.92/77.99
% 77.92/77.99 fof(less3,axiom,
% 77.92/77.99 ! [X] :
% 77.94/78.00 ( less(X,n3)
% 77.94/78.00 <=> less_or_equal(X,n2) ) ).
% 77.94/78.00
% 77.94/78.00 fof(less4,axiom,
% 77.94/78.00 ! [X] :
% 77.94/78.00 ( less(X,n4)
% 77.94/78.00 <=> less_or_equal(X,n3) ) ).
% 77.94/78.00
% 77.94/78.00 fof(less5,axiom,
% 77.94/78.00 ! [X] :
% 77.94/78.00 ( less(X,n5)
% 77.94/78.00 <=> less_or_equal(X,n4) ) ).
% 77.94/78.00
% 77.94/78.00 fof(less6,axiom,
% 77.94/78.00 ! [X] :
% 77.94/78.00 ( less(X,n6)
% 77.94/78.00 <=> less_or_equal(X,n5) ) ).
% 77.94/78.00
% 77.94/78.00 fof(less7,axiom,
% 77.94/78.00 ! [X] :
% 77.94/78.00 ( less(X,n7)
% 77.94/78.00 <=> less_or_equal(X,n6) ) ).
% 77.94/78.00
% 77.94/78.00 fof(less8,axiom,
% 77.94/78.00 ! [X] :
% 77.94/78.00 ( less(X,n8)
% 77.94/78.00 <=> less_or_equal(X,n7) ) ).
% 77.94/78.00
% 77.94/78.00 fof(less9,axiom,
% 77.94/78.00 ! [X] :
% 77.94/78.00 ( less(X,n9)
% 77.94/78.00 <=> less_or_equal(X,n8) ) ).
% 77.94/78.00
% 77.94/78.00 fof(less_property,axiom,
% 77.94/78.00 ! [X,Y] :
% 77.94/78.00 ( less(X,Y)
% 77.94/78.00 <=> ( ~ less(Y,X)
% 77.94/78.00 & Y != X ) ) ).
% 77.94/78.00
% 77.94/78.00 %----Initial conditions
% 77.94/78.00 fof(waterLevel_0,hypothesis,
% 77.94/78.00 holdsAt(waterLevel(n0),n0) ).
% 77.94/78.00
% 77.94/78.00 fof(not_filling_0,hypothesis,
% 77.94/78.00 ~ holdsAt(filling,n0) ).
% 77.94/78.00
% 77.94/78.00 fof(not_spilling_0,hypothesis,
% 77.94/78.00 ~ holdsAt(spilling,n0) ).
% 77.94/78.00
% 77.94/78.00 fof(not_released_waterLevel_0,hypothesis,
% 77.94/78.00 ! [Height] : ~ releasedAt(waterLevel(Height),n0) ).
% 77.94/78.00
% 77.94/78.00 fof(not_released_filling_0,hypothesis,
% 77.94/78.00 ~ releasedAt(filling,n0) ).
% 77.94/78.00
% 77.94/78.00 fof(not_released_spilling_0,hypothesis,
% 77.94/78.00 ~ releasedAt(spilling,n0) ).
% 77.94/78.00
% 77.94/78.00 fof(filling_3_l1,conjecture,
% 77.94/78.00 ~ releasedAt(filling,n3) ).
% 77.94/78.00
% 77.94/78.00 %--------------------------------------------------------------------------
% 77.94/78.00 %-------------------------------------------
% 77.94/78.00 % Proof found
% 77.94/78.00 % SZS status Theorem for theBenchmark
% 77.94/78.00 % SZS output start Proof
% 77.94/78.00 %ClaNum:206(EqnAxiom:70)
% 77.94/78.00 %VarNum:619(SingletonVarNum:232)
% 77.94/78.00 %MaxLitNum:6
% 77.94/78.00 %MaxfuncDepth:2
% 77.94/78.00 %SharedTerms:47
% 77.94/78.00 %goalClause: 81
% 77.94/78.00 %singleGoalClaCount:1
% 77.94/78.00 [81]P1(a2,a16)
% 77.94/78.00 [84]~E(a21,a26)
% 77.94/78.00 [85]~E(a27,a2)
% 77.94/78.00 [86]~E(a28,a26)
% 77.94/78.00 [87]~E(a28,a21)
% 77.94/78.00 [90]~P2(a2,a1)
% 77.94/78.00 [91]~P2(a27,a1)
% 77.94/78.00 [92]~P1(a2,a1)
% 77.94/78.00 [93]~P1(a27,a1)
% 77.94/78.00 [71]E(f14(a1,a1),a1)
% 77.94/78.00 [72]E(f14(a1,a15),a15)
% 77.94/78.00 [73]E(f14(a1,a16),a16)
% 77.94/78.00 [74]E(f14(a1,a17),a17)
% 77.94/78.00 [75]E(f14(a15,a15),a17)
% 77.94/78.00 [76]E(f14(a15,a16),a18)
% 77.94/78.00 [77]E(f14(a15,a17),a16)
% 77.94/78.00 [78]E(f14(a16,a16),a19)
% 77.94/78.00 [79]E(f14(a17,a16),a20)
% 77.94/78.00 [80]E(f14(a17,a17),a18)
% 77.94/78.00 [82]P2(f25(a1),a1)
% 77.94/78.00 [94]~P6(x941,a1)
% 77.94/78.00 [88]~E(f25(x881),a2)
% 77.94/78.00 [89]~E(f25(x891),a27)
% 77.94/78.00 [95]~P1(f25(x951),a1)
% 77.94/78.00 [83]E(f14(x831,x832),f14(x832,x831))
% 77.94/78.00 [103]~P8(x1031,a1)+P6(x1031,a15)
% 77.94/78.00 [104]~P8(x1041,a17)+P6(x1041,a16)
% 77.94/78.00 [105]~P8(x1051,a15)+P6(x1051,a17)
% 77.94/78.00 [106]~P8(x1061,a16)+P6(x1061,a18)
% 77.94/78.00 [107]~P8(x1071,a18)+P6(x1071,a20)
% 77.94/78.00 [108]~P8(x1081,a20)+P6(x1081,a19)
% 77.94/78.00 [109]~P8(x1091,a19)+P6(x1091,a22)
% 77.94/78.00 [110]~P8(x1101,a22)+P6(x1101,a23)
% 77.94/78.00 [111]~P8(x1111,a23)+P6(x1111,a24)
% 77.94/78.00 [112]~P6(x1121,a15)+P8(x1121,a1)
% 77.94/78.00 [113]~P6(x1131,a17)+P8(x1131,a15)
% 77.94/78.00 [114]~P6(x1141,a18)+P8(x1141,a16)
% 77.94/78.00 [115]~P6(x1151,a16)+P8(x1151,a17)
% 77.94/78.00 [116]~P6(x1161,a20)+P8(x1161,a18)
% 77.94/78.00 [117]~P6(x1171,a19)+P8(x1171,a20)
% 77.94/78.00 [118]~P6(x1181,a22)+P8(x1181,a19)
% 77.94/78.00 [119]~P6(x1191,a23)+P8(x1191,a22)
% 77.94/78.00 [120]~P6(x1201,a24)+P8(x1201,a23)
% 77.94/78.00 [97]~E(x971,x972)+P8(x971,x972)
% 77.94/78.00 [101]~P6(x1012,x1011)+~E(x1011,x1012)
% 77.94/78.00 [121]~P6(x1211,x1212)+P8(x1211,x1212)
% 77.94/78.00 [127]~P6(x1272,x1271)+~P6(x1271,x1272)
% 77.94/78.00 [96]E(x961,x962)+~E(f25(x961),f25(x962))
% 77.94/78.00 [135]~P10(x1351,x1352,x1353)+E(x1351,a26)
% 77.94/78.00 [136]~P9(x1362,x1361,x1363)+E(x1361,a2)
% 77.94/78.00 [150]~P4(x1502,x1501,x1503)+P7(x1501,x1502,x1503)
% 77.94/78.00 [151]~P7(x1512,x1511,x1513)+P4(x1511,x1512,x1513)
% 77.94/78.00 [169]~P11(x1691,x1692,x1693)+P6(x1691,f7(x1691,x1692,x1693))
% 77.94/78.00 [170]~P12(x1701,x1703,x1702)+P6(x1701,f9(x1701,x1702,x1703))
% 77.94/78.00 [171]~P11(x1711,x1712,x1713)+P6(f7(x1711,x1712,x1713),x1713)
% 77.94/78.00 [172]~P12(x1721,x1723,x1722)+P6(f9(x1721,x1722,x1723),x1722)
% 77.94/78.00 [181]~P11(x1811,x1812,x1813)+P3(f8(x1811,x1812,x1813),f7(x1811,x1812,x1813))
% 77.94/78.00 [182]~P12(x1821,x1823,x1822)+P3(f10(x1821,x1822,x1823),f9(x1821,x1822,x1823))
% 77.94/78.00 [191]~P11(x1911,x1912,x1913)+P9(f8(x1911,x1912,x1913),x1912,f7(x1911,x1912,x1913))
% 77.94/78.00 [192]~P12(x1921,x1923,x1922)+P7(f10(x1921,x1922,x1923),x1923,f9(x1921,x1922,x1923))
% 77.94/78.00 [148]~P10(x1481,x1482,x1483)+E(f25(f13(x1481,x1482)),x1482)
% 77.94/78.00 [98]P3(x981,x982)+~E(x982,a1)+~E(x981,a26)
% 77.94/78.00 [99]~P3(x992,x991)+E(x991,a1)+E(x992,a21)
% 77.94/78.00 [100]~P3(x1001,x1002)+E(x1001,a21)+E(x1001,a26)
% 77.94/78.00 [102]P6(x1022,x1021)+P6(x1021,x1022)+E(x1021,x1022)
% 77.94/78.00 [122]~P3(x1221,x1222)+E(x1221,a26)+P2(a2,x1222)
% 77.94/78.00 [123]~P3(x1232,x1231)+P2(a2,x1231)+E(x1231,a1)
% 77.94/78.00 [124]P6(x1241,x1242)+~P8(x1241,x1242)+E(x1241,x1242)
% 77.94/78.00 [125]~P3(x1251,x1252)+E(x1251,a26)+P2(f25(a16),x1252)
% 77.94/78.00 [126]~P3(x1262,x1261)+E(x1261,a1)+P2(f25(a16),x1261)
% 77.94/78.00 [146]~P1(x1461,x1462)+P3(f3(x1461,x1462),x1462)+P1(x1461,f14(x1462,a15))
% 77.94/78.00 [147]P1(x1471,x1472)+P3(f12(x1471,x1472),x1472)+~P1(x1471,f14(x1472,a15))
% 77.94/78.00 [155]P1(x1551,x1552)+P10(f12(x1551,x1552),x1551,x1552)+~P1(x1551,f14(x1552,a15))
% 77.94/78.00 [128]P9(x1281,x1282,x1283)+~E(x1282,a2)+~E(x1281,a21)
% 77.94/78.00 [129]P9(x1291,x1292,x1293)+~E(x1292,a2)+~E(x1291,a28)
% 77.94/78.01 [130]P4(x1301,x1302,x1303)+~E(x1301,a2)+~E(x1302,a26)
% 77.94/78.01 [131]P4(x1311,x1312,x1313)+~E(x1311,a27)+~E(x1312,a21)
% 77.94/78.01 [139]~P9(x1391,x1392,x1393)+E(x1391,a28)+E(x1391,a21)
% 77.94/78.01 [134]E(x1341,x1342)+~P2(f25(x1341),x1343)+~P2(f25(x1342),x1343)
% 77.94/78.01 [152]~P7(x1523,x1521,x1522)+~P3(x1523,x1522)+P2(x1521,f14(x1522,a15))
% 77.94/78.01 [153]~P10(x1533,x1531,x1532)+~P3(x1533,x1532)+P1(x1531,f14(x1532,a15))
% 77.94/78.01 [156]~P3(x1561,x1562)+~P9(x1561,x1563,x1562)+~P1(x1563,f14(x1562,a15))
% 77.94/78.01 [157]~P3(x1571,x1572)+~P7(x1571,x1573,x1572)+~P1(x1573,f14(x1572,a15))
% 77.94/78.01 [158]~P3(x1581,x1582)+~P9(x1581,x1583,x1582)+~P2(x1583,f14(x1582,a15))
% 77.94/78.01 [133]P10(x1331,x1332,x1333)+~E(x1331,a26)+~E(x1332,f25(x1334))
% 77.94/78.01 [176]~P2(f25(x1764),x1761)+P13(a2,x1761,f25(x1762),x1763)+~E(x1762,f14(x1764,x1763))
% 77.94/78.01 [132]P3(x1321,x1322)+~E(x1321,a21)+~P2(a2,x1322)+~P2(f25(a16),x1322)
% 77.94/78.01 [149]~P2(x1491,x1492)+P3(f4(x1491,x1492),x1492)+P1(x1491,f14(x1492,a15))+P2(x1491,f14(x1492,a15))
% 77.94/78.01 [154]P2(x1541,x1542)+P3(f11(x1541,x1542),x1542)+~P2(x1541,f14(x1542,a15))+P1(x1541,f14(x1542,a15))
% 77.94/78.01 [159]~P2(x1591,x1592)+P9(f4(x1591,x1592),x1591,x1592)+P1(x1591,f14(x1592,a15))+P2(x1591,f14(x1592,a15))
% 77.94/78.01 [160]P2(x1601,x1602)+P7(f11(x1601,x1602),x1601,x1602)+~P2(x1601,f14(x1602,a15))+P1(x1601,f14(x1602,a15))
% 77.94/78.01 [175]~P1(x1751,x1752)+P9(f3(x1751,x1752),x1751,x1752)+P7(f3(x1751,x1752),x1751,x1752)+P1(x1751,f14(x1752,a15))
% 77.94/78.01 [140]~P4(x1401,x1402,x1403)+E(x1402,a28)+E(x1401,a2)+E(x1402,a21)
% 77.94/78.01 [141]~P4(x1412,x1411,x1413)+E(x1411,a21)+E(x1411,a28)+E(x1411,a26)
% 77.94/78.01 [161]~P4(x1611,x1612,x1613)+E(x1611,a2)+E(x1612,a21)+E(f25(f5(x1613,x1612,x1611)),x1611)
% 77.94/78.01 [162]~P4(x1623,x1621,x1622)+E(x1621,a21)+E(x1621,a26)+E(f25(f5(x1622,x1621,x1623)),x1623)
% 77.94/78.01 [183]~P4(x1831,x1832,x1833)+E(x1831,a2)+E(x1832,a21)+P2(f25(f5(x1833,x1832,x1831)),x1833)
% 77.94/78.01 [184]~P4(x1843,x1841,x1842)+E(x1841,a21)+E(x1841,a26)+P2(f25(f5(x1842,x1841,x1843)),x1842)
% 77.94/78.01 [144]P4(x1441,x1442,x1443)+~E(x1442,a21)+~E(x1441,f25(x1444))+~P2(f25(x1444),x1443)
% 77.94/78.01 [145]P4(x1451,x1452,x1453)+~E(x1452,a28)+~E(x1451,f25(x1454))+~P2(f25(x1454),x1453)
% 77.94/78.01 [164]~P4(x1642,x1641,x1643)+E(x1641,a28)+E(x1641,a26)+E(x1642,a27)+E(f25(f6(x1643,x1641,x1642)),x1642)
% 77.94/78.01 [166]~P4(x1662,x1661,x1663)+E(x1662,a27)+E(x1661,a28)+E(x1662,a2)+E(f25(f6(x1663,x1661,x1662)),x1662)
% 77.94/78.01 [178]~P4(x1782,x1781,x1783)+E(x1781,a26)+E(x1782,a27)+E(f25(f6(x1783,x1781,x1782)),x1782)+E(f25(f5(x1783,x1781,x1782)),x1782)
% 77.94/78.01 [180]~P4(x1801,x1803,x1802)+E(x1801,a27)+E(x1801,a2)+E(f25(f6(x1802,x1803,x1801)),x1801)+E(f25(f5(x1802,x1803,x1801)),x1801)
% 77.94/78.01 [185]~P4(x1851,x1852,x1853)+E(x1851,a27)+E(x1851,a2)+E(x1852,a28)+P2(f25(f6(x1853,x1852,x1851)),x1853)
% 77.94/78.01 [188]~P4(x1881,x1882,x1883)+E(x1882,a28)+E(x1881,a27)+E(x1882,a26)+P2(f25(f6(x1883,x1882,x1881)),x1883)
% 77.94/78.01 [194]~P4(x1942,x1941,x1943)+E(x1941,a26)+E(x1942,a27)+P2(f25(f5(x1943,x1941,x1942)),x1943)+E(f25(f6(x1943,x1941,x1942)),x1942)
% 77.94/78.01 [195]~P4(x1951,x1953,x1952)+E(x1951,a27)+E(x1951,a2)+P2(f25(f6(x1952,x1953,x1951)),x1952)+E(f25(f5(x1952,x1953,x1951)),x1951)
% 77.94/78.01 [198]~P4(x1981,x1982,x1983)+E(x1981,a27)+E(x1982,a26)+P2(f25(f6(x1983,x1982,x1981)),x1983)+E(f25(f5(x1983,x1982,x1981)),x1981)
% 77.94/78.01 [200]~P4(x2001,x2003,x2002)+E(x2001,a27)+E(x2001,a2)+P2(f25(f5(x2002,x2003,x2001)),x2002)+E(f25(f6(x2002,x2003,x2001)),x2001)
% 77.94/78.01 [201]~P4(x2011,x2013,x2012)+E(x2011,a27)+E(x2011,a2)+P2(f25(f6(x2012,x2013,x2011)),x2012)+P2(f25(f5(x2012,x2013,x2011)),x2012)
% 77.94/78.01 [203]~P4(x2031,x2032,x2033)+E(x2031,a27)+E(x2032,a26)+P2(f25(f6(x2033,x2032,x2031)),x2033)+P2(f25(f5(x2033,x2032,x2031)),x2033)
% 77.94/78.01 [173]~P6(x1731,x1735)+~P6(x1735,x1733)+~P9(x1734,x1732,x1735)+P11(x1731,x1732,x1733)+~P3(x1734,x1735)
% 77.94/78.01 [174]~P6(x1741,x1745)+~P6(x1745,x1743)+~P7(x1744,x1742,x1745)+P12(x1741,x1742,x1743)+~P3(x1744,x1745)
% 77.94/78.01 [205]~P7(x2055,x2054,x2052)+~P13(x2054,x2052,x2051,x2053)+~P3(x2055,x2052)+P11(x2052,x2054,f14(x2052,x2053))+~P6(a1,x2053)+P2(x2051,f14(x2052,x2053))
% 77.94/78.01 [206]~P9(x2065,x2064,x2062)+~P5(x2064,x2062,x2061,x2063)+~P3(x2065,x2062)+P12(x2062,x2064,f14(x2062,x2063))+~P6(a1,x2063)+P2(x2061,f14(x2062,x2063))
% 77.94/78.01 %EqnAxiom
% 77.94/78.01 [1]E(x11,x11)
% 77.94/78.01 [2]E(x22,x21)+~E(x21,x22)
% 77.94/78.01 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 77.94/78.01 [4]~E(x41,x42)+E(f14(x41,x43),f14(x42,x43))
% 77.94/78.01 [5]~E(x51,x52)+E(f14(x53,x51),f14(x53,x52))
% 77.94/78.01 [6]~E(x61,x62)+E(f25(x61),f25(x62))
% 77.94/78.01 [7]~E(x71,x72)+E(f6(x71,x73,x74),f6(x72,x73,x74))
% 77.94/78.01 [8]~E(x81,x82)+E(f6(x83,x81,x84),f6(x83,x82,x84))
% 77.94/78.01 [9]~E(x91,x92)+E(f6(x93,x94,x91),f6(x93,x94,x92))
% 77.94/78.01 [10]~E(x101,x102)+E(f5(x101,x103,x104),f5(x102,x103,x104))
% 77.94/78.01 [11]~E(x111,x112)+E(f5(x113,x111,x114),f5(x113,x112,x114))
% 77.94/78.01 [12]~E(x121,x122)+E(f5(x123,x124,x121),f5(x123,x124,x122))
% 77.94/78.01 [13]~E(x131,x132)+E(f4(x131,x133),f4(x132,x133))
% 77.94/78.01 [14]~E(x141,x142)+E(f4(x143,x141),f4(x143,x142))
% 77.94/78.01 [15]~E(x151,x152)+E(f7(x151,x153,x154),f7(x152,x153,x154))
% 77.94/78.01 [16]~E(x161,x162)+E(f7(x163,x161,x164),f7(x163,x162,x164))
% 77.94/78.01 [17]~E(x171,x172)+E(f7(x173,x174,x171),f7(x173,x174,x172))
% 77.94/78.01 [18]~E(x181,x182)+E(f9(x181,x183,x184),f9(x182,x183,x184))
% 77.94/78.01 [19]~E(x191,x192)+E(f9(x193,x191,x194),f9(x193,x192,x194))
% 77.94/78.01 [20]~E(x201,x202)+E(f9(x203,x204,x201),f9(x203,x204,x202))
% 77.94/78.01 [21]~E(x211,x212)+E(f12(x211,x213),f12(x212,x213))
% 77.94/78.01 [22]~E(x221,x222)+E(f12(x223,x221),f12(x223,x222))
% 77.94/78.01 [23]~E(x231,x232)+E(f11(x231,x233),f11(x232,x233))
% 77.94/78.01 [24]~E(x241,x242)+E(f11(x243,x241),f11(x243,x242))
% 77.94/78.01 [25]~E(x251,x252)+E(f10(x251,x253,x254),f10(x252,x253,x254))
% 77.94/78.01 [26]~E(x261,x262)+E(f10(x263,x261,x264),f10(x263,x262,x264))
% 77.94/78.01 [27]~E(x271,x272)+E(f10(x273,x274,x271),f10(x273,x274,x272))
% 77.94/78.01 [28]~E(x281,x282)+E(f3(x281,x283),f3(x282,x283))
% 77.94/78.01 [29]~E(x291,x292)+E(f3(x293,x291),f3(x293,x292))
% 77.94/78.01 [30]~E(x301,x302)+E(f8(x301,x303,x304),f8(x302,x303,x304))
% 77.94/78.01 [31]~E(x311,x312)+E(f8(x313,x311,x314),f8(x313,x312,x314))
% 77.94/78.01 [32]~E(x321,x322)+E(f8(x323,x324,x321),f8(x323,x324,x322))
% 77.94/78.01 [33]~E(x331,x332)+E(f13(x331,x333),f13(x332,x333))
% 77.94/78.01 [34]~E(x341,x342)+E(f13(x343,x341),f13(x343,x342))
% 77.94/78.01 [35]P1(x352,x353)+~E(x351,x352)+~P1(x351,x353)
% 77.94/78.01 [36]P1(x363,x362)+~E(x361,x362)+~P1(x363,x361)
% 77.94/78.01 [37]P2(x372,x373)+~E(x371,x372)+~P2(x371,x373)
% 77.94/78.01 [38]P2(x383,x382)+~E(x381,x382)+~P2(x383,x381)
% 77.94/78.01 [39]P4(x392,x393,x394)+~E(x391,x392)+~P4(x391,x393,x394)
% 77.94/78.01 [40]P4(x403,x402,x404)+~E(x401,x402)+~P4(x403,x401,x404)
% 77.94/78.01 [41]P4(x413,x414,x412)+~E(x411,x412)+~P4(x413,x414,x411)
% 77.94/78.01 [42]P13(x422,x423,x424,x425)+~E(x421,x422)+~P13(x421,x423,x424,x425)
% 77.94/78.01 [43]P13(x433,x432,x434,x435)+~E(x431,x432)+~P13(x433,x431,x434,x435)
% 77.94/78.01 [44]P13(x443,x444,x442,x445)+~E(x441,x442)+~P13(x443,x444,x441,x445)
% 77.94/78.01 [45]P13(x453,x454,x455,x452)+~E(x451,x452)+~P13(x453,x454,x455,x451)
% 77.94/78.01 [46]P5(x462,x463,x464,x465)+~E(x461,x462)+~P5(x461,x463,x464,x465)
% 77.94/78.01 [47]P5(x473,x472,x474,x475)+~E(x471,x472)+~P5(x473,x471,x474,x475)
% 77.94/78.01 [48]P5(x483,x484,x482,x485)+~E(x481,x482)+~P5(x483,x484,x481,x485)
% 77.94/78.01 [49]P5(x493,x494,x495,x492)+~E(x491,x492)+~P5(x493,x494,x495,x491)
% 77.94/78.01 [50]P9(x502,x503,x504)+~E(x501,x502)+~P9(x501,x503,x504)
% 77.94/78.01 [51]P9(x513,x512,x514)+~E(x511,x512)+~P9(x513,x511,x514)
% 77.94/78.01 [52]P9(x523,x524,x522)+~E(x521,x522)+~P9(x523,x524,x521)
% 77.94/78.01 [53]P6(x532,x533)+~E(x531,x532)+~P6(x531,x533)
% 77.94/78.01 [54]P6(x543,x542)+~E(x541,x542)+~P6(x543,x541)
% 77.94/78.01 [55]P3(x552,x553)+~E(x551,x552)+~P3(x551,x553)
% 77.94/78.01 [56]P3(x563,x562)+~E(x561,x562)+~P3(x563,x561)
% 77.94/78.01 [57]P8(x572,x573)+~E(x571,x572)+~P8(x571,x573)
% 77.94/78.01 [58]P8(x583,x582)+~E(x581,x582)+~P8(x583,x581)
% 77.94/78.01 [59]P10(x592,x593,x594)+~E(x591,x592)+~P10(x591,x593,x594)
% 77.94/78.01 [60]P10(x603,x602,x604)+~E(x601,x602)+~P10(x603,x601,x604)
% 77.94/78.01 [61]P10(x613,x614,x612)+~E(x611,x612)+~P10(x613,x614,x611)
% 77.94/78.01 [62]P11(x622,x623,x624)+~E(x621,x622)+~P11(x621,x623,x624)
% 77.94/78.01 [63]P11(x633,x632,x634)+~E(x631,x632)+~P11(x633,x631,x634)
% 77.94/78.01 [64]P11(x643,x644,x642)+~E(x641,x642)+~P11(x643,x644,x641)
% 77.94/78.01 [65]P12(x652,x653,x654)+~E(x651,x652)+~P12(x651,x653,x654)
% 77.94/78.01 [66]P12(x663,x662,x664)+~E(x661,x662)+~P12(x663,x661,x664)
% 77.94/78.01 [67]P12(x673,x674,x672)+~E(x671,x672)+~P12(x673,x674,x671)
% 77.94/78.01 [68]P7(x682,x683,x684)+~E(x681,x682)+~P7(x681,x683,x684)
% 77.94/78.01 [69]P7(x693,x692,x694)+~E(x691,x692)+~P7(x693,x691,x694)
% 77.94/78.01 [70]P7(x703,x704,x702)+~E(x701,x702)+~P7(x703,x704,x701)
% 77.94/78.01
% 77.94/78.01 %-------------------------------------------
% 77.94/78.03 cnf(208,plain,
% 77.94/78.03 (P8(x2081,x2081)),
% 77.94/78.03 inference(equality_inference,[],[97])).
% 77.94/78.03 cnf(209,plain,
% 77.94/78.03 (~P6(x2091,x2091)),
% 77.94/78.03 inference(equality_inference,[],[101])).
% 77.94/78.03 cnf(211,plain,
% 77.94/78.03 (~P2(f25(x2111),x2113)+P13(a2,x2113,f25(f14(x2111,x2112)),x2112)),
% 77.94/78.03 inference(equality_inference,[],[176])).
% 77.94/78.03 cnf(216,plain,
% 77.94/78.03 (~P10(x2161,a2,x2162)),
% 77.94/78.03 inference(scs_inference,[],[84,85,88,135,136,148])).
% 77.94/78.03 cnf(217,plain,
% 77.94/78.03 (~E(f25(x2171),a2)),
% 77.94/78.03 inference(rename_variables,[],[88])).
% 77.94/78.03 cnf(219,plain,
% 77.94/78.03 (~P6(f14(x2191,x2192),f14(x2192,x2191))),
% 77.94/78.03 inference(scs_inference,[],[83,84,85,88,135,136,148,101])).
% 77.94/78.03 cnf(222,plain,
% 77.94/78.03 (~P6(x2221,x2221)),
% 77.94/78.03 inference(rename_variables,[],[209])).
% 77.94/78.03 cnf(225,plain,
% 77.94/78.03 (~P6(x2251,x2251)),
% 77.94/78.03 inference(rename_variables,[],[209])).
% 77.94/78.03 cnf(227,plain,
% 77.94/78.03 (~P8(a17,a15)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,84,85,88,135,136,148,101,103,104,105])).
% 77.94/78.03 cnf(228,plain,
% 77.94/78.03 (~P6(x2281,x2281)),
% 77.94/78.03 inference(rename_variables,[],[209])).
% 77.94/78.03 cnf(230,plain,
% 77.94/78.03 (~P8(a18,a16)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,228,84,85,88,135,136,148,101,103,104,105,106])).
% 77.94/78.03 cnf(231,plain,
% 77.94/78.03 (~P6(x2311,x2311)),
% 77.94/78.03 inference(rename_variables,[],[209])).
% 77.94/78.03 cnf(233,plain,
% 77.94/78.03 (~P8(a20,a18)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,228,231,84,85,88,135,136,148,101,103,104,105,106,107])).
% 77.94/78.03 cnf(234,plain,
% 77.94/78.03 (~P6(x2341,x2341)),
% 77.94/78.03 inference(rename_variables,[],[209])).
% 77.94/78.03 cnf(236,plain,
% 77.94/78.03 (~P8(a19,a20)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,228,231,234,84,85,88,135,136,148,101,103,104,105,106,107,108])).
% 77.94/78.03 cnf(237,plain,
% 77.94/78.03 (~P6(x2371,x2371)),
% 77.94/78.03 inference(rename_variables,[],[209])).
% 77.94/78.03 cnf(239,plain,
% 77.94/78.03 (~P8(a22,a19)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,228,231,234,237,84,85,88,135,136,148,101,103,104,105,106,107,108,109])).
% 77.94/78.03 cnf(240,plain,
% 77.94/78.03 (~P6(x2401,x2401)),
% 77.94/78.03 inference(rename_variables,[],[209])).
% 77.94/78.03 cnf(242,plain,
% 77.94/78.03 (~P8(a23,a22)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,228,231,234,237,240,84,85,88,135,136,148,101,103,104,105,106,107,108,109,110])).
% 77.94/78.03 cnf(243,plain,
% 77.94/78.03 (~P6(x2431,x2431)),
% 77.94/78.03 inference(rename_variables,[],[209])).
% 77.94/78.03 cnf(245,plain,
% 77.94/78.03 (~P8(a24,a23)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,228,231,234,237,240,243,84,85,88,135,136,148,101,103,104,105,106,107,108,109,110,111])).
% 77.94/78.03 cnf(246,plain,
% 77.94/78.03 (~P6(x2461,x2461)),
% 77.94/78.03 inference(rename_variables,[],[209])).
% 77.94/78.03 cnf(248,plain,
% 77.94/78.03 (~P6(a16,a17)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,228,231,234,237,240,243,84,85,88,135,136,148,101,103,104,105,106,107,108,109,110,111,121])).
% 77.94/78.03 cnf(250,plain,
% 77.94/78.03 (~P11(x2501,x2502,a1)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,228,231,234,237,240,243,94,84,85,88,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171])).
% 77.94/78.03 cnf(251,plain,
% 77.94/78.03 (~P6(x2511,a1)),
% 77.94/78.03 inference(rename_variables,[],[94])).
% 77.94/78.03 cnf(253,plain,
% 77.94/78.03 (~P12(x2531,x2532,a1)),
% 77.94/78.03 inference(scs_inference,[],[83,209,222,225,228,231,234,237,240,243,94,251,84,85,88,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172])).
% 77.94/78.03 cnf(254,plain,
% 77.94/78.03 (~P6(x2541,a1)),
% 77.94/78.03 inference(rename_variables,[],[94])).
% 77.94/78.03 cnf(258,plain,
% 77.94/78.03 (E(a1,f14(a1,a1))),
% 77.94/78.03 inference(scs_inference,[],[83,71,209,222,225,228,231,234,237,240,243,94,251,84,85,88,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2])).
% 77.94/78.03 cnf(264,plain,
% 77.94/78.03 (P6(a1,a16)),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,94,251,254,84,85,86,87,88,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102])).
% 77.94/78.03 cnf(267,plain,
% 77.94/78.03 (~P3(a21,a1)),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,94,251,254,84,85,86,87,90,88,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122])).
% 77.94/78.03 cnf(269,plain,
% 77.94/78.03 (P13(a2,a1,f25(f14(x2691,a1)),x2691)),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,94,251,254,84,85,86,87,90,88,82,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122,176])).
% 77.94/78.03 cnf(272,plain,
% 77.94/78.03 (~E(a16,f14(a1,a1))),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,94,251,254,84,85,86,87,90,88,82,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122,176,3])).
% 77.94/78.03 cnf(273,plain,
% 77.94/78.03 (P2(f25(a1),f14(a1,a1))),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,94,251,254,84,85,86,87,90,88,82,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122,176,3,38])).
% 77.94/78.03 cnf(275,plain,
% 77.94/78.03 (~E(a1,a16)),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,246,94,251,254,84,85,86,87,90,88,82,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122,176,3,38,43,53])).
% 77.94/78.03 cnf(277,plain,
% 77.94/78.03 (~E(a1,a15)),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,246,208,94,251,254,84,85,86,87,90,88,82,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122,176,3,38,43,53,57])).
% 77.94/78.03 cnf(278,plain,
% 77.94/78.03 (P8(x2781,x2781)),
% 77.94/78.03 inference(rename_variables,[],[208])).
% 77.94/78.03 cnf(279,plain,
% 77.94/78.03 (~E(a15,a1)),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,246,208,278,94,251,254,84,85,86,87,90,88,82,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122,176,3,38,43,53,57,58])).
% 77.94/78.03 cnf(284,plain,
% 77.94/78.03 (~P4(a2,a28,x2841)),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,246,208,278,94,251,254,84,85,86,87,90,88,217,89,82,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122,176,3,38,43,53,57,58,161,162])).
% 77.94/78.03 cnf(289,plain,
% 77.94/78.03 (~E(a16,a17)),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,246,208,278,94,251,254,84,85,86,87,90,88,217,89,82,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122,176,3,38,43,53,57,58,161,162,151,97])).
% 77.94/78.03 cnf(292,plain,
% 77.94/78.03 (P2(x2921,f14(a1,a1))+~E(f25(a1),x2921)),
% 77.94/78.03 inference(scs_inference,[],[81,83,92,71,209,222,225,228,231,234,237,240,243,246,208,278,94,251,254,84,85,86,87,90,88,217,89,82,135,136,148,101,103,104,105,106,107,108,109,110,111,121,171,172,191,2,36,99,100,102,122,176,3,38,43,53,57,58,161,162,151,97,35,37])).
% 77.94/78.03 cnf(303,plain,
% 77.94/78.03 (~P6(a17,a15)),
% 77.94/78.03 inference(scs_inference,[],[227,88,136,121])).
% 77.94/78.03 cnf(305,plain,
% 77.94/78.03 (~P8(a17,a1)),
% 77.94/78.03 inference(scs_inference,[],[227,88,136,121,103])).
% 77.94/78.03 cnf(307,plain,
% 77.94/78.03 (~E(a17,a15)),
% 77.94/78.03 inference(scs_inference,[],[227,88,136,121,103,97])).
% 77.94/78.03 cnf(315,plain,
% 77.94/78.03 (~P10(x3151,a27,x3152)),
% 77.94/78.03 inference(scs_inference,[],[71,227,88,89,86,136,121,103,97,135,101,191,148])).
% 77.94/78.03 cnf(318,plain,
% 77.94/78.03 (~P8(a16,a15)),
% 77.94/78.03 inference(scs_inference,[],[71,227,248,88,89,86,136,121,103,97,135,101,191,148,105])).
% 77.94/78.03 cnf(322,plain,
% 77.94/78.03 (E(a15,f14(a1,a15))),
% 77.94/78.03 inference(scs_inference,[],[71,72,284,227,248,88,89,86,136,121,103,97,135,101,191,148,105,151,2])).
% 77.94/78.03 cnf(325,plain,
% 77.94/78.03 (P6(a17,a16)),
% 77.94/78.03 inference(scs_inference,[],[71,72,273,284,258,227,248,289,88,89,86,136,121,103,97,135,101,191,148,105,151,2,176,102])).
% 77.94/78.03 cnf(327,plain,
% 77.94/78.03 (P13(a2,a1,f25(a1),a1)),
% 77.94/78.03 inference(scs_inference,[],[71,72,273,284,258,227,248,289,88,89,86,136,121,103,97,135,101,191,148,105,151,2,176,102,43])).
% 77.94/78.03 cnf(328,plain,
% 77.94/78.03 (~E(a1,f14(a1,a15))),
% 77.94/78.03 inference(scs_inference,[],[71,72,273,284,258,227,248,277,289,88,89,86,136,121,103,97,135,101,191,148,105,151,2,176,102,43,3])).
% 77.94/78.03 cnf(329,plain,
% 77.94/78.03 (~E(a17,a16)),
% 77.94/78.03 inference(scs_inference,[],[71,72,273,284,258,227,248,277,289,209,88,89,86,136,121,103,97,135,101,191,148,105,151,2,176,102,43,3,53])).
% 77.94/78.03 cnf(331,plain,
% 77.94/78.03 (P13(a2,f14(a1,a1),f25(a1),f14(a1,a1))),
% 77.94/78.03 inference(scs_inference,[],[71,72,273,284,258,227,248,277,289,209,88,89,86,136,121,103,97,135,101,191,148,105,151,2,176,102,43,3,53,45])).
% 77.94/78.03 cnf(340,plain,
% 77.94/78.03 (~P6(a18,a16)),
% 77.94/78.03 inference(scs_inference,[],[230,121])).
% 77.94/78.03 cnf(342,plain,
% 77.94/78.03 (~P8(a18,a17)),
% 77.94/78.03 inference(scs_inference,[],[230,121,104])).
% 77.94/78.03 cnf(344,plain,
% 77.94/78.03 (~E(a18,a16)),
% 77.94/78.03 inference(scs_inference,[],[230,121,104,97])).
% 77.94/78.03 cnf(348,plain,
% 77.94/78.03 (E(a16,f14(a1,a16))),
% 77.94/78.03 inference(scs_inference,[],[73,230,121,104,97,101,2])).
% 77.94/78.03 cnf(349,plain,
% 77.94/78.03 (P13(a2,f14(a1,a1),f25(a15),a15)),
% 77.94/78.03 inference(scs_inference,[],[73,273,230,322,121,104,97,101,2,176])).
% 77.94/78.03 cnf(355,plain,
% 77.94/78.03 (~E(a15,a17)),
% 77.94/78.03 inference(scs_inference,[],[71,73,273,230,303,322,327,307,209,258,121,104,97,101,2,176,45,102,43,53])).
% 77.94/78.03 cnf(357,plain,
% 77.94/78.03 (~E(a1,f14(a1,a16))),
% 77.94/78.03 inference(scs_inference,[],[71,73,273,230,303,275,322,327,307,209,258,121,104,97,101,2,176,45,102,43,53,3])).
% 77.94/78.03 cnf(358,plain,
% 77.94/78.03 (~E(a17,a1)),
% 77.94/78.03 inference(scs_inference,[],[71,73,273,94,230,303,275,322,327,307,209,258,121,104,97,101,2,176,45,102,43,53,3,54])).
% 77.94/78.03 cnf(368,plain,
% 77.94/78.03 (~P6(a16,a15)),
% 77.94/78.03 inference(scs_inference,[],[318,121])).
% 77.94/78.03 cnf(374,plain,
% 77.94/78.03 (~E(a16,a15)),
% 77.94/78.03 inference(scs_inference,[],[74,318,121,103,101,97])).
% 77.94/78.03 cnf(376,plain,
% 77.94/78.03 (E(a17,f14(a1,a17))),
% 77.94/78.03 inference(scs_inference,[],[74,318,121,103,101,97,2])).
% 77.94/78.03 cnf(377,plain,
% 77.94/78.03 (~E(a1,a17)),
% 77.94/78.03 inference(scs_inference,[],[74,208,305,318,121,103,101,97,2,57])).
% 77.94/78.03 cnf(379,plain,
% 77.94/78.03 (P13(a2,f14(a1,a1),f25(a16),a16)),
% 77.94/78.03 inference(scs_inference,[],[74,273,208,305,318,348,121,103,101,97,2,57,176])).
% 77.94/78.03 cnf(381,plain,
% 77.94/78.03 (P6(a16,a18)),
% 77.94/78.03 inference(scs_inference,[],[74,273,208,305,318,340,348,344,121,103,101,97,2,57,176,102])).
% 77.94/78.03 cnf(383,plain,
% 77.94/78.03 (P13(a2,a1,f25(a16),a16)),
% 77.94/78.03 inference(scs_inference,[],[71,74,273,208,305,318,340,348,344,121,103,101,97,2,57,176,102,43])).
% 77.94/78.03 cnf(384,plain,
% 77.94/78.03 (P13(a2,f14(a1,a1),f25(a15),f14(a1,a15))),
% 77.94/78.03 inference(scs_inference,[],[71,74,273,208,305,318,340,348,349,344,322,121,103,101,97,2,57,176,102,43,45])).
% 77.94/78.03 cnf(385,plain,
% 77.94/78.03 (~E(a17,a18)),
% 77.94/78.03 inference(scs_inference,[],[71,325,74,273,208,305,318,340,348,349,344,322,121,103,101,97,2,57,176,102,43,45,53])).
% 77.94/78.03 cnf(386,plain,
% 77.94/78.03 (~E(a15,f14(a1,a17))),
% 77.94/78.03 inference(scs_inference,[],[71,325,74,273,208,305,318,340,348,349,344,355,322,121,103,101,97,2,57,176,102,43,45,53,3])).
% 77.94/78.03 cnf(387,plain,
% 77.94/78.03 (~E(a18,a1)),
% 77.94/78.03 inference(scs_inference,[],[71,325,74,273,208,94,305,318,340,348,349,344,355,322,121,103,101,97,2,57,176,102,43,45,53,3,54])).
% 77.94/78.03 cnf(397,plain,
% 77.94/78.03 (~P6(a20,a18)),
% 77.94/78.03 inference(scs_inference,[],[233,121])).
% 77.94/78.03 cnf(399,plain,
% 78.01/78.03 (~E(a20,a18)),
% 78.01/78.03 inference(scs_inference,[],[233,121,97])).
% 78.01/78.03 cnf(403,plain,
% 78.01/78.03 (E(a17,f14(a15,a15))),
% 78.01/78.03 inference(scs_inference,[],[75,233,121,97,101,2])).
% 78.01/78.03 cnf(404,plain,
% 78.01/78.03 (P6(a15,a16)),
% 78.01/78.03 inference(scs_inference,[],[75,233,368,374,121,97,101,2,102])).
% 78.01/78.03 cnf(406,plain,
% 78.01/78.03 (P13(a2,f14(a1,a1),f25(a17),a17)),
% 78.01/78.03 inference(scs_inference,[],[75,273,233,368,376,374,121,97,101,2,102,176])).
% 78.01/78.03 cnf(409,plain,
% 78.01/78.03 (P13(a2,f14(a1,a1),f25(a15),f14(a15,a1))),
% 78.01/78.03 inference(scs_inference,[],[71,75,83,273,233,368,384,376,374,121,97,101,2,102,176,43,45])).
% 78.01/78.03 cnf(411,plain,
% 78.01/78.03 (~E(a16,a18)),
% 78.01/78.03 inference(scs_inference,[],[71,381,75,83,273,209,233,368,384,376,374,121,97,101,2,102,176,43,45,53])).
% 78.01/78.03 cnf(413,plain,
% 78.01/78.03 (~E(a1,f14(a15,a15))),
% 78.01/78.03 inference(scs_inference,[],[71,381,75,83,273,209,233,368,384,376,374,377,121,97,101,2,102,176,43,45,53,3])).
% 78.01/78.03 cnf(414,plain,
% 78.01/78.03 (~P8(a20,a16)),
% 78.01/78.03 inference(scs_inference,[],[71,381,75,83,273,209,233,368,384,376,374,377,121,97,101,2,102,176,43,45,53,3,106])).
% 78.01/78.03 cnf(424,plain,
% 78.01/78.03 (~P6(a18,a17)),
% 78.01/78.03 inference(scs_inference,[],[342,121])).
% 78.01/78.03 cnf(426,plain,
% 78.01/78.03 (~E(a18,a17)),
% 78.01/78.03 inference(scs_inference,[],[342,121,97])).
% 78.01/78.03 cnf(430,plain,
% 78.01/78.03 (E(a18,f14(a15,a16))),
% 78.01/78.03 inference(scs_inference,[],[76,342,121,97,101,2])).
% 78.01/78.03 cnf(431,plain,
% 78.01/78.03 (P6(a18,a20)),
% 78.01/78.03 inference(scs_inference,[],[76,342,397,399,121,97,101,2,102])).
% 78.01/78.03 cnf(433,plain,
% 78.01/78.03 (P13(a2,f14(a1,a1),f25(a16),f14(a1,a16))),
% 78.01/78.03 inference(scs_inference,[],[76,342,397,379,399,348,121,97,101,2,102,45])).
% 78.01/78.03 cnf(434,plain,
% 78.01/78.03 (P13(a2,a1,f25(a15),f14(a15,a1))),
% 78.01/78.03 inference(scs_inference,[],[71,76,342,397,409,379,399,348,121,97,101,2,102,45,43])).
% 78.01/78.03 cnf(435,plain,
% 78.03/78.03 (~E(a15,a16)),
% 78.03/78.03 inference(scs_inference,[],[71,404,76,209,342,397,409,379,399,348,121,97,101,2,102,45,43,53])).
% 78.03/78.03 cnf(437,plain,
% 78.03/78.03 (~E(a17,f14(a15,a16))),
% 78.03/78.03 inference(scs_inference,[],[71,404,76,209,342,397,409,379,385,399,348,121,97,101,2,102,45,43,53,3])).
% 78.03/78.03 cnf(438,plain,
% 78.03/78.03 (~P8(a18,a15)),
% 78.03/78.03 inference(scs_inference,[],[71,404,76,209,342,397,409,379,385,399,348,121,97,101,2,102,45,43,53,3,105])).
% 78.03/78.03 cnf(445,plain,
% 78.03/78.03 (~P6(a19,a20)),
% 78.03/78.03 inference(scs_inference,[],[236,121])).
% 78.03/78.03 cnf(447,plain,
% 78.03/78.03 (~E(a19,a20)),
% 78.03/78.03 inference(scs_inference,[],[236,121,97])).
% 78.03/78.03 cnf(451,plain,
% 78.03/78.03 (E(a16,f14(a15,a17))),
% 78.03/78.03 inference(scs_inference,[],[77,236,121,97,101,2])).
% 78.03/78.03 cnf(452,plain,
% 78.03/78.03 (P6(a17,a18)),
% 78.03/78.03 inference(scs_inference,[],[77,236,424,426,121,97,101,2,102])).
% 78.03/78.03 cnf(454,plain,
% 78.03/78.03 (P13(a2,f14(a1,a1),f25(a17),f14(a1,a17))),
% 78.03/78.04 inference(scs_inference,[],[77,236,406,424,426,376,121,97,101,2,102,45])).
% 78.03/78.04 cnf(455,plain,
% 78.03/78.04 (~E(a18,a20)),
% 78.03/78.04 inference(scs_inference,[],[431,77,209,236,406,424,426,376,121,97,101,2,102,45,53])).
% 78.03/78.04 cnf(457,plain,
% 78.03/78.04 (P13(a2,a1,f25(a17),a17)),
% 78.03/78.04 inference(scs_inference,[],[71,431,77,209,236,406,424,426,376,121,97,101,2,102,45,53,43])).
% 78.03/78.04 cnf(458,plain,
% 78.03/78.04 (~E(a17,f14(a15,a17))),
% 78.03/78.04 inference(scs_inference,[],[71,431,77,209,236,329,406,424,426,376,121,97,101,2,102,45,53,43,3])).
% 78.03/78.04 cnf(459,plain,
% 78.03/78.04 (~P8(a19,a18)),
% 78.03/78.04 inference(scs_inference,[],[71,431,77,209,236,329,406,424,426,376,121,97,101,2,102,45,53,43,3,107])).
% 78.03/78.04 cnf(466,plain,
% 78.03/78.04 (~E(a20,a16)),
% 78.03/78.04 inference(scs_inference,[],[414,97])).
% 78.03/78.04 cnf(468,plain,
% 78.03/78.04 (~P6(a20,a16)),
% 78.03/78.04 inference(scs_inference,[],[414,97,121])).
% 78.03/78.04 cnf(472,plain,
% 78.03/78.04 (E(a19,f14(a16,a16))),
% 78.03/78.04 inference(scs_inference,[],[78,414,97,121,101,2])).
% 78.03/78.04 cnf(473,plain,
% 78.03/78.04 (P6(a20,a19)),
% 78.03/78.04 inference(scs_inference,[],[78,414,445,447,97,121,101,2,102])).
% 78.03/78.04 cnf(475,plain,
% 78.03/78.04 (~E(a20,a1)),
% 78.03/78.04 inference(scs_inference,[],[431,78,94,414,445,447,97,121,101,2,102,54])).
% 78.03/78.04 cnf(477,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),f25(a16),f14(a16,a1))),
% 78.03/78.04 inference(scs_inference,[],[431,78,83,94,414,445,433,447,97,121,101,2,102,54,45])).
% 78.03/78.04 cnf(479,plain,
% 78.03/78.04 (P13(a2,a1,f25(a16),f14(a1,a16))),
% 78.03/78.04 inference(scs_inference,[],[71,431,78,83,94,414,445,433,447,97,121,101,2,102,54,45,43])).
% 78.03/78.04 cnf(481,plain,
% 78.03/78.04 (~E(a20,a19)),
% 78.03/78.04 inference(scs_inference,[],[71,431,78,79,83,94,209,414,445,433,447,97,121,101,2,102,54,45,43,3,53])).
% 78.03/78.04 cnf(483,plain,
% 78.03/78.04 (~P8(a20,a17)),
% 78.03/78.04 inference(scs_inference,[],[71,431,78,79,83,94,209,414,445,433,447,97,121,101,2,102,54,45,43,3,53,104])).
% 78.03/78.04 cnf(489,plain,
% 78.03/78.04 (~P6(a18,a15)),
% 78.03/78.04 inference(scs_inference,[],[438,121])).
% 78.03/78.04 cnf(491,plain,
% 78.03/78.04 (~E(a18,a15)),
% 78.03/78.04 inference(scs_inference,[],[438,121,97])).
% 78.03/78.04 cnf(495,plain,
% 78.03/78.04 (E(a18,f14(a17,a17))),
% 78.03/78.04 inference(scs_inference,[],[80,438,121,97,101,2])).
% 78.03/78.04 cnf(496,plain,
% 78.03/78.04 (P6(a16,a20)),
% 78.03/78.04 inference(scs_inference,[],[80,438,468,466,121,97,101,2,102])).
% 78.03/78.04 cnf(498,plain,
% 78.03/78.04 (~E(a19,a1)),
% 78.03/78.04 inference(scs_inference,[],[473,80,94,438,468,466,121,97,101,2,102,54])).
% 78.03/78.04 cnf(500,plain,
% 78.03/78.04 (P13(a2,a1,f25(a16),f14(a15,a17))),
% 78.03/78.04 inference(scs_inference,[],[473,80,94,438,468,383,466,451,121,97,101,2,102,54,45])).
% 78.03/78.04 cnf(501,plain,
% 78.03/78.04 (P13(a2,a1,f25(a17),f14(a1,a17))),
% 78.03/78.04 inference(scs_inference,[],[71,473,80,94,438,468,454,383,466,451,121,97,101,2,102,54,45,43])).
% 78.03/78.04 cnf(502,plain,
% 78.03/78.04 (~E(a16,f14(a17,a17))),
% 78.03/78.04 inference(scs_inference,[],[71,473,80,94,438,411,468,454,383,466,451,121,97,101,2,102,54,45,43,3])).
% 78.03/78.04 cnf(503,plain,
% 78.03/78.04 (~E(a16,a20)),
% 78.03/78.04 inference(scs_inference,[],[71,473,80,94,209,438,411,468,454,383,466,451,121,97,101,2,102,54,45,43,3,53])).
% 78.03/78.04 cnf(516,plain,
% 78.03/78.04 (~E(a19,a18)),
% 78.03/78.04 inference(scs_inference,[],[459,97])).
% 78.03/78.04 cnf(518,plain,
% 78.03/78.04 (~P6(a19,a18)),
% 78.03/78.04 inference(scs_inference,[],[459,97,121])).
% 78.03/78.04 cnf(522,plain,
% 78.03/78.04 (E(a20,f14(a17,a16))),
% 78.03/78.04 inference(scs_inference,[],[79,459,97,121,101,2])).
% 78.03/78.04 cnf(523,plain,
% 78.03/78.04 (P6(a15,a18)),
% 78.03/78.04 inference(scs_inference,[],[79,459,489,491,97,121,101,2,102])).
% 78.03/78.04 cnf(525,plain,
% 78.03/78.04 (P13(a2,a1,f25(a16),f14(a16,a1))),
% 78.03/78.04 inference(scs_inference,[],[71,79,459,489,477,491,97,121,101,2,102,43])).
% 78.03/78.04 cnf(526,plain,
% 78.03/78.04 (~E(a18,f14(a17,a16))),
% 78.03/78.04 inference(scs_inference,[],[71,79,459,455,489,477,491,97,121,101,2,102,43,3])).
% 78.03/78.04 cnf(527,plain,
% 78.03/78.04 (P13(a2,a1,f25(a17),f14(a15,a15))),
% 78.03/78.04 inference(scs_inference,[],[71,79,459,455,489,477,457,491,403,97,121,101,2,102,43,3,45])).
% 78.03/78.04 cnf(528,plain,
% 78.03/78.04 (~E(a15,a18)),
% 78.03/78.04 inference(scs_inference,[],[71,79,209,459,455,489,477,457,491,403,97,121,101,2,102,43,3,45,53])).
% 78.03/78.04 cnf(530,plain,
% 78.03/78.04 (~P8(a19,a16)),
% 78.03/78.04 inference(scs_inference,[],[71,79,209,459,455,489,477,457,491,403,97,121,101,2,102,43,3,45,53,106])).
% 78.03/78.04 cnf(537,plain,
% 78.03/78.04 (~P6(a20,a17)),
% 78.03/78.04 inference(scs_inference,[],[483,121])).
% 78.03/78.04 cnf(539,plain,
% 78.03/78.04 (~E(a20,a17)),
% 78.03/78.04 inference(scs_inference,[],[483,121,97])).
% 78.03/78.04 cnf(543,plain,
% 78.03/78.04 (P6(a18,a19)),
% 78.03/78.04 inference(scs_inference,[],[72,483,518,516,121,97,101,102])).
% 78.03/78.04 cnf(546,plain,
% 78.03/78.04 (~E(a18,a19)),
% 78.03/78.04 inference(scs_inference,[],[72,209,483,518,500,516,258,121,97,101,102,43,53])).
% 78.03/78.04 cnf(549,plain,
% 78.03/78.04 (~P8(a20,a15)),
% 78.03/78.04 inference(scs_inference,[],[78,72,209,483,481,518,500,516,258,121,97,101,102,43,53,3,105])).
% 78.03/78.04 cnf(557,plain,
% 78.03/78.04 (~E(a22,a19)),
% 78.03/78.04 inference(scs_inference,[],[239,97])).
% 78.03/78.04 cnf(559,plain,
% 78.03/78.04 (~P6(a22,a19)),
% 78.03/78.04 inference(scs_inference,[],[239,97,121])).
% 78.03/78.04 cnf(563,plain,
% 78.03/78.04 (P6(a17,a20)),
% 78.03/78.04 inference(scs_inference,[],[239,430,537,539,97,121,101,102])).
% 78.03/78.04 cnf(566,plain,
% 78.03/78.04 (~E(a17,a20)),
% 78.03/78.04 inference(scs_inference,[],[209,239,527,430,258,537,539,97,121,101,102,43,53])).
% 78.03/78.04 cnf(569,plain,
% 78.03/78.04 (~P8(a22,a20)),
% 78.03/78.04 inference(scs_inference,[],[78,209,239,527,430,258,537,539,546,97,121,101,102,43,53,3,108])).
% 78.03/78.04 cnf(571,plain,
% 78.03/78.04 (~P8(f14(a15,a16),a16)),
% 78.03/78.04 inference(scs_inference,[],[78,209,239,527,430,258,537,539,546,97,121,101,102,43,53,3,108,106])).
% 78.03/78.04 cnf(581,plain,
% 78.03/78.04 (~P6(a19,a16)),
% 78.03/78.04 inference(scs_inference,[],[530,121])).
% 78.03/78.04 cnf(583,plain,
% 78.03/78.04 (~E(a19,a16)),
% 78.03/78.04 inference(scs_inference,[],[530,121,97])).
% 78.03/78.04 cnf(587,plain,
% 78.03/78.04 (P6(a19,a22)),
% 78.03/78.04 inference(scs_inference,[],[472,530,559,557,121,97,101,102])).
% 78.03/78.04 cnf(589,plain,
% 78.03/78.04 (~E(a22,a1)),
% 78.03/78.04 inference(scs_inference,[],[94,472,530,559,557,121,97,101,102,54])).
% 78.03/78.04 cnf(591,plain,
% 78.03/78.04 (~E(a1,a18)),
% 78.03/78.04 inference(scs_inference,[],[264,94,340,472,530,559,557,121,97,101,102,54,53])).
% 78.03/78.04 cnf(595,plain,
% 78.03/78.04 (~P8(f14(a16,a16),a20)),
% 78.03/78.04 inference(scs_inference,[],[264,83,73,94,340,472,501,530,435,559,557,121,97,101,102,54,53,45,3,108])).
% 78.03/78.04 cnf(597,plain,
% 78.03/78.04 (~P8(a19,a17)),
% 78.03/78.04 inference(scs_inference,[],[264,83,73,94,340,472,501,530,435,559,557,121,97,101,102,54,53,45,3,108,104])).
% 78.03/78.04 cnf(600,plain,
% 78.03/78.04 (P13(a2,a1,x6001,f14(a1,a16))+~E(f25(a16),x6001)),
% 78.03/78.04 inference(scs_inference,[],[264,83,73,94,340,472,258,479,501,530,435,559,557,121,97,101,102,54,53,45,3,108,104,43,44])).
% 78.03/78.04 cnf(608,plain,
% 78.03/78.04 (~E(a23,a22)),
% 78.03/78.04 inference(scs_inference,[],[242,97])).
% 78.03/78.04 cnf(610,plain,
% 78.03/78.04 (~P6(a23,a22)),
% 78.03/78.04 inference(scs_inference,[],[242,97,121])).
% 78.03/78.04 cnf(614,plain,
% 78.03/78.04 (P6(a16,a19)),
% 78.03/78.04 inference(scs_inference,[],[495,242,581,583,97,121,101,102])).
% 78.03/78.04 cnf(616,plain,
% 78.03/78.04 (~E(a19,a22)),
% 78.03/78.04 inference(scs_inference,[],[587,209,495,242,581,583,97,121,101,102,53])).
% 78.03/78.04 cnf(619,plain,
% 78.03/78.04 (~P8(a23,a19)),
% 78.03/78.04 inference(scs_inference,[],[76,587,209,495,242,528,581,583,97,121,101,102,53,3,109])).
% 78.03/78.04 cnf(621,plain,
% 78.03/78.04 (~P8(f14(a17,a17),a16)),
% 78.03/78.04 inference(scs_inference,[],[76,587,209,495,242,528,581,583,97,121,101,102,53,3,109,106])).
% 78.03/78.04 cnf(623,plain,
% 78.03/78.04 (P13(a2,a1,x6231,f14(a16,a1))+~E(f25(a16),x6231)),
% 78.03/78.04 inference(scs_inference,[],[76,587,209,495,242,525,528,581,583,97,121,101,102,53,3,109,106,44])).
% 78.03/78.04 cnf(624,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x6241,f14(a16,a1))+~E(f25(a16),x6241)),
% 78.03/78.04 inference(scs_inference,[],[76,587,209,495,258,242,525,528,581,583,97,121,101,102,53,3,109,106,44,43])).
% 78.03/78.04 cnf(625,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x6251,f14(a1,a16))+~E(f25(a16),x6251)),
% 78.03/78.04 inference(scs_inference,[],[76,83,587,209,269,495,258,242,525,528,581,583,97,121,101,102,53,3,109,106,44,43,42,45])).
% 78.03/78.04 cnf(634,plain,
% 78.03/78.04 (~P6(a20,a15)),
% 78.03/78.04 inference(scs_inference,[],[549,121])).
% 78.03/78.04 cnf(636,plain,
% 78.03/78.04 (~E(a20,a15)),
% 78.03/78.04 inference(scs_inference,[],[549,121,97])).
% 78.03/78.04 cnf(640,plain,
% 78.03/78.04 (P6(a22,a23)),
% 78.03/78.04 inference(scs_inference,[],[522,549,610,608,121,97,101,102])).
% 78.03/78.04 cnf(644,plain,
% 78.03/78.04 (~E(a16,a19)),
% 78.03/78.04 inference(scs_inference,[],[614,94,209,522,549,610,608,121,97,101,102,54,53])).
% 78.03/78.04 cnf(648,plain,
% 78.03/78.04 (~E(a1,f14(a1,a17))),
% 78.03/78.04 inference(scs_inference,[],[83,74,614,94,209,522,500,549,610,608,377,121,97,101,102,54,53,45,3])).
% 78.03/78.04 cnf(649,plain,
% 78.03/78.04 (~P8(f14(a17,a16),a18)),
% 78.03/78.04 inference(scs_inference,[],[83,74,614,94,209,522,500,549,610,608,377,121,97,101,102,54,53,45,3,107])).
% 78.03/78.04 cnf(653,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),f25(a16),f14(a17,a15))),
% 78.03/78.04 inference(scs_inference,[],[83,74,614,94,209,522,258,500,549,610,608,377,121,97,101,102,54,53,45,3,107,103,43])).
% 78.03/78.04 cnf(654,plain,
% 78.03/78.04 (P13(a2,a1,x6541,f14(a15,a1))+~E(f25(a15),x6541)),
% 78.03/78.04 inference(scs_inference,[],[83,74,614,94,209,522,258,434,500,549,610,608,377,121,97,101,102,54,53,45,3,107,103,43,44])).
% 78.03/78.04 cnf(662,plain,
% 78.03/78.04 (~E(f14(a15,a16),a16)),
% 78.03/78.04 inference(scs_inference,[],[571,97])).
% 78.03/78.04 cnf(664,plain,
% 78.03/78.04 (~P6(f14(a15,a16),a16)),
% 78.03/78.04 inference(scs_inference,[],[571,97,121])).
% 78.03/78.04 cnf(668,plain,
% 78.03/78.04 (P6(a15,a20)),
% 78.03/78.04 inference(scs_inference,[],[403,571,634,636,97,121,101,102])).
% 78.03/78.04 cnf(670,plain,
% 78.03/78.04 (~E(a22,a23)),
% 78.03/78.04 inference(scs_inference,[],[640,209,403,571,634,636,97,121,101,102,53])).
% 78.03/78.04 cnf(672,plain,
% 78.03/78.04 (~E(a1,f14(a17,a17))),
% 78.03/78.04 inference(scs_inference,[],[80,640,209,403,571,634,591,636,97,121,101,102,53,3])).
% 78.03/78.04 cnf(673,plain,
% 78.03/78.04 (~P8(f14(a15,a16),a17)),
% 78.03/78.04 inference(scs_inference,[],[80,640,209,403,571,634,591,636,97,121,101,102,53,3,104])).
% 78.03/78.04 cnf(675,plain,
% 78.03/78.04 (~P8(f14(a15,a15),a15)),
% 78.03/78.04 inference(scs_inference,[],[80,640,209,403,571,634,591,636,97,121,101,102,53,3,104,105])).
% 78.03/78.04 cnf(678,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x6781,f14(a1,a15))+~E(f25(a15),x6781)),
% 78.03/78.04 inference(scs_inference,[],[80,640,209,403,322,349,571,634,591,636,97,121,101,102,53,3,104,105,44,45])).
% 78.03/78.04 cnf(688,plain,
% 78.03/78.04 (~P6(f14(a15,a15),a15)),
% 78.03/78.04 inference(scs_inference,[],[305,75,112,57])).
% 78.03/78.04 cnf(689,plain,
% 78.03/78.04 (~P8(f14(a15,a15),a1)),
% 78.03/78.04 inference(scs_inference,[],[688,103])).
% 78.03/78.04 cnf(691,plain,
% 78.03/78.04 (~P6(a22,a20)),
% 78.03/78.04 inference(scs_inference,[],[569,688,103,121])).
% 78.03/78.04 cnf(693,plain,
% 78.03/78.04 (~E(a22,a20)),
% 78.03/78.04 inference(scs_inference,[],[569,688,103,121,97])).
% 78.03/78.04 cnf(697,plain,
% 78.03/78.04 (P6(a16,f14(a15,a16))),
% 78.03/78.04 inference(scs_inference,[],[451,569,664,662,688,103,121,97,101,102])).
% 78.03/78.04 cnf(699,plain,
% 78.03/78.04 (~E(f14(a15,a16),a1)),
% 78.03/78.04 inference(scs_inference,[],[94,451,569,664,662,688,103,121,97,101,102,54])).
% 78.03/78.04 cnf(703,plain,
% 78.03/78.04 (~E(f14(a15,a16),f14(a15,a17))),
% 78.03/78.04 inference(scs_inference,[],[77,668,94,451,209,569,664,662,688,103,121,97,101,102,54,53,3])).
% 78.03/78.04 cnf(704,plain,
% 78.03/78.04 (~P8(a22,a18)),
% 78.03/78.04 inference(scs_inference,[],[77,668,94,451,209,569,664,662,688,103,121,97,101,102,54,53,3,107])).
% 78.03/78.04 cnf(706,plain,
% 78.03/78.04 (~P8(f14(a15,a17),a17)),
% 78.03/78.04 inference(scs_inference,[],[77,668,94,451,209,569,664,662,688,103,121,97,101,102,54,53,3,107,104])).
% 78.03/78.04 cnf(708,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x7081,a16)+~E(f25(a16),x7081)),
% 78.03/78.04 inference(scs_inference,[],[77,668,94,451,209,379,569,664,662,688,103,121,97,101,102,54,53,3,107,104,44])).
% 78.03/78.04 cnf(709,plain,
% 78.03/78.04 (P13(a2,a1,x7091,a16)+~E(f25(a16),x7091)),
% 78.03/78.04 inference(scs_inference,[],[71,77,668,94,451,209,379,569,664,662,688,103,121,97,101,102,54,53,3,107,104,44,43])).
% 78.03/78.04 cnf(710,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x7101,f14(a15,a17))+~E(f25(a16),x7101)),
% 78.03/78.04 inference(scs_inference,[],[71,77,668,94,451,209,379,569,664,662,688,103,121,97,101,102,54,53,3,107,104,44,43,45])).
% 78.03/78.04 cnf(719,plain,
% 78.03/78.04 (~P6(f14(a16,a16),a20)),
% 78.03/78.04 inference(scs_inference,[],[595,121])).
% 78.03/78.04 cnf(721,plain,
% 78.03/78.04 (~E(f14(a16,a16),a20)),
% 78.03/78.04 inference(scs_inference,[],[595,121,97])).
% 78.03/78.04 cnf(725,plain,
% 78.03/78.04 (P6(a20,a22)),
% 78.03/78.04 inference(scs_inference,[],[348,595,691,693,121,97,101,102])).
% 78.03/78.04 cnf(730,plain,
% 78.03/78.04 (~P8(f14(a16,a16),a18)),
% 78.03/78.04 inference(scs_inference,[],[78,697,209,348,595,644,691,693,121,97,101,102,53,3,107])).
% 78.03/78.04 cnf(732,plain,
% 78.03/78.04 (~P8(f14(a1,a16),a17)),
% 78.03/78.04 inference(scs_inference,[],[78,697,209,348,595,644,691,693,121,97,101,102,53,3,107,104])).
% 78.03/78.04 cnf(734,plain,
% 78.03/78.04 (P13(a2,a1,x7341,a17)+~E(f25(a17),x7341)),
% 78.03/78.04 inference(scs_inference,[],[78,697,209,348,457,595,644,691,693,121,97,101,102,53,3,107,104,44])).
% 78.03/78.04 cnf(735,plain,
% 78.03/78.04 (P13(a2,a1,x7351,f14(a15,a15))+~E(f25(a17),x7351)),
% 78.03/78.04 inference(scs_inference,[],[78,697,403,209,348,457,595,644,691,693,121,97,101,102,53,3,107,104,44,45])).
% 78.03/78.04 cnf(745,plain,
% 78.03/78.04 (~P6(a19,a17)),
% 78.03/78.04 inference(scs_inference,[],[597,121])).
% 78.03/78.04 cnf(747,plain,
% 78.03/78.04 (~E(a19,a17)),
% 78.03/78.04 inference(scs_inference,[],[597,121,97])).
% 78.03/78.04 cnf(749,plain,
% 78.03/78.04 (~P6(f14(a1,a17),a17)),
% 78.03/78.04 inference(scs_inference,[],[376,597,121,97,101])).
% 78.03/78.04 cnf(755,plain,
% 78.03/78.04 (~E(a20,a22)),
% 78.03/78.04 inference(scs_inference,[],[725,94,209,376,597,719,721,121,97,101,102,54,53])).
% 78.03/78.04 cnf(757,plain,
% 78.03/78.04 (~E(f14(a15,a16),f14(a17,a15))),
% 78.03/78.04 inference(scs_inference,[],[83,725,94,209,376,597,703,719,721,121,97,101,102,54,53,3])).
% 78.03/78.04 cnf(759,plain,
% 78.03/78.04 (~P8(a19,a15)),
% 78.03/78.04 inference(scs_inference,[],[83,725,94,209,376,597,703,719,721,121,97,101,102,54,53,3,105])).
% 78.03/78.04 cnf(769,plain,
% 78.03/78.04 (~P8(f14(a1,a17),a15)),
% 78.03/78.04 inference(scs_inference,[],[749,105])).
% 78.03/78.04 cnf(771,plain,
% 78.03/78.04 (~P6(f14(a17,a17),a16)),
% 78.03/78.04 inference(scs_inference,[],[621,749,105,121])).
% 78.03/78.04 cnf(773,plain,
% 78.03/78.04 (~E(f14(a17,a17),a16)),
% 78.03/78.04 inference(scs_inference,[],[621,749,105,121,97])).
% 78.03/78.04 cnf(777,plain,
% 78.03/78.04 (P6(a17,a19)),
% 78.03/78.04 inference(scs_inference,[],[322,621,745,749,747,105,121,97,101,102])).
% 78.03/78.04 cnf(779,plain,
% 78.03/78.04 (~E(a17,a19)),
% 78.03/78.04 inference(scs_inference,[],[209,322,621,745,749,747,105,121,97,101,102,53])).
% 78.03/78.04 cnf(782,plain,
% 78.03/78.04 (~P8(f14(a1,a15),a1)),
% 78.03/78.04 inference(scs_inference,[],[79,209,322,621,503,745,749,747,105,121,97,101,102,53,3,103])).
% 78.03/78.04 cnf(784,plain,
% 78.03/78.04 (~P8(f14(a17,a17),a17)),
% 78.03/78.04 inference(scs_inference,[],[79,209,322,621,503,745,749,747,105,121,97,101,102,53,3,103,104])).
% 78.03/78.04 cnf(786,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x7861,f14(a1,a17))+~E(f25(a17),x7861)),
% 78.03/78.04 inference(scs_inference,[],[79,209,322,454,621,503,745,749,747,105,121,97,101,102,53,3,103,104,44])).
% 78.03/78.04 cnf(787,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x7871,f14(a17,a1))+~E(f25(a17),x7871)),
% 78.03/78.04 inference(scs_inference,[],[83,79,209,322,454,621,503,745,749,747,105,121,97,101,102,53,3,103,104,44,45])).
% 78.03/78.04 cnf(798,plain,
% 78.03/78.04 (~P6(a23,a19)),
% 78.03/78.04 inference(scs_inference,[],[619,121])).
% 78.03/78.04 cnf(800,plain,
% 78.03/78.04 (~E(a23,a19)),
% 78.03/78.04 inference(scs_inference,[],[619,121,97])).
% 78.03/78.04 cnf(807,plain,
% 78.03/78.04 (~P8(a23,a20)),
% 78.03/78.04 inference(scs_inference,[],[75,94,619,771,773,289,121,97,102,54,3,108])).
% 78.03/78.04 cnf(809,plain,
% 78.03/78.04 (P13(a2,a1,x8091,f14(a1,a17))+~E(f25(a17),x8091)),
% 78.03/78.04 inference(scs_inference,[],[75,94,501,619,771,773,289,121,97,102,54,3,108,44])).
% 78.03/78.04 cnf(810,plain,
% 78.03/78.04 (P13(a2,a1,x8101,f14(a17,a1))+~E(f25(a17),x8101)),
% 78.03/78.04 inference(scs_inference,[],[83,75,94,501,619,771,773,289,121,97,102,54,3,108,44,45])).
% 78.03/78.04 cnf(821,plain,
% 78.03/78.04 (~P6(f14(a17,a16),a18)),
% 78.03/78.04 inference(scs_inference,[],[649,121])).
% 78.03/78.04 cnf(823,plain,
% 78.03/78.04 (~E(f14(a17,a16),a18)),
% 78.03/78.04 inference(scs_inference,[],[649,121,97])).
% 78.03/78.04 cnf(825,plain,
% 78.03/78.04 (P6(a19,a23)),
% 78.03/78.04 inference(scs_inference,[],[649,798,800,121,97,102])).
% 78.03/78.04 cnf(827,plain,
% 78.03/78.04 (~E(a19,a23)),
% 78.03/78.04 inference(scs_inference,[],[209,649,798,800,121,97,102,53])).
% 78.03/78.04 cnf(830,plain,
% 78.03/78.04 (~P8(f14(a17,a16),a16)),
% 78.03/78.04 inference(scs_inference,[],[77,209,649,798,800,435,121,97,102,53,3,106])).
% 78.03/78.04 cnf(832,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x8321,f14(a15,a1))+~E(f25(a15),x8321)),
% 78.03/78.04 inference(scs_inference,[],[77,209,409,649,798,800,435,121,97,102,53,3,106,44])).
% 78.03/78.04 cnf(840,plain,
% 78.03/78.04 (~P6(f14(a15,a16),a17)),
% 78.03/78.04 inference(scs_inference,[],[673,121])).
% 78.03/78.04 cnf(842,plain,
% 78.03/78.04 (~E(f14(a15,a16),a17)),
% 78.03/78.04 inference(scs_inference,[],[673,121,97])).
% 78.03/78.04 cnf(846,plain,
% 78.03/78.04 (~E(f14(a17,a16),a1)),
% 78.03/78.04 inference(scs_inference,[],[94,673,821,823,121,97,102,54])).
% 78.03/78.04 cnf(849,plain,
% 78.03/78.04 (~P8(f14(a15,a16),a15)),
% 78.03/78.04 inference(scs_inference,[],[76,94,673,821,823,121,97,102,54,3,105])).
% 78.03/78.04 cnf(851,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x8511,a17)+~E(f25(a17),x8511)),
% 78.03/78.04 inference(scs_inference,[],[76,94,406,673,821,823,121,97,102,54,3,105,44])).
% 78.03/78.04 cnf(852,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x8521,f14(a15,a15))+~E(f25(a17),x8521)),
% 78.03/78.04 inference(scs_inference,[],[76,403,94,406,673,821,823,121,97,102,54,3,105,44,45])).
% 78.03/78.04 cnf(859,plain,
% 78.03/78.04 (~E(f14(a15,a15),a15)),
% 78.03/78.04 inference(scs_inference,[],[675,97])).
% 78.03/78.04 cnf(861,plain,
% 78.03/78.04 (~P6(a22,a18)),
% 78.03/78.04 inference(scs_inference,[],[675,704,97,121])).
% 78.03/78.04 cnf(868,plain,
% 78.03/78.04 (~P8(a22,a16)),
% 78.03/78.04 inference(scs_inference,[],[73,209,675,704,688,329,97,121,102,53,3,106])).
% 78.03/78.04 cnf(881,plain,
% 78.03/78.04 (~P6(f14(a15,a17),a17)),
% 78.03/78.04 inference(scs_inference,[],[706,121])).
% 78.03/78.04 cnf(888,plain,
% 78.03/78.04 (~P8(f14(a15,a17),a15)),
% 78.03/78.04 inference(scs_inference,[],[80,689,706,840,842,516,121,97,102,3,105])).
% 78.03/78.04 cnf(890,plain,
% 78.03/78.04 (P13(a2,a1,x8901,f14(a15,a17))+~E(f25(a16),x8901)),
% 78.03/78.04 inference(scs_inference,[],[80,500,689,706,840,842,516,121,97,102,3,105,44])).
% 78.03/78.04 cnf(891,plain,
% 78.03/78.04 (P13(a2,a1,x8911,f14(a17,a15))+~E(f25(a16),x8911)),
% 78.03/78.04 inference(scs_inference,[],[83,80,500,689,706,840,842,516,121,97,102,3,105,44,45])).
% 78.03/78.04 cnf(899,plain,
% 78.03/78.04 (~E(a22,a18)),
% 78.03/78.04 inference(scs_inference,[],[704,97])).
% 78.03/78.04 cnf(903,plain,
% 78.03/78.04 (P6(a18,a22)),
% 78.03/78.04 inference(scs_inference,[],[704,730,861,97,121,102])).
% 78.03/78.04 cnf(905,plain,
% 78.03/78.04 (~E(a18,a22)),
% 78.03/78.04 inference(scs_inference,[],[209,704,730,861,97,121,102,53])).
% 78.03/78.04 cnf(908,plain,
% 78.03/78.04 (~P8(f14(a16,a16),a16)),
% 78.03/78.04 inference(scs_inference,[],[72,209,704,730,861,859,97,121,102,53,3,106])).
% 78.03/78.04 cnf(910,plain,
% 78.03/78.04 (P13(a2,f14(a1,a1),x9101,f14(a17,a15))+~E(f25(a16),x9101)),
% 78.03/78.04 inference(scs_inference,[],[72,209,653,704,730,861,859,97,121,102,53,3,106,44])).
% 78.03/78.04 cnf(918,plain,
% 78.03/78.04 (~P6(f14(a1,a16),a17)),
% 78.03/78.04 inference(scs_inference,[],[732,121])).
% 78.03/78.04 cnf(920,plain,
% 78.03/78.04 (~E(f14(a15,a17),a17)),
% 78.03/78.04 inference(scs_inference,[],[706,732,121,97])).
% 78.03/78.04 cnf(925,plain,
% 78.03/78.04 (~P8(f14(a1,a16),a15)),
% 78.03/78.04 inference(scs_inference,[],[74,706,732,881,426,121,97,102,3,105])).
% 78.03/78.04 cnf(933,plain,
% 78.03/78.04 (~E(f14(a16,a16),a18)),
% 78.03/78.04 inference(scs_inference,[],[730,97])).
% 78.03/78.04 cnf(935,plain,
% 78.03/78.04 (~P6(a19,a15)),
% 78.03/78.04 inference(scs_inference,[],[730,759,97,121])).
% 78.03/78.04 cnf(950,plain,
% 78.03/78.04 (~P6(f14(a17,a17),a17)),
% 78.03/78.04 inference(scs_inference,[],[784,121])).
% 78.03/78.04 cnf(952,plain,
% 78.03/78.04 (~E(f14(a1,a16),a17)),
% 78.03/78.04 inference(scs_inference,[],[732,784,121,97])).
% 78.03/78.04 cnf(957,plain,
% 78.03/78.04 (~P8(f14(a17,a17),a15)),
% 78.03/78.04 inference(scs_inference,[],[78,732,784,918,779,121,97,102,3,105])).
% 78.03/78.04 cnf(967,plain,
% 78.03/78.04 (~E(a19,a15)),
% 78.03/78.04 inference(scs_inference,[],[759,97])).
% 78.03/78.04 cnf(969,plain,
% 78.03/78.04 (~P6(f14(a1,a17),a15)),
% 78.03/78.04 inference(scs_inference,[],[759,769,97,121])).
% 78.03/78.04 cnf(971,plain,
% 78.03/78.04 (P6(a15,a19)),
% 78.03/78.04 inference(scs_inference,[],[759,769,935,97,121,102])).
% 78.03/78.04 cnf(973,plain,
% 78.03/78.04 (~E(a15,a19)),
% 78.03/78.04 inference(scs_inference,[],[209,759,769,935,97,121,102,53])).
% 78.03/78.04 cnf(975,plain,
% 78.03/78.04 (~E(f14(a16,a16),f14(a17,a17))),
% 78.03/78.04 inference(scs_inference,[],[80,209,759,769,935,933,97,121,102,53,3])).
% 78.03/78.04 cnf(976,plain,
% 78.03/78.04 (~P8(f14(a1,a17),a1)),
% 78.03/78.04 inference(scs_inference,[],[80,209,759,769,935,933,97,121,102,53,3,103])).
% 78.03/78.04 cnf(984,plain,
% 78.03/78.04 (~P6(a23,a20)),
% 78.03/78.04 inference(scs_inference,[],[807,121])).
% 78.03/78.04 cnf(989,plain,
% 78.03/78.04 (~P8(a23,a18)),
% 78.03/78.04 inference(scs_inference,[],[79,782,807,566,121,97,3,107])).
% 78.03/78.04 cnf(1003,plain,
% 78.03/78.04 (~E(f14(a17,a17),a17)),
% 78.03/78.04 inference(scs_inference,[],[784,97])).
% 78.03/78.04 cnf(1005,plain,
% 78.03/78.04 (~P6(a24,a23)),
% 78.03/78.04 inference(scs_inference,[],[784,245,97,121])).
% 78.03/78.04 cnf(1012,plain,
% 78.03/78.04 (~P8(a24,a22)),
% 78.03/78.04 inference(scs_inference,[],[75,209,784,245,950,920,97,121,102,53,3,110])).
% 78.03/78.04 cnf(1020,plain,
% 78.03/78.04 (~P6(f14(a17,a16),a16)),
% 78.03/78.04 inference(scs_inference,[],[830,121])).
% 78.03/78.04 cnf(1022,plain,
% 78.03/78.04 (~E(f14(a1,a17),a15)),
% 78.03/78.04 inference(scs_inference,[],[769,830,121,97])).
% 78.03/78.04 cnf(1027,plain,
% 78.03/78.04 (~P8(f14(a17,a16),a17)),
% 78.03/78.04 inference(scs_inference,[],[77,769,830,969,466,121,97,102,3,104])).
% 78.03/78.04 cnf(1040,plain,
% 78.03/78.04 (~E(a23,a20)),
% 78.03/78.04 inference(scs_inference,[],[807,97])).
% 78.03/78.04 cnf(1042,plain,
% 78.03/78.05 (~P6(f14(a15,a16),a15)),
% 78.03/78.05 inference(scs_inference,[],[807,849,97,121])).
% 78.03/78.05 cnf(1044,plain,
% 78.03/78.05 (P6(a20,a23)),
% 78.03/78.05 inference(scs_inference,[],[807,849,984,97,121,102])).
% 78.03/78.05 cnf(1061,plain,
% 78.03/78.05 (~P6(a22,a16)),
% 78.03/78.05 inference(scs_inference,[],[868,121])).
% 78.03/78.05 cnf(1063,plain,
% 78.03/78.05 (~E(f14(a17,a16),a16)),
% 78.03/78.05 inference(scs_inference,[],[830,868,121,97])).
% 78.03/78.05 cnf(1067,plain,
% 78.03/78.05 (~E(a19,f14(a1,a15))),
% 78.03/78.05 inference(scs_inference,[],[72,830,868,1020,967,121,97,102,3])).
% 78.03/78.05 cnf(1068,plain,
% 78.03/78.05 (~P8(a22,a17)),
% 78.03/78.05 inference(scs_inference,[],[72,830,868,1020,967,121,97,102,3,104])).
% 78.03/78.05 cnf(1079,plain,
% 78.03/78.05 (~E(f14(a15,a16),a15)),
% 78.03/78.05 inference(scs_inference,[],[849,97])).
% 78.03/78.05 cnf(1086,plain,
% 78.03/78.05 (~P8(f14(a15,a17),a1)),
% 78.03/78.05 inference(scs_inference,[],[74,849,888,1042,952,97,121,102,3,103])).
% 78.03/78.05 cnf(1094,plain,
% 78.03/78.05 (~P6(f14(a16,a16),a16)),
% 78.03/78.05 inference(scs_inference,[],[908,121])).
% 78.03/78.05 cnf(1100,plain,
% 78.03/78.05 (~E(a23,a24)),
% 78.03/78.05 inference(scs_inference,[],[209,245,908,1005,121,97,102,53])).
% 78.03/78.05 cnf(1103,plain,
% 78.03/78.05 (~P8(f14(a16,a16),a17)),
% 78.03/78.05 inference(scs_inference,[],[78,209,245,908,1005,973,121,97,102,53,3,104])).
% 78.03/78.05 cnf(1111,plain,
% 78.03/78.05 (~E(a22,a16)),
% 78.03/78.05 inference(scs_inference,[],[868,97])).
% 78.03/78.05 cnf(1113,plain,
% 78.03/78.05 (~P6(f14(a1,a16),a15)),
% 78.03/78.05 inference(scs_inference,[],[868,925,97,121])).
% 78.03/78.05 cnf(1115,plain,
% 78.03/78.05 (P6(a16,a22)),
% 78.03/78.05 inference(scs_inference,[],[868,925,1061,97,121,102])).
% 78.03/78.05 cnf(1120,plain,
% 78.03/78.05 (~P8(f14(a1,a16),a1)),
% 78.03/78.05 inference(scs_inference,[],[76,209,868,925,1061,399,97,121,102,53,3,103])).
% 78.03/78.05 cnf(1125,plain,
% 78.03/78.05 (~P6(f14(a17,a17),a15)),
% 78.03/78.05 inference(scs_inference,[],[957,121])).
% 78.03/78.05 cnf(1127,plain,
% 78.03/78.05 (~E(f14(a15,a17),a15)),
% 78.03/78.05 inference(scs_inference,[],[888,957,121,97])).
% 78.03/78.05 cnf(1137,plain,
% 78.03/78.05 (~E(f14(a16,a16),a16)),
% 78.03/78.05 inference(scs_inference,[],[908,97])).
% 78.03/78.05 cnf(1139,plain,
% 78.03/78.05 (~P6(a23,a18)),
% 78.03/78.05 inference(scs_inference,[],[908,989,97,121])).
% 78.03/78.05 cnf(1144,plain,
% 78.03/78.05 (~P8(a23,a16)),
% 78.03/78.05 inference(scs_inference,[],[75,908,989,1003,1094,97,121,102,3,106])).
% 78.03/78.05 cnf(1149,plain,
% 78.03/78.05 (~P6(a24,a22)),
% 78.03/78.05 inference(scs_inference,[],[1012,121])).
% 78.03/78.05 cnf(1155,plain,
% 78.03/78.05 (~E(f14(a17,a16),f14(a15,a17))),
% 78.03/78.05 inference(scs_inference,[],[77,925,1012,1063,1113,121,97,102,3])).
% 78.03/78.05 cnf(1156,plain,
% 78.03/78.05 (~P8(a24,a19)),
% 78.03/78.05 inference(scs_inference,[],[77,925,1012,1063,1113,121,97,102,3,109])).
% 78.03/78.05 cnf(1163,plain,
% 78.03/78.05 (~P6(f14(a17,a16),a17)),
% 78.03/78.05 inference(scs_inference,[],[957,1027,97,121])).
% 78.03/78.05 cnf(1170,plain,
% 78.03/78.05 (~P8(f14(a17,a16),a15)),
% 78.03/78.05 inference(scs_inference,[],[80,209,957,1027,1125,899,97,121,102,53,3,105])).
% 78.03/78.05 cnf(1175,plain,
% 78.03/78.05 (~P6(a22,a17)),
% 78.03/78.05 inference(scs_inference,[],[1068,121])).
% 78.03/78.05 cnf(1180,plain,
% 78.03/78.05 (~P8(a22,a15)),
% 78.03/78.05 inference(scs_inference,[],[73,976,1068,1111,121,97,3,105])).
% 78.03/78.05 cnf(1194,plain,
% 78.03/78.05 (~E(a23,a18)),
% 78.03/78.05 inference(scs_inference,[],[989,97])).
% 78.03/78.05 cnf(1196,plain,
% 78.03/78.05 (~P6(f14(a16,a16),a17)),
% 78.03/78.05 inference(scs_inference,[],[989,1103,97,121])).
% 78.03/78.05 cnf(1198,plain,
% 78.03/78.05 (P6(a18,a23)),
% 78.03/78.05 inference(scs_inference,[],[989,1103,1139,97,121,102])).
% 78.03/78.05 cnf(1203,plain,
% 78.03/78.05 (~P8(f14(a16,a16),a15)),
% 78.03/78.05 inference(scs_inference,[],[72,209,989,1103,1139,1022,97,121,102,53,3,105])).
% 78.03/78.05 cnf(1208,plain,
% 78.03/78.05 (~P6(a23,a16)),
% 78.03/78.05 inference(scs_inference,[],[1144,121])).
% 78.03/78.05 cnf(1212,plain,
% 78.03/78.05 (P6(a22,a24)),
% 78.03/78.05 inference(scs_inference,[],[1012,1149,1144,121,97,102])).
% 78.03/78.05 cnf(1214,plain,
% 78.03/78.05 (~E(a22,a24)),
% 78.03/78.05 inference(scs_inference,[],[209,1012,1149,1144,121,97,102,53])).
% 78.03/78.05 cnf(1217,plain,
% 78.03/78.05 (~P8(a23,a17)),
% 78.03/78.05 inference(scs_inference,[],[74,209,1012,1149,1144,539,121,97,102,53,3,104])).
% 78.03/78.05 cnf(1222,plain,
% 78.03/78.05 (~E(f14(a17,a16),a17)),
% 78.03/78.05 inference(scs_inference,[],[1027,97])).
% 78.03/78.05 cnf(1224,plain,
% 78.03/78.05 (~P6(a24,a19)),
% 78.03/78.05 inference(scs_inference,[],[1027,1156,97,121])).
% 78.03/78.05 cnf(1229,plain,
% 78.03/78.05 (~P8(a24,a20)),
% 78.03/78.05 inference(scs_inference,[],[76,1027,1156,1163,1194,97,121,102,3,108])).
% 78.03/78.05 cnf(1234,plain,
% 78.03/78.05 (~P6(f14(a17,a16),a15)),
% 78.03/78.05 inference(scs_inference,[],[1170,121])).
% 78.03/78.05 cnf(1236,plain,
% 78.03/78.05 (~E(a22,a17)),
% 78.03/78.05 inference(scs_inference,[],[1068,1170,121,97])).
% 78.03/78.05 cnf(1238,plain,
% 78.03/78.05 (P6(a17,a22)),
% 78.03/78.05 inference(scs_inference,[],[1068,1170,1175,121,97,102])).
% 78.03/78.05 cnf(1243,plain,
% 78.03/78.05 (~P8(f14(a17,a16),a1)),
% 78.03/78.05 inference(scs_inference,[],[78,209,1068,1170,1175,800,121,97,102,53,3,103])).
% 78.03/78.05 cnf(1250,plain,
% 78.03/78.05 (~P6(a22,a15)),
% 78.03/78.05 inference(scs_inference,[],[1086,1180,97,121])).
% 78.03/78.05 cnf(1252,plain,
% 78.03/78.05 (~E(a23,f14(a17,a16))),
% 78.03/78.05 inference(scs_inference,[],[79,1086,1040,1180,97,121,3])).
% 78.03/78.05 cnf(1253,plain,
% 78.03/78.05 (~P8(a22,a1)),
% 78.03/78.05 inference(scs_inference,[],[79,1086,1040,1180,97,121,3,103])).
% 78.03/78.05 cnf(1266,plain,
% 78.03/78.05 (~P6(f14(a16,a16),a15)),
% 78.03/78.05 inference(scs_inference,[],[1203,121])).
% 78.03/78.05 cnf(1271,plain,
% 78.03/78.05 (~P8(f14(a16,a16),a1)),
% 78.03/78.05 inference(scs_inference,[],[75,1120,1203,1222,121,97,3,103])).
% 78.03/78.05 cnf(1285,plain,
% 78.03/78.05 (~E(f14(a16,a16),a17)),
% 78.03/78.05 inference(scs_inference,[],[1103,97])).
% 78.03/78.05 cnf(1287,plain,
% 78.03/78.05 (~P6(a23,a17)),
% 78.03/78.05 inference(scs_inference,[],[1103,1217,97,121])).
% 78.03/78.05 cnf(1292,plain,
% 78.03/78.05 (~P8(a23,a15)),
% 78.03/78.05 inference(scs_inference,[],[73,1103,1217,1196,1137,97,121,102,3,105])).
% 78.03/78.05 cnf(1297,plain,
% 78.03/78.05 (~P6(a24,a20)),
% 78.03/78.05 inference(scs_inference,[],[1229,121])).
% 78.03/78.05 cnf(1299,plain,
% 78.03/78.05 (~E(a23,a16)),
% 78.03/78.05 inference(scs_inference,[],[1144,1229,121,97])).
% 78.03/78.05 cnf(1301,plain,
% 78.03/78.05 (P6(a16,a23)),
% 78.03/78.05 inference(scs_inference,[],[1144,1229,1208,121,97,102])).
% 78.03/78.05 cnf(1306,plain,
% 78.03/78.05 (~P8(a24,a18)),
% 78.03/78.05 inference(scs_inference,[],[72,209,1144,1229,1208,1079,121,97,102,53,3,107])).
% 78.03/78.05 cnf(1313,plain,
% 78.03/78.05 (~P6(a23,a15)),
% 78.03/78.05 inference(scs_inference,[],[1156,1292,97,121])).
% 78.03/78.05 cnf(1315,plain,
% 78.03/78.05 (P6(a19,a24)),
% 78.03/78.05 inference(scs_inference,[],[1156,1224,1292,97,121,102])).
% 78.03/78.05 cnf(1317,plain,
% 78.03/78.05 (~E(a19,a24)),
% 78.03/78.05 inference(scs_inference,[],[209,1156,1224,1292,97,121,102,53])).
% 78.03/78.05 cnf(1320,plain,
% 78.03/78.05 (~P8(a23,a1)),
% 78.03/78.05 inference(scs_inference,[],[74,209,1156,1224,1236,1292,97,121,102,53,3,103])).
% 78.03/78.05 cnf(1325,plain,
% 78.03/78.05 (~P6(a24,a18)),
% 78.03/78.05 inference(scs_inference,[],[1306,121])).
% 78.03/78.05 cnf(1332,plain,
% 78.03/78.05 (~P8(a24,a16)),
% 78.03/78.05 inference(scs_inference,[],[77,1170,1234,1299,1306,121,97,102,3,106])).
% 78.03/78.05 cnf(1339,plain,
% 78.03/78.05 (~P6(a24,a16)),
% 78.03/78.05 inference(scs_inference,[],[1180,1332,97,121])).
% 78.03/78.05 cnf(1341,plain,
% 78.03/78.05 (P6(a15,a22)),
% 78.03/78.05 inference(scs_inference,[],[1180,1250,1332,97,121,102])).
% 78.03/78.05 cnf(1345,plain,
% 78.03/78.05 (~E(f14(a15,a17),f14(a1,a15))),
% 78.03/78.05 inference(scs_inference,[],[72,209,1180,1127,1250,1332,97,121,102,53,3])).
% 78.03/78.05 cnf(1346,plain,
% 78.03/78.05 (~P8(a24,a17)),
% 78.03/78.05 inference(scs_inference,[],[72,209,1180,1127,1250,1332,97,121,102,53,3,104])).
% 78.03/78.05 cnf(1351,plain,
% 78.03/78.05 (~P6(a24,a17)),
% 78.03/78.05 inference(scs_inference,[],[1346,121])).
% 78.03/78.05 cnf(1358,plain,
% 78.03/78.05 (~P8(a24,a15)),
% 78.03/78.05 inference(scs_inference,[],[73,1203,1266,1346,773,121,97,102,3,105])).
% 78.03/78.05 cnf(1365,plain,
% 78.03/78.05 (~P6(a24,a15)),
% 78.03/78.05 inference(scs_inference,[],[1217,1358,97,121])).
% 78.03/78.05 cnf(1367,plain,
% 78.03/78.05 (P6(a17,a23)),
% 78.03/78.05 inference(scs_inference,[],[1217,1287,1358,97,121,102])).
% 78.03/78.05 cnf(1372,plain,
% 78.03/78.05 (~P8(a24,a1)),
% 78.03/78.05 inference(scs_inference,[],[74,209,1217,1285,1287,1358,97,121,102,53,3,103])).
% 78.03/78.05 cnf(1379,plain,
% 78.03/78.05 (P6(a20,a24)),
% 78.03/78.05 inference(scs_inference,[],[1229,1297,97,102])).
% 78.03/78.05 cnf(1381,plain,
% 78.03/78.05 (~E(a20,a24)),
% 78.03/78.05 inference(scs_inference,[],[209,1229,1297,97,102,53])).
% 78.03/78.05 cnf(1388,plain,
% 78.03/78.05 (~E(a24,a1)),
% 78.03/78.05 inference(scs_inference,[],[1372,97])).
% 78.03/78.05 cnf(1405,plain,
% 78.03/78.05 (P6(a15,a23)),
% 78.03/78.05 inference(scs_inference,[],[1292,1313,97,102])).
% 78.03/78.05 cnf(1416,plain,
% 78.03/78.05 (P6(a18,a24)),
% 78.03/78.05 inference(scs_inference,[],[1306,1325,97,102])).
% 78.03/78.05 cnf(1418,plain,
% 78.03/78.05 (~E(a18,a24)),
% 78.03/78.05 inference(scs_inference,[],[209,1306,1325,97,102,53])).
% 78.03/78.05 cnf(1427,plain,
% 78.03/78.05 (P6(a16,a24)),
% 78.03/78.05 inference(scs_inference,[],[1332,1339,97,102])).
% 78.03/78.05 cnf(1438,plain,
% 78.03/78.05 (P6(a17,a24)),
% 78.03/78.05 inference(scs_inference,[],[1346,1351,97,102])).
% 78.03/78.05 cnf(1451,plain,
% 78.03/78.05 (~E(a15,a24)),
% 78.03/78.05 inference(scs_inference,[],[209,1358,1365,97,102,53])).
% 78.03/78.05 cnf(1523,plain,
% 78.03/78.05 (~E(f14(a1,a16),f14(a15,a15))),
% 78.03/78.05 inference(scs_inference,[],[75,952,3])).
% 78.03/78.05 cnf(1528,plain,
% 78.03/78.05 (~E(a1,f14(a15,a17))),
% 78.03/78.05 inference(scs_inference,[],[77,275,3])).
% 78.03/78.05 cnf(1821,plain,
% 78.03/78.05 (E(f25(a1),f25(f14(a1,a1)))),
% 78.03/78.05 inference(scs_inference,[],[71,6,2])).
% 78.03/78.05 cnf(1822,plain,
% 78.03/78.05 (P2(f25(f14(a1,a1)),f14(a1,a1))),
% 78.03/78.05 inference(scs_inference,[],[1821,292])).
% 78.03/78.05 cnf(1825,plain,
% 78.03/78.05 (E(f25(f14(a1,a1)),f25(a1))),
% 78.03/78.05 inference(scs_inference,[],[1821,292,101,2])).
% 78.03/78.05 cnf(1827,plain,
% 78.03/78.05 (P2(f25(f14(a1,a1)),a1)),
% 78.03/78.05 inference(scs_inference,[],[71,331,1821,292,101,2,44,38])).
% 78.03/78.05 cnf(4237,plain,
% 78.03/78.05 (E(f6(a16,x42371,x42372),f6(f14(a1,a16),x42371,x42372))),
% 78.03/78.05 inference(scs_inference,[],[348,6,13,14,21,22,23,24,28,29,33,34,709,7])).
% 78.03/78.05 cnf(4238,plain,
% 78.03/78.05 (E(f6(x42381,a16,x42382),f6(x42381,f14(a1,a16),x42382))),
% 78.03/78.05 inference(scs_inference,[],[348,6,13,14,21,22,23,24,28,29,33,34,709,7,8])).
% 78.03/78.05 cnf(4274,plain,
% 78.03/78.05 (E(f14(x42741,a16),f14(x42741,f14(a1,a16)))),
% 78.03/78.05 inference(scs_inference,[],[279,1405,1416,1341,82,348,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5])).
% 78.03/78.05 cnf(4275,plain,
% 78.03/78.05 (E(f14(a16,x42751),f14(f14(a1,a16),x42751))),
% 78.03/78.05 inference(scs_inference,[],[279,1405,1416,1341,82,348,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4])).
% 78.03/78.05 cnf(4286,plain,
% 78.03/78.05 (~E(a1,a20)),
% 78.03/78.05 inference(scs_inference,[],[279,475,1405,1416,1341,971,563,523,1825,404,82,348,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4,116,117,114,115,97,2])).
% 78.03/78.05 cnf(4288,plain,
% 78.03/78.05 (P8(x42881,x42881)),
% 78.03/78.05 inference(rename_variables,[],[208])).
% 78.03/78.05 cnf(4295,plain,
% 78.03/78.05 (~P2(f25(f14(a1,a16)),a1)),
% 78.03/78.05 inference(scs_inference,[],[267,279,475,250,253,357,1405,1416,1341,971,563,523,1825,404,82,348,208,71,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4,116,117,114,115,97,2,103,121,56,64,67,134])).
% 78.03/78.05 cnf(4297,plain,
% 78.03/78.05 (~P1(a2,f14(a1,a15))),
% 78.03/78.05 inference(scs_inference,[],[267,279,475,216,250,253,357,1405,1416,1341,971,563,523,1825,404,82,348,92,208,71,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4,116,117,114,115,97,2,103,121,56,64,67,134,155])).
% 78.03/78.05 cnf(4300,plain,
% 78.03/78.05 (~P6(a16,f14(a16,a1))),
% 78.03/78.05 inference(scs_inference,[],[267,279,475,216,250,253,219,357,1405,1416,1341,971,563,523,1825,404,82,348,92,208,71,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4,116,117,114,115,97,2,103,121,56,64,67,134,155,53])).
% 78.03/78.05 cnf(4301,plain,
% 78.03/78.05 (~P6(f14(x43011,x43012),f14(x43012,x43011))),
% 78.03/78.05 inference(rename_variables,[],[219])).
% 78.03/78.05 cnf(4302,plain,
% 78.03/78.05 (~E(a22,f14(a1,a1))),
% 78.03/78.05 inference(scs_inference,[],[267,279,475,589,216,250,253,219,357,1405,1416,1341,971,563,523,1825,404,82,348,92,208,71,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4,116,117,114,115,97,2,103,121,56,64,67,134,155,53,3])).
% 78.03/78.05 cnf(4303,plain,
% 78.03/78.05 (~P8(a23,f14(a1,a1))),
% 78.03/78.05 inference(scs_inference,[],[267,279,475,589,216,250,253,219,357,1320,1405,1416,1341,971,563,523,1825,404,82,348,92,208,71,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4,116,117,114,115,97,2,103,121,56,64,67,134,155,53,3,58])).
% 78.03/78.05 cnf(4307,plain,
% 78.03/78.05 (~P2(f25(a16),a1)),
% 78.03/78.05 inference(scs_inference,[],[267,279,358,475,589,216,250,253,219,357,1320,1405,1416,1341,971,563,523,1825,404,82,348,92,94,208,71,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4,116,117,114,115,97,2,103,121,56,64,67,134,155,53,3,58,102,37])).
% 78.03/78.05 cnf(4310,plain,
% 78.03/78.05 (~P6(f14(a16,a1),a16)),
% 78.03/78.05 inference(scs_inference,[],[267,279,358,475,589,216,250,253,219,4301,357,1320,1405,1416,1341,971,563,523,1825,404,90,95,82,348,92,94,208,71,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4,116,117,114,115,97,2,103,121,56,64,67,134,155,53,3,58,102,37,36,38,54])).
% 78.03/78.05 cnf(4312,plain,
% 78.03/78.05 (~E(a1,a23)),
% 78.03/78.05 inference(scs_inference,[],[267,279,358,475,589,216,250,253,219,4301,357,1320,1405,1416,1341,971,563,523,1825,404,90,95,82,348,92,94,208,4288,71,6,13,14,21,22,23,24,28,29,33,34,709,7,8,9,10,11,12,15,16,17,18,19,20,25,26,27,30,31,32,211,600,623,708,890,891,624,625,710,910,120,119,96,118,5,4,116,117,114,115,97,2,103,121,56,64,67,134,155,53,3,58,102,37,36,38,54,57])).
% 78.03/78.06 cnf(4329,plain,
% 78.03/78.06 (P13(a2,f14(a1,a1),f25(f14(a1,x43291)),x43291)),
% 78.03/78.06 inference(scs_inference,[],[387,1238,264,273,118,96,115,211])).
% 78.03/78.06 cnf(4333,plain,
% 78.03/78.06 (E(f25(a17),f25(f14(a1,a17)))),
% 78.03/78.06 inference(scs_inference,[],[387,1238,496,264,376,273,118,96,115,211,116,6])).
% 78.03/78.06 cnf(4344,plain,
% 78.03/78.06 (E(f14(x43441,a17),f14(x43441,f14(a1,a17)))),
% 78.03/78.06 inference(scs_inference,[],[387,4237,1301,1238,496,452,264,376,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5])).
% 78.03/78.06 cnf(4359,plain,
% 78.03/78.06 (E(f6(x43591,a17,x43592),f6(x43591,f14(a1,a17),x43592))),
% 78.03/78.06 inference(scs_inference,[],[387,4237,1427,1301,1238,777,496,452,264,376,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8])).
% 78.03/78.06 cnf(4371,plain,
% 78.03/78.06 (E(f14(a17,x43711),f14(f14(a1,a17),x43711))),
% 78.03/78.06 inference(scs_inference,[],[387,4237,1427,1301,1238,777,496,452,264,376,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4])).
% 78.03/78.06 cnf(4372,plain,
% 78.03/78.06 (~E(a1,a19)),
% 78.03/78.06 inference(scs_inference,[],[387,498,4237,1427,1301,1238,777,496,452,264,376,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2])).
% 78.03/78.06 cnf(4377,plain,
% 78.03/78.06 (~P1(a2,f14(f14(a1,a15),a15))),
% 78.03/78.06 inference(scs_inference,[],[387,498,4297,4237,1427,1301,1238,777,496,452,216,264,376,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155])).
% 78.03/78.06 cnf(4380,plain,
% 78.03/78.06 (~P2(f25(a18),a1)),
% 78.03/78.06 inference(scs_inference,[],[387,498,4297,4237,1427,1301,1238,777,496,452,216,264,376,82,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155,134])).
% 78.03/78.06 cnf(4383,plain,
% 78.03/78.06 (E(f6(a16,x43831,x43832),f6(f14(a1,a16),x43831,x43832))),
% 78.03/78.06 inference(rename_variables,[],[4237])).
% 78.03/78.06 cnf(4384,plain,
% 78.03/78.06 (E(f6(x43841,a16,x43842),f6(x43841,f14(a1,a16),x43842))),
% 78.03/78.06 inference(rename_variables,[],[4238])).
% 78.03/78.06 cnf(4385,plain,
% 78.03/78.06 (E(f14(a16,a1),a16)),
% 78.03/78.06 inference(scs_inference,[],[387,498,4297,4300,4310,4237,4238,1427,1301,1238,777,496,452,216,264,376,82,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155,134,3,102])).
% 78.03/78.06 cnf(4387,plain,
% 78.03/78.06 (P8(f6(x43871,a16,x43872),f6(x43871,f14(a1,a16),x43872))),
% 78.03/78.06 inference(scs_inference,[],[387,498,4297,4300,4310,4237,4238,4384,1427,1301,1238,777,496,452,216,264,376,82,208,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155,134,3,102,58])).
% 78.03/78.06 cnf(4388,plain,
% 78.03/78.06 (P8(x43881,x43881)),
% 78.03/78.06 inference(rename_variables,[],[208])).
% 78.03/78.06 cnf(4389,plain,
% 78.03/78.06 (~P6(f14(x43891,a16),f14(f14(a1,a16),x43891))),
% 78.03/78.06 inference(scs_inference,[],[387,498,4297,4300,4310,4237,4238,4384,4274,1427,1301,1238,777,496,452,216,219,264,376,82,208,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155,134,3,102,58,53])).
% 78.03/78.06 cnf(4392,plain,
% 78.03/78.06 (P1(a2,f14(a15,a17))),
% 78.03/78.06 inference(scs_inference,[],[81,387,498,4297,4300,4310,4237,4238,4384,4274,1427,1301,1238,777,496,452,216,219,264,376,82,451,208,273,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155,134,3,102,58,53,36])).
% 78.03/78.06 cnf(4393,plain,
% 78.03/78.06 (~P2(f25(a16),f14(a1,a1))),
% 78.03/78.06 inference(scs_inference,[],[81,387,498,4297,4300,4310,4307,4237,4238,4384,4274,1427,1301,1238,777,496,452,216,219,264,376,82,451,208,273,71,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155,134,3,102,58,53,36,38])).
% 78.03/78.06 cnf(4394,plain,
% 78.03/78.06 (P8(f6(f14(a1,a16),x43941,x43942),f6(a16,x43941,x43942))),
% 78.03/78.06 inference(scs_inference,[],[81,387,498,4297,4300,4310,4307,4237,4383,4238,4384,4274,1427,1301,1238,777,496,452,216,219,264,376,82,451,208,4388,273,71,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155,134,3,102,58,53,36,38,57])).
% 78.03/78.06 cnf(4396,plain,
% 78.03/78.06 (~P6(f6(f14(a1,a16),x43961,x43962),f6(a16,x43961,x43962))),
% 78.03/78.06 inference(scs_inference,[],[81,387,498,4297,4300,4310,4307,4237,4383,4238,4384,4274,1427,1301,1238,777,496,452,216,219,264,376,82,451,208,4388,273,71,209,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155,134,3,102,58,53,36,38,57,54])).
% 78.03/78.06 cnf(4404,plain,
% 78.03/78.06 (~E(f25(a1),f25(a16))),
% 78.03/78.06 inference(scs_inference,[],[81,387,498,4297,4300,4310,4307,4237,4383,4238,4384,4274,1427,1301,1238,777,496,452,216,219,264,376,82,451,208,4388,273,71,209,118,96,115,211,116,6,28,23,7,114,97,20,119,5,117,22,29,30,13,120,19,34,18,21,25,10,8,33,24,31,9,14,26,11,16,15,32,17,4,2,12,27,121,155,134,3,102,58,53,36,38,57,54,735,809,810,786,787,852,292])).
% 78.03/78.06 cnf(4422,plain,
% 78.03/78.06 (E(f9(x44221,x44222,f14(a16,a1)),f9(x44221,x44222,a16))),
% 78.03/78.06 inference(scs_inference,[],[616,4385,1367,1115,668,118,96,119,116,6,97,23,20])).
% 78.03/78.06 cnf(4430,plain,
% 78.03/78.06 (E(f14(x44301,f14(a16,a1)),f14(x44301,a16))),
% 78.03/78.06 inference(scs_inference,[],[616,4385,1438,1367,1115,543,668,118,96,119,116,6,97,23,20,117,7,120,28,21,5])).
% 78.03/78.06 cnf(4431,plain,
% 78.03/78.06 (E(f8(x44311,x44312,f14(a16,a1)),f8(x44311,x44312,a16))),
% 78.03/78.06 inference(scs_inference,[],[616,4385,1438,1367,1115,543,668,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32])).
% 78.03/78.06 cnf(4435,plain,
% 78.03/78.06 (E(f9(f14(a16,a1),x44351,x44352),f9(a16,x44351,x44352))),
% 78.03/78.06 inference(scs_inference,[],[616,4385,1438,1367,1115,543,668,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18])).
% 78.03/78.06 cnf(4439,plain,
% 78.03/78.06 (E(f6(x44391,x44392,f14(a16,a1)),f6(x44391,x44392,a16))),
% 78.03/78.06 inference(scs_inference,[],[616,4385,1438,1367,1115,543,668,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9])).
% 78.03/78.06 cnf(4448,plain,
% 78.03/78.06 (E(f14(f14(a16,a1),x44481),f14(a16,x44481))),
% 78.03/78.06 inference(scs_inference,[],[616,272,4385,1438,1367,1115,543,668,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4])).
% 78.03/78.06 cnf(4456,plain,
% 78.03/78.06 (P6(f14(a16,a1),a18)),
% 78.03/78.06 inference(scs_inference,[],[616,272,4385,1438,1367,1115,543,668,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106])).
% 78.03/78.06 cnf(4458,plain,
% 78.03/78.06 (~E(a18,f14(a16,a1))),
% 78.03/78.06 inference(scs_inference,[],[616,272,4385,1438,1367,1115,543,668,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101])).
% 78.03/78.06 cnf(4462,plain,
% 78.03/78.06 (~P1(a27,f14(a1,a15))),
% 78.03/78.06 inference(scs_inference,[],[616,315,272,4385,1438,1367,1115,543,668,93,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155])).
% 78.03/78.06 cnf(4465,plain,
% 78.03/78.06 (~P2(f25(a20),a1)),
% 78.03/78.06 inference(scs_inference,[],[616,315,4286,272,4385,1438,1367,1115,543,668,93,82,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155,134])).
% 78.03/78.06 cnf(4467,plain,
% 78.03/78.06 (P6(a1,a20)),
% 78.03/78.06 inference(scs_inference,[],[616,315,4286,272,4385,1438,1367,1115,543,668,93,82,94,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155,134,102])).
% 78.03/78.06 cnf(4471,plain,
% 78.03/78.06 (~P2(f25(f14(a16,a1)),f14(a1,a1))),
% 78.03/78.06 inference(scs_inference,[],[616,315,4286,272,4393,4385,1438,1367,1115,543,668,93,82,472,94,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155,134,102,3,37])).
% 78.03/78.06 cnf(4472,plain,
% 78.03/78.06 (~P8(f14(a16,a16),f14(a1,a1))),
% 78.03/78.06 inference(scs_inference,[],[616,315,4286,272,4393,4385,1271,1438,1367,1115,543,668,93,82,472,94,71,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155,134,102,3,37,58])).
% 78.03/78.06 cnf(4473,plain,
% 78.03/78.06 (~P6(f14(a17,a16),f14(f14(a1,a16),f14(a1,a17)))),
% 78.03/78.06 inference(scs_inference,[],[616,315,4286,272,4393,4385,4371,4389,1271,1438,1367,1115,543,668,93,82,472,94,71,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155,134,102,3,37,58,53])).
% 78.03/78.06 cnf(4478,plain,
% 78.03/78.06 (~P2(f25(a18),f14(a1,a1))),
% 78.03/78.06 inference(scs_inference,[],[616,315,4286,272,4393,4385,4380,4371,4389,4377,1271,1438,1367,1115,543,668,93,82,472,83,94,71,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155,134,102,3,37,58,53,36,38])).
% 78.03/78.06 cnf(4479,plain,
% 78.03/78.06 (~E(f14(a1,a1),a23)),
% 78.03/78.06 inference(scs_inference,[],[616,315,4286,272,4393,4385,4303,4380,4371,4389,4377,1271,1438,1367,1115,543,668,93,82,472,83,94,208,71,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155,134,102,3,37,58,53,36,38,57])).
% 78.03/78.06 cnf(4481,plain,
% 78.03/78.06 (~P6(f6(f14(a1,a16),f14(a1,a17),x44811),f6(a16,a17,x44811))),
% 78.03/78.06 inference(scs_inference,[],[616,315,4286,272,4393,4385,4303,4380,4396,4359,4371,4389,4377,1271,1438,1367,1115,543,668,93,82,472,83,94,208,71,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155,134,102,3,37,58,53,36,38,57,54])).
% 78.03/78.06 cnf(4484,plain,
% 78.03/78.06 (~P6(a18,f14(a16,a1))),
% 78.03/78.06 inference(scs_inference,[],[616,315,4286,272,4393,4385,4303,4380,4396,4359,4371,4389,4377,1271,1438,1367,1115,543,668,93,82,472,83,94,208,71,118,96,119,116,6,97,23,20,117,7,120,28,21,5,32,16,22,26,18,34,25,33,9,15,29,13,10,2,24,19,17,4,14,30,31,8,11,27,12,106,101,121,155,134,102,3,37,58,53,36,38,57,54,127])).
% 78.03/78.06 cnf(4500,plain,
% 78.03/78.06 (P8(a1,a18)),
% 78.03/78.06 inference(scs_inference,[],[670,4467,4422,903,118,96,97,116])).
% 78.03/78.06 cnf(4515,plain,
% 78.03/78.06 (E(f14(x45151,a18),f14(x45151,f14(a17,a17)))),
% 78.03/78.06 inference(scs_inference,[],[670,4467,4422,1315,1198,903,614,495,118,96,97,116,119,117,20,6,120,23,28,21,7,16,5])).
% 78.03/78.06 cnf(4543,plain,
% 78.03/78.06 (~P1(a27,f14(f14(a1,a15),a15))),
% 78.03/78.06 inference(scs_inference,[],[670,4467,757,4478,4462,4422,1315,1198,903,315,614,495,118,96,97,116,119,117,20,6,120,23,28,21,7,16,5,15,33,31,32,14,9,22,29,2,34,18,11,17,25,24,26,13,8,4,19,10,27,30,292,12,121,155])).
% 78.03/78.06 cnf(4546,plain,
% 78.03/78.06 (~P2(f25(a23),a1)),
% 78.03/78.06 inference(scs_inference,[],[670,4312,4467,757,4478,4462,4422,1315,1198,903,315,614,495,82,118,96,97,116,119,117,20,6,120,23,28,21,7,16,5,15,33,31,32,14,9,22,29,2,34,18,11,17,25,24,26,13,8,4,19,10,27,30,292,12,121,155,134])).
% 78.03/78.06 cnf(4548,plain,
% 78.03/78.06 (~P8(a18,f14(a16,a1))),
% 78.03/78.06 inference(scs_inference,[],[670,4312,4467,757,4478,4458,4462,4484,4422,1315,1198,903,315,614,495,82,118,96,97,116,119,117,20,6,120,23,28,21,7,16,5,15,33,31,32,14,9,22,29,2,34,18,11,17,25,24,26,13,8,4,19,10,27,30,292,12,121,155,134,124])).
% 78.03/78.06 cnf(4550,plain,
% 78.03/78.06 (E(a16,f14(a16,a1))),
% 78.03/78.06 inference(scs_inference,[],[670,4312,4467,757,4478,4458,4462,4484,4422,1315,1198,903,315,4300,4310,614,495,82,118,96,97,116,119,117,20,6,120,23,28,21,7,16,5,15,33,31,32,14,9,22,29,2,34,18,11,17,25,24,26,13,8,4,19,10,27,30,292,12,121,155,134,124,102])).
% 78.03/78.06 cnf(4554,plain,
% 78.03/78.06 (E(f9(x45541,x45542,f14(a16,a1)),f9(x45541,x45542,a16))),
% 78.03/78.06 inference(rename_variables,[],[4422])).
% 78.03/78.06 cnf(4557,plain,
% 78.03/78.06 (P8(x45571,x45571)),
% 78.03/78.06 inference(rename_variables,[],[208])).
% 78.03/78.06 cnf(4558,plain,
% 78.03/78.06 (~P6(f6(f14(a1,a16),f14(a1,a17),f14(a16,a1)),f6(a16,a17,a16))),
% 78.03/78.06 inference(scs_inference,[],[670,4312,4467,757,4478,4458,4462,4484,4422,4431,4435,4439,4481,1822,1315,1198,903,315,4300,4310,614,495,82,208,118,96,97,116,119,117,20,6,120,23,28,21,7,16,5,15,33,31,32,14,9,22,29,2,34,18,11,17,25,24,26,13,8,4,19,10,27,30,292,12,121,155,134,124,102,37,3,58,53])).
% 78.03/78.06 cnf(4563,plain,
% 78.03/78.06 (~P2(f25(a20),f14(a1,a1))),
% 78.03/78.06 inference(scs_inference,[],[670,4312,4467,757,4478,4392,4458,4462,4484,4465,4422,4431,4435,4439,4481,1822,4344,1315,1198,903,315,4300,4310,614,495,82,208,71,118,96,97,116,119,117,20,6,120,23,28,21,7,16,5,15,33,31,32,14,9,22,29,2,34,18,11,17,25,24,26,13,8,4,19,10,27,30,292,12,121,155,134,124,102,37,3,58,53,36,38])).
% 78.03/78.06 cnf(4566,plain,
% 78.03/78.06 (~P6(f9(x45661,x45662,a16),f9(x45661,x45662,f14(a16,a1)))),
% 78.03/78.06 inference(scs_inference,[],[670,4312,4467,757,4478,4392,4458,4462,4484,4465,4422,4554,4431,4435,4439,4481,1822,4344,1315,1198,903,315,4300,4310,614,495,82,208,4557,209,71,118,96,97,116,119,117,20,6,120,23,28,21,7,16,5,15,33,31,32,14,9,22,29,2,34,18,11,17,25,24,26,13,8,4,19,10,27,30,292,12,121,155,134,124,102,37,3,58,53,36,38,57,54])).
% 78.03/78.06 cnf(4568,plain,
% 78.03/78.06 (P6(a1,a19)),
% 78.03/78.06 inference(scs_inference,[],[670,4312,4467,757,4478,4392,4458,4462,4484,4465,4422,4554,4431,4435,4439,4481,1822,4344,1315,1198,903,315,4300,4310,614,495,82,208,4557,209,71,118,96,97,116,119,117,20,6,120,23,28,21,7,16,5,15,33,31,32,14,9,22,29,2,34,18,11,17,25,24,26,13,8,4,19,10,27,30,292,12,121,155,134,124,102,37,3,58,53,36,38,57,54,108])).
% 78.03/78.06 cnf(4589,plain,
% 78.03/78.06 (E(f9(x45891,x45892,a16),f9(x45891,x45892,f14(a16,a1)))),
% 78.03/78.06 inference(scs_inference,[],[755,4550,1379,1044,725,118,96,119,97,120,6,21,20])).
% 78.03/78.06 cnf(4591,plain,
% 78.03/78.06 (E(f6(a16,x45911,x45912),f6(f14(a16,a1),x45911,x45912))),
% 78.03/78.06 inference(scs_inference,[],[755,4550,1379,1044,725,118,96,119,97,120,6,21,20,28,7])).
% 78.03/78.06 cnf(4593,plain,
% 78.03/78.06 (E(f7(a16,x45931,x45932),f7(f14(a16,a1),x45931,x45932))),
% 78.03/78.06 inference(scs_inference,[],[755,4550,1379,1044,725,118,96,119,97,120,6,21,20,28,7,23,15])).
% 78.03/78.06 cnf(4600,plain,
% 78.03/78.06 (E(f9(x46001,a16,x46002),f9(x46001,f14(a16,a1),x46002))),
% 78.03/78.06 inference(scs_inference,[],[755,1067,4550,1379,1044,725,118,96,119,97,120,6,21,20,28,7,23,15,16,2,5,22,29,8,19])).
% 78.03/78.06 cnf(4617,plain,
% 78.03/78.06 (~E(f25(a1),f25(a20))),
% 78.03/78.06 inference(scs_inference,[],[755,1067,4550,4563,1379,1044,725,118,96,119,97,120,6,21,20,28,7,23,15,16,2,5,22,29,8,19,34,17,33,32,14,26,9,27,25,18,31,13,10,24,12,11,292])).
% 78.03/78.06 cnf(4619,plain,
% 78.03/78.06 (E(f14(a16,x46191),f14(f14(a16,a1),x46191))),
% 78.03/78.06 inference(scs_inference,[],[755,1067,4550,4563,1379,1044,725,118,96,119,97,120,6,21,20,28,7,23,15,16,2,5,22,29,8,19,34,17,33,32,14,26,9,27,25,18,31,13,10,24,12,11,292,30,4])).
% 78.03/78.06 cnf(4625,plain,
% 78.03/78.06 (~P2(f25(a23),f14(a1,a1))),
% 78.03/78.06 inference(scs_inference,[],[755,4568,1067,4550,4563,4479,4515,1379,1044,1822,725,82,118,96,119,97,120,6,21,20,28,7,23,15,16,2,5,22,29,8,19,34,17,33,32,14,26,9,27,25,18,31,13,10,24,12,11,292,30,4,121,176,134])).
% 78.03/78.06 cnf(4629,plain,
% 78.03/78.06 (P6(a1,f14(a15,a17))),
% 78.03/78.06 inference(scs_inference,[],[755,4500,4568,1067,1528,4550,4563,4479,4515,1379,1044,591,1822,725,82,94,118,96,119,97,120,6,21,20,28,7,23,15,16,2,5,22,29,8,19,34,17,33,32,14,26,9,27,25,18,31,13,10,24,12,11,292,30,4,121,176,134,124,102])).
% 78.03/78.06 cnf(4635,plain,
% 78.03/78.06 (~P8(a22,f14(a1,a1))),
% 78.03/78.06 inference(scs_inference,[],[755,4500,4568,1067,1528,4550,4563,4479,4558,4515,1253,1379,1044,591,1822,4359,725,522,82,94,71,118,96,119,97,120,6,21,20,28,7,23,15,16,2,5,22,29,8,19,34,17,33,32,14,26,9,27,25,18,31,13,10,24,12,11,292,30,4,121,176,134,124,102,3,53,58])).
% 78.03/78.06 cnf(4638,plain,
% 78.03/78.06 (~P2(f25(f14(a1,a16)),f14(a1,a1))),
% 78.03/78.06 inference(scs_inference,[],[755,4500,4568,1067,1528,4550,4563,4479,4558,4515,4295,4543,1253,1379,1044,591,1822,4359,725,522,82,83,94,71,118,96,119,97,120,6,21,20,28,7,23,15,16,2,5,22,29,8,19,34,17,33,32,14,26,9,27,25,18,31,13,10,24,12,11,292,30,4,121,176,134,124,102,3,53,58,36,38])).
% 78.03/78.06 cnf(4641,plain,
% 78.03/78.06 (~P6(f14(a17,a16),f14(a16,f14(a1,a17)))),
% 78.03/78.06 inference(scs_inference,[],[755,4500,4568,1067,1528,4472,4550,4563,4479,4558,4473,4515,4295,4543,1253,4430,1379,4275,1044,591,1822,4359,725,522,82,83,94,71,118,96,119,97,120,6,21,20,28,7,23,15,16,2,5,22,29,8,19,34,17,33,32,14,26,9,27,25,18,31,13,10,24,12,11,292,30,4,121,176,134,124,102,3,53,58,36,38,57,54])).
% 78.03/78.06 cnf(4652,plain,
% 78.03/78.06 (P6(a1,a22)),
% 78.03/78.06 inference(scs_inference,[],[755,4500,4568,1067,1528,4472,4550,4563,4479,4558,4473,4515,4295,4543,1253,4430,1379,4275,1044,591,1822,4359,725,522,82,83,94,71,118,96,119,97,120,6,21,20,28,7,23,15,16,2,5,22,29,8,19,34,17,33,32,14,26,9,27,25,18,31,13,10,24,12,11,292,30,4,121,176,134,124,102,3,53,58,36,38,57,54,624,890,623,910,891,710,600,114,109])).
% 78.03/78.06 cnf(4670,plain,
% 78.03/78.06 (E(f6(a18,x46701,x46702),f6(f14(a15,a16),x46701,x46702))),
% 78.03/78.06 inference(scs_inference,[],[827,4591,1212,825,430,96,119,97,120,6,21,23,28,7])).
% 78.03/78.06 cnf(4681,plain,
% 78.03/78.06 (E(f9(a18,x46811,x46812),f9(f14(a15,a16),x46811,x46812))),
% 78.03/78.06 inference(scs_inference,[],[827,1345,4591,1212,825,430,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18])).
% 78.03/78.06 cnf(4695,plain,
% 78.03/78.06 (~E(f25(a1),f25(a23))),
% 78.03/78.06 inference(scs_inference,[],[827,1345,4625,4591,1212,825,430,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18,34,11,25,22,26,10,24,19,9,12,31,32,27,292])).
% 78.03/78.06 cnf(4701,plain,
% 78.03/78.06 (~P2(f25(a19),a1)),
% 78.03/78.06 inference(scs_inference,[],[827,4372,4652,1345,4625,4591,1212,825,430,82,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18,34,11,25,22,26,10,24,19,9,12,31,32,27,292,4,13,30,121,134])).
% 78.03/78.06 cnf(4706,plain,
% 78.03/78.06 (~P6(f9(x47061,a16,a16),f9(x47061,f14(a16,a1),f14(a16,a1)))),
% 78.03/78.06 inference(scs_inference,[],[827,4372,4652,1345,4625,4394,4566,4591,4600,1212,825,4396,430,82,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18,34,11,25,22,26,10,24,19,9,12,31,32,27,292,4,13,30,121,134,124,53])).
% 78.03/78.06 cnf(4707,plain,
% 78.03/78.06 (E(f9(x47071,a16,x47072),f9(x47071,f14(a16,a1),x47072))),
% 78.03/78.06 inference(rename_variables,[],[4600])).
% 78.03/78.06 cnf(4709,plain,
% 78.03/78.06 (E(f9(x47091,a16,a16),f9(x47091,f14(a16,a1),f14(a16,a1)))),
% 78.03/78.06 inference(scs_inference,[],[827,4372,4652,1345,4625,4394,4566,4589,4591,4600,4707,1212,825,4396,430,82,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18,34,11,25,22,26,10,24,19,9,12,31,32,27,292,4,13,30,121,134,124,53,3])).
% 78.03/78.06 cnf(4712,plain,
% 78.03/78.06 (P8(f7(a16,x47121,x47122),f7(f14(a16,a1),x47121,x47122))),
% 78.03/78.06 inference(scs_inference,[],[827,4372,4652,1345,4625,4394,4566,4589,4591,4593,4600,4707,1212,825,4396,430,82,208,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18,34,11,25,22,26,10,24,19,9,12,31,32,27,292,4,13,30,121,134,124,53,3,58])).
% 78.03/78.06 cnf(4713,plain,
% 78.03/78.06 (P8(x47131,x47131)),
% 78.03/78.06 inference(rename_variables,[],[208])).
% 78.03/78.06 cnf(4715,plain,
% 78.03/78.06 (P8(f7(f14(a16,a1),x47151,x47152),f7(a16,x47151,x47152))),
% 78.03/78.06 inference(scs_inference,[],[827,4372,4652,1345,4625,4394,4566,4589,4591,4593,4600,4707,1212,825,4396,4297,430,82,322,208,4713,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18,34,11,25,22,26,10,24,19,9,12,31,32,27,292,4,13,30,121,134,124,53,3,58,36,57])).
% 78.03/78.06 cnf(4717,plain,
% 78.03/78.06 (~P6(f6(f14(a16,a1),x47171,x47172),f6(a16,x47171,x47172))),
% 78.03/78.06 inference(scs_inference,[],[827,4372,4652,1345,4625,4394,4566,4589,4591,4593,4600,4707,1212,825,4396,4297,430,82,322,208,4713,209,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18,34,11,25,22,26,10,24,19,9,12,31,32,27,292,4,13,30,121,134,124,53,3,58,36,57,54])).
% 78.03/78.06 cnf(4719,plain,
% 78.03/78.06 (P6(a1,a23)),
% 78.03/78.06 inference(scs_inference,[],[827,4372,4652,1345,4625,4394,4566,4589,4591,4593,4600,4707,1212,825,4396,4297,430,82,322,208,4713,209,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18,34,11,25,22,26,10,24,19,9,12,31,32,27,292,4,13,30,121,134,124,53,3,58,36,57,54,110])).
% 78.03/78.06 cnf(4723,plain,
% 78.03/78.06 (~P1(a2,f14(a15,a15))),
% 78.03/78.06 inference(scs_inference,[],[827,4372,4652,1345,4625,4394,4566,4589,4591,4593,4600,4707,1212,825,4396,4297,216,430,82,322,208,4713,209,96,119,97,120,6,21,23,28,7,20,2,8,16,33,17,15,5,14,29,18,34,11,25,22,26,10,24,19,9,12,31,32,27,292,4,13,30,121,134,124,53,3,58,36,57,54,110,133,155])).
% 78.03/78.06 cnf(4732,plain,
% 78.03/78.06 (E(f6(a20,x47321,x47322),f6(f14(a17,a16),x47321,x47322))),
% 78.03/78.06 inference(scs_inference,[],[905,4670,522,96,97,6,7])).
% 78.03/78.06 cnf(4740,plain,
% 78.03/78.06 (E(f6(x47401,a20,x47402),f6(x47401,f14(a17,a16),x47402))),
% 78.03/78.06 inference(scs_inference,[],[905,1523,4670,522,96,97,6,7,23,21,20,28,2,33,16,8])).
% 78.03/78.06 cnf(4749,plain,
% 78.03/78.06 (E(f9(a20,x47491,x47492),f9(f14(a17,a16),x47491,x47492))),
% 78.03/78.06 inference(scs_inference,[],[905,1523,4670,522,96,97,6,7,23,21,20,28,2,33,16,8,14,17,11,34,5,15,22,26,18])).
% 78.03/78.06 cnf(4768,plain,
% 78.03/78.06 (P6(a1,f14(a1,a17))),
% 78.03/78.06 inference(scs_inference,[],[905,4719,1523,648,4638,4670,522,82,94,96,97,6,7,23,21,20,28,2,33,16,8,14,17,11,34,5,15,22,26,18,4,27,32,9,19,29,10,25,292,24,13,12,31,121,30,134,102])).
% 78.03/78.06 cnf(4773,plain,
% 78.03/78.06 (~P2(f25(a17),a1)),
% 78.03/78.06 inference(scs_inference,[],[905,4719,1523,648,4638,4670,4329,4333,522,82,94,96,97,6,7,23,21,20,28,2,33,16,8,14,17,11,34,5,15,22,26,18,4,27,32,9,19,29,10,25,292,24,13,12,31,121,30,134,102,45,37])).
% 78.03/78.06 cnf(4778,plain,
% 78.03/78.06 (~P8(a18,f14(f14(a16,a1),a1))),
% 78.03/78.06 inference(scs_inference,[],[905,4719,1523,4548,648,4638,4670,4681,4706,4329,4448,4333,522,82,94,495,96,97,6,7,23,21,20,28,2,33,16,8,14,17,11,34,5,15,22,26,18,4,27,32,9,19,29,10,25,292,24,13,12,31,121,30,134,102,45,37,53,3,58])).
% 78.03/78.06 cnf(4779,plain,
% 78.03/78.06 (E(f14(f14(a16,a1),x47791),f14(a16,x47791))),
% 78.03/78.06 inference(rename_variables,[],[4448])).
% 78.03/78.06 cnf(4780,plain,
% 78.03/78.06 (~P1(a2,a17)),
% 78.03/78.06 inference(scs_inference,[],[905,4719,1523,4548,4723,648,4638,4670,4681,4706,4329,4448,4333,522,403,82,94,495,96,97,6,7,23,21,20,28,2,33,16,8,14,17,11,34,5,15,22,26,18,4,27,32,9,19,29,10,25,292,24,13,12,31,121,30,134,102,45,37,53,3,58,36])).
% 78.03/78.06 cnf(4781,plain,
% 78.03/78.06 (~P8(f14(a15,a16),f14(a16,a1))),
% 78.03/78.06 inference(scs_inference,[],[905,4719,1523,4548,4723,648,4638,4670,4681,4706,4329,4448,4333,522,403,82,76,94,495,96,97,6,7,23,21,20,28,2,33,16,8,14,17,11,34,5,15,22,26,18,4,27,32,9,19,29,10,25,292,24,13,12,31,121,30,134,102,45,37,53,3,58,36,57])).
% 78.03/78.06 cnf(4784,plain,
% 78.03/78.06 (P6(a1,a24)),
% 78.03/78.06 inference(scs_inference,[],[905,4719,1523,4548,4723,648,4638,4670,4681,4706,4641,4329,4448,4779,4333,522,403,82,76,94,495,96,97,6,7,23,21,20,28,2,33,16,8,14,17,11,34,5,15,22,26,18,4,27,32,9,19,29,10,25,292,24,13,12,31,121,30,134,102,45,37,53,3,58,36,57,54,111])).
% 78.03/78.06 cnf(4798,plain,
% 78.03/78.06 (E(f9(x47981,x47982,a19),f9(x47981,x47982,f14(a16,a16)))),
% 78.03/78.06 inference(scs_inference,[],[1100,4732,472,96,97,6,23,20])).
% 78.03/78.06 cnf(4808,plain,
% 78.03/78.06 (E(f6(x48081,a19,x48082),f6(x48081,f14(a16,a16),x48082))),
% 78.03/78.06 inference(scs_inference,[],[1100,975,4732,472,96,97,6,23,20,21,2,16,7,33,28,17,14,15,8])).
% 78.03/78.06 cnf(4824,plain,
% 78.03/78.06 (E(f9(x48241,a19,x48242),f9(x48241,f14(a16,a16),x48242))),
% 78.03/78.06 inference(scs_inference,[],[1100,4784,975,4732,472,96,97,6,23,20,21,2,16,7,33,28,17,14,15,8,11,4,18,34,5,32,26,9,25,10,13,12,22,121,19])).
% 78.03/78.06 cnf(4830,plain,
% 78.03/78.06 (P6(a1,f14(a1,a15))),
% 78.03/78.06 inference(scs_inference,[],[1100,4784,975,328,4732,472,94,96,97,6,23,20,21,2,16,7,33,28,17,14,15,8,11,4,18,34,5,32,26,9,25,10,13,12,22,121,19,27,29,31,24,30,102])).
% 78.03/78.06 cnf(4833,plain,
% 78.03/78.06 (~P2(f25(a22),a1)),
% 78.03/78.06 inference(scs_inference,[],[1100,4784,975,4302,328,4732,1827,472,94,96,97,6,23,20,21,2,16,7,33,28,17,14,15,8,11,4,18,34,5,32,26,9,25,10,13,12,22,121,19,27,29,31,24,30,102,134])).
% 78.03/78.06 cnf(4837,plain,
% 78.03/78.06 (~P6(f9(a20,x48371,a16),f9(f14(a17,a16),x48371,f14(a16,a1)))),
% 78.03/78.06 inference(scs_inference,[],[1100,4784,975,4546,4302,328,4471,4732,4749,1827,4566,472,94,258,96,97,6,23,20,21,2,16,7,33,28,17,14,15,8,11,4,18,34,5,32,26,9,25,10,13,12,22,121,19,27,29,31,24,30,102,134,37,38,53])).
% 78.03/78.06 cnf(4841,plain,
% 78.03/78.06 (E(f6(a20,x48411,x48412),f6(f14(a17,a16),x48411,x48412))),
% 78.03/78.06 inference(rename_variables,[],[4732])).
% 78.03/78.06 cnf(4846,plain,
% 78.03/78.06 (~P1(a27,a15)),
% 78.03/78.06 inference(scs_inference,[],[1100,4784,975,4546,4302,328,4471,4387,4732,4841,4740,4749,1827,4566,4462,472,322,94,258,96,97,6,23,20,21,2,16,7,33,28,17,14,15,8,11,4,18,34,5,32,26,9,25,10,13,12,22,121,19,27,29,31,24,30,102,134,37,38,53,58,3,36])).
% 78.03/78.06 cnf(4861,plain,
% 78.03/78.06 (E(f6(a17,x48611,x48612),f6(f14(a15,a15),x48611,x48612))),
% 78.03/78.07 inference(scs_inference,[],[1214,4798,403,96,97,6,23,21,7])).
% 78.03/78.07 cnf(4863,plain,
% 78.03/78.07 (E(f9(x48631,x48632,a17),f9(x48631,x48632,f14(a15,a15)))),
% 78.03/78.07 inference(scs_inference,[],[1214,4798,403,96,97,6,23,21,7,33,20])).
% 78.03/78.07 cnf(4869,plain,
% 78.03/78.07 (E(f14(a17,x48691),f14(f14(a15,a15),x48691))),
% 78.03/78.07 inference(scs_inference,[],[1214,4404,4798,403,96,97,6,23,21,7,33,20,28,2,16,15,14,4])).
% 78.03/78.07 cnf(4872,plain,
% 78.03/78.07 (E(f14(x48721,a17),f14(x48721,f14(a15,a15)))),
% 78.03/78.07 inference(scs_inference,[],[1214,4404,4798,403,96,97,6,23,21,7,33,20,28,2,16,15,14,4,34,17,5])).
% 78.03/78.07 cnf(4874,plain,
% 78.03/78.07 (E(f6(x48741,a17,x48742),f6(x48741,f14(a15,a15),x48742))),
% 78.03/78.07 inference(scs_inference,[],[1214,4404,4798,403,96,97,6,23,21,7,33,20,28,2,16,15,14,4,34,17,5,11,8])).
% 78.03/78.07 cnf(4879,plain,
% 78.03/78.07 (E(f9(a17,x48791,x48792),f9(f14(a15,a15),x48791,x48792))),
% 78.03/78.07 inference(scs_inference,[],[1214,4404,4798,403,96,97,6,23,21,7,33,20,28,2,16,15,14,4,34,17,5,11,8,26,13,25,32,18])).
% 78.03/78.07 cnf(4892,plain,
% 78.03/78.07 (~P1(a27,f14(a15,a15))),
% 78.03/78.07 inference(scs_inference,[],[1214,4846,4404,4830,4798,315,403,96,97,6,23,21,7,33,20,28,2,16,15,14,4,34,17,5,11,8,26,13,25,32,18,12,121,10,9,22,31,29,19,27,24,30,155])).
% 78.03/78.07 cnf(4895,plain,
% 78.03/78.07 (P6(a1,f14(a15,a15))),
% 78.03/78.07 inference(scs_inference,[],[1214,4846,4404,4830,413,4798,315,403,94,96,97,6,23,21,7,33,20,28,2,16,15,14,4,34,17,5,11,8,26,13,25,32,18,12,121,10,9,22,31,29,19,27,24,30,155,102])).
% 78.03/78.07 cnf(4900,plain,
% 78.03/78.07 (~P2(f25(a19),f14(a1,a1))),
% 78.03/78.07 inference(scs_inference,[],[1214,4846,4404,4830,413,4701,4798,315,403,82,94,71,96,97,6,23,21,7,33,20,28,2,16,15,14,4,34,17,5,11,8,26,13,25,32,18,12,121,10,9,22,31,29,19,27,24,30,155,102,134,38])).
% 78.03/78.07 cnf(4907,plain,
% 78.03/78.07 (~P1(a2,f14(a1,a17))),
% 78.03/78.07 inference(scs_inference,[],[1214,1317,4780,4846,4404,4781,4830,413,4701,4798,4824,4837,4448,315,403,82,74,94,472,71,96,97,6,23,21,7,33,20,28,2,16,15,14,4,34,17,5,11,8,26,13,25,32,18,12,121,10,9,22,31,29,19,27,24,30,155,102,134,38,58,53,3,36])).
% 78.03/78.07 cnf(4921,plain,
% 78.03/78.07 (~E(f25(a1),f25(a19))),
% 78.03/78.07 inference(scs_inference,[],[1214,1317,4780,4846,4404,4781,4830,413,4701,4717,4798,4808,4824,4837,4430,4448,315,403,82,74,94,472,71,96,97,6,23,21,7,33,20,28,2,16,15,14,4,34,17,5,11,8,26,13,25,32,18,12,121,10,9,22,31,29,19,27,24,30,155,102,134,38,58,53,3,36,57,54,734,851,852,787,786,809,735,810,292])).
% 78.03/78.07 cnf(4931,plain,
% 78.03/78.07 (E(f6(f14(a17,a17),x49311,x49312),f6(a18,x49311,x49312))),
% 78.03/78.07 inference(scs_inference,[],[1381,4861,80,96,97,21,23,7])).
% 78.03/78.07 cnf(4950,plain,
% 78.03/78.07 (E(f6(x49501,f14(a17,a17),x49502),f6(x49501,a18,x49502))),
% 78.03/78.07 inference(scs_inference,[],[1381,1252,4895,4861,80,96,97,21,23,7,20,6,28,33,4,34,2,17,14,16,15,11,26,18,5,121,13,8])).
% 78.03/78.07 cnf(4966,plain,
% 78.03/78.07 (P6(a1,f14(a17,a17))),
% 78.03/78.07 inference(scs_inference,[],[1381,1252,4892,4895,672,4861,315,80,94,96,97,21,23,7,20,6,28,33,4,34,2,17,14,16,15,11,26,18,5,121,13,8,32,10,29,25,22,19,9,12,27,31,30,24,155,102])).
% 78.03/78.07 cnf(4973,plain,
% 78.03/78.07 (E(f6(a17,x49731,x49732),f6(f14(a15,a15),x49731,x49732))),
% 78.03/78.07 inference(rename_variables,[],[4861])).
% 78.03/78.07 cnf(4976,plain,
% 78.03/78.07 (E(f6(a17,x49761,x49762),f6(f14(a15,a15),x49761,x49762))),
% 78.03/78.07 inference(rename_variables,[],[4861])).
% 78.03/78.07 cnf(4978,plain,
% 78.03/78.07 (~P6(f9(a17,a16,a16),f9(f14(a15,a15),f14(a16,a1),f14(a16,a1)))),
% 78.03/78.07 inference(scs_inference,[],[1381,1252,4773,4892,4895,672,4861,4973,4874,4879,4387,4706,315,80,82,94,71,96,97,21,23,7,20,6,28,33,4,34,2,17,14,16,15,11,26,18,5,121,13,8,32,10,29,25,22,19,9,12,27,31,30,24,155,102,134,38,58,3,53])).
% 78.03/78.07 cnf(4981,plain,
% 78.03/78.07 (~P1(a27,f14(a17,a15))),
% 78.03/78.07 inference(scs_inference,[],[1381,1252,4773,4892,4895,672,4861,4973,4874,4879,4869,4387,4706,315,80,82,94,71,96,97,21,23,7,20,6,28,33,4,34,2,17,14,16,15,11,26,18,5,121,13,8,32,10,29,25,22,19,9,12,27,31,30,24,155,102,134,38,58,3,53,36])).
% 78.03/78.07 cnf(4985,plain,
% 78.03/78.07 (~P6(f6(f14(a15,a15),x49851,x49852),f6(a17,x49851,x49852))),
% 78.03/78.07 inference(scs_inference,[],[1381,1252,4773,4892,4895,672,4861,4973,4976,4863,4874,4879,4869,4387,4706,315,80,82,94,208,209,71,96,97,21,23,7,20,6,28,33,4,34,2,17,14,16,15,11,26,18,5,121,13,8,32,10,29,25,22,19,9,12,27,31,30,24,155,102,134,38,58,3,53,36,57,54])).
% 78.03/78.07 cnf(4987,plain,
% 78.03/78.07 (~E(f25(a1),f25(a17))),
% 78.03/78.07 inference(scs_inference,[],[1381,1252,4773,4892,4895,672,4861,4973,4976,4863,4874,4879,4869,4387,4706,315,80,82,94,208,209,71,96,97,21,23,7,20,6,28,33,4,34,2,17,14,16,15,11,26,18,5,121,13,8,32,10,29,25,22,19,9,12,27,31,30,24,155,102,134,38,58,3,53,36,57,54,292])).
% 78.03/78.07 cnf(5001,plain,
% 78.03/78.07 (E(f6(a16,x50011,x50012),f6(f14(a15,a17),x50011,x50012))),
% 78.03/78.07 inference(scs_inference,[],[1418,4931,451,96,97,23,21,6,7])).
% 78.03/78.07 cnf(5005,plain,
% 78.03/78.07 (E(f7(x50051,a16,x50052),f7(x50051,f14(a15,a17),x50052))),
% 78.03/78.07 inference(scs_inference,[],[1418,4931,451,96,97,23,21,6,7,20,28,33,16])).
% 78.03/78.07 cnf(5011,plain,
% 78.03/78.07 (E(f14(a16,x50111),f14(f14(a15,a17),x50111))),
% 78.03/78.07 inference(scs_inference,[],[1418,4617,4966,4931,451,96,97,23,21,6,7,20,28,33,16,121,14,34,2,4])).
% 78.03/78.07 cnf(5012,plain,
% 78.03/78.07 (E(f10(x50121,a16,x50122),f10(x50121,f14(a15,a17),x50122))),
% 78.03/78.07 inference(scs_inference,[],[1418,4617,4966,4931,451,96,97,23,21,6,7,20,28,33,16,121,14,34,2,4,26])).
% 78.03/78.07 cnf(5014,plain,
% 78.03/78.07 (E(f9(a16,x50141,x50142),f9(f14(a15,a17),x50141,x50142))),
% 78.03/78.07 inference(scs_inference,[],[1418,4617,4966,4931,451,96,97,23,21,6,7,20,28,33,16,121,14,34,2,4,26,17,18])).
% 78.03/78.07 cnf(5018,plain,
% 78.03/78.07 (E(f6(x50181,a16,x50182),f6(x50181,f14(a15,a17),x50182))),
% 78.03/78.07 inference(scs_inference,[],[1418,4617,4966,4931,451,96,97,23,21,6,7,20,28,33,16,121,14,34,2,4,26,17,18,29,15,13,8])).
% 78.03/78.07 cnf(5035,plain,
% 78.03/78.07 (P6(a1,f14(a1,a16))),
% 78.03/78.07 inference(scs_inference,[],[1418,4617,4981,4966,4931,357,315,451,94,96,97,23,21,6,7,20,28,33,16,121,14,34,2,4,26,17,18,29,15,13,8,11,22,32,5,9,19,10,25,27,12,30,31,24,155,102])).
% 78.03/78.07 cnf(5039,plain,
% 78.03/78.07 (~P2(f25(a22),f14(a1,a1))),
% 78.03/78.07 inference(scs_inference,[],[1418,4617,4900,4981,4833,4966,4931,357,1822,315,451,94,71,96,97,23,21,6,7,20,28,33,16,121,14,34,2,4,26,17,18,29,15,13,8,11,22,32,5,9,19,10,25,27,12,30,31,24,155,102,37,38])).
% 78.03/78.07 cnf(5047,plain,
% 78.03/78.07 (~P1(a2,f14(a17,a1))),
% 78.03/78.07 inference(scs_inference,[],[1418,4617,4900,4635,4907,4981,4833,4966,4985,4931,4950,1243,357,1822,315,451,83,94,208,430,71,96,97,23,21,6,7,20,28,33,16,121,14,34,2,4,26,17,18,29,15,13,8,11,22,32,5,9,19,10,25,27,12,30,31,24,155,102,37,38,58,3,53,57,36])).
% 78.03/78.07 cnf(5061,plain,
% 78.03/78.07 (~E(f25(a1),f25(a22))),
% 78.03/78.07 inference(scs_inference,[],[1418,4617,4900,4635,4907,4981,4833,4966,4985,4931,4950,4978,1243,4709,357,1822,315,451,83,94,208,430,71,96,97,23,21,6,7,20,28,33,16,121,14,34,2,4,26,17,18,29,15,13,8,11,22,32,5,9,19,10,25,27,12,30,31,24,155,102,37,38,58,3,53,57,36,54,709,625,624,708,891,623,890,710,910,600,292])).
% 78.03/78.07 cnf(5063,plain,
% 78.03/78.07 (~P2(f25(a24),a1)),
% 78.03/78.07 inference(scs_inference,[],[1418,4617,4900,4635,4907,4981,4833,4966,4985,4931,4950,4978,1388,1243,4709,357,1822,315,451,82,83,94,208,430,71,96,97,23,21,6,7,20,28,33,16,121,14,34,2,4,26,17,18,29,15,13,8,11,22,32,5,9,19,10,25,27,12,30,31,24,155,102,37,38,58,3,53,57,36,54,709,625,624,708,891,623,890,710,910,600,292,67,134])).
% 78.03/78.07 cnf(5087,plain,
% 78.03/78.07 (E(f6(f14(a15,a16),x50871,x50872),f6(a18,x50871,x50872))),
% 78.03/78.07 inference(scs_inference,[],[1451,5001,76,96,97,21,28,6,23,33,7])).
% 78.03/78.07 cnf(5119,plain,
% 78.03/78.07 (P6(a1,f14(a15,a16))),
% 78.03/78.07 inference(scs_inference,[],[1451,4695,5035,5047,5001,699,216,76,94,96,97,21,28,6,23,33,7,2,4,34,20,14,121,26,16,13,18,15,17,22,10,29,11,8,5,27,9,12,32,19,30,25,31,24,155,102])).
% 78.03/78.07 cnf(5122,plain,
% 78.03/78.07 (~P2(f25(f14(a15,a17)),a1)),
% 78.03/78.07 inference(scs_inference,[],[1451,4695,5035,5047,5001,699,1528,216,76,82,94,96,97,21,28,6,23,33,7,2,4,34,20,14,121,26,16,13,18,15,17,22,10,29,11,8,5,27,9,12,32,19,30,25,31,24,155,102,134])).
% 78.03/78.07 cnf(5127,plain,
% 78.03/78.07 (E(f6(a16,x51271,x51272),f6(f14(a15,a17),x51271,x51272))),
% 78.03/78.07 inference(rename_variables,[],[5001])).
% 78.03/78.07 cnf(5141,plain,
% 78.03/78.07 (~E(f25(a1),f25(a24))),
% 78.03/78.07 inference(scs_inference,[],[1451,4695,5035,5047,5063,4715,5001,5127,5005,5012,5014,5018,699,4872,1528,4392,4380,4706,216,76,82,94,208,209,71,96,97,21,28,6,23,33,7,2,4,34,20,14,121,26,16,13,18,15,17,22,10,29,11,8,5,27,9,12,32,19,30,25,31,24,155,102,134,37,38,3,58,53,36,57,54,292])).
% 78.03/78.07 cnf(5158,plain,
% 78.03/78.07 (E(f25(f14(a17,a16)),f25(a20))),
% 78.03/78.07 inference(scs_inference,[],[386,4987,5119,5087,79,96,97,33,23,21,121,2,28,20,6])).
% 78.03/78.07 cnf(5160,plain,
% 78.03/78.07 (E(f6(f14(a17,a16),x51601,x51602),f6(a20,x51601,x51602))),
% 78.03/78.07 inference(scs_inference,[],[386,4987,5119,5087,79,96,97,33,23,21,121,2,28,20,6,4,7])).
% 78.03/78.07 cnf(5164,plain,
% 78.03/78.07 (E(f7(x51641,f14(a17,a16),x51642),f7(x51641,a20,x51642))),
% 78.03/78.07 inference(scs_inference,[],[386,4987,5119,5087,79,96,97,33,23,21,121,2,28,20,6,4,7,14,34,13,16])).
% 78.03/78.07 cnf(5218,plain,
% 78.03/78.07 (E(f9(x52181,x52182,f14(a16,a16)),f9(x52181,x52182,a19))),
% 78.03/78.07 inference(scs_inference,[],[437,4921,5160,4768,78,96,97,23,121,33,6,2,21,4,20])).
% 78.03/78.07 cnf(5250,plain,
% 78.03/78.07 (P1(a2,f14(a16,a1))),
% 78.03/78.07 inference(scs_inference,[],[81,437,4921,5160,5164,5158,4712,4768,4465,328,78,82,4550,96,97,23,121,33,6,2,21,4,20,28,7,16,13,15,14,34,18,10,5,32,30,26,8,9,17,11,27,29,19,12,22,25,24,31,134,37,57,36])).
% 78.03/78.07 cnf(5278,plain,
% 78.03/78.07 (E(f6(f14(a15,a17),x52781,x52782),f6(a16,x52781,x52782))),
% 78.03/78.07 inference(scs_inference,[],[458,5218,4629,77,96,97,121,23,21,33,6,7])).
% 78.03/78.07 cnf(5281,plain,
% 78.03/78.07 (E(f7(x52811,f14(a15,a17),x52812),f7(x52811,a16,x52812))),
% 78.03/78.07 inference(scs_inference,[],[458,5061,5218,4629,77,96,97,121,23,21,33,6,7,2,4,16])).
% 78.03/78.07 cnf(5282,plain,
% 78.03/78.07 (E(f9(x52821,x52822,f14(a15,a17)),f9(x52821,x52822,a16))),
% 78.03/78.07 inference(scs_inference,[],[458,5061,5218,4629,77,96,97,121,23,21,33,6,7,2,4,16,20])).
% 78.03/78.07 cnf(5287,plain,
% 78.03/78.07 (E(f5(f14(a15,a17),x52871,x52872),f5(a16,x52871,x52872))),
% 78.03/78.07 inference(scs_inference,[],[458,5061,5218,4629,77,96,97,121,23,21,33,6,7,2,4,16,20,28,34,13,5,10])).
% 78.03/78.07 cnf(5296,plain,
% 78.03/78.07 (E(f6(x52961,f14(a15,a17),x52962),f6(x52961,a16,x52962))),
% 78.03/78.07 inference(scs_inference,[],[458,5061,5218,4629,77,96,97,121,23,21,33,6,7,2,4,16,20,28,34,13,5,10,26,15,18,14,29,30,17,27,8])).
% 78.03/78.07 cnf(5306,plain,
% 78.03/78.07 (~P2(f25(a15),a1)),
% 78.03/78.07 inference(scs_inference,[],[458,5061,5218,4629,279,77,82,96,97,121,23,21,33,6,7,2,4,16,20,28,34,13,5,10,26,15,18,14,29,30,17,27,8,32,9,19,25,11,22,12,24,31,134])).
% 78.03/78.07 cnf(5309,plain,
% 78.03/78.07 (~P8(f14(a17,a17),f14(f14(a16,a1),a1))),
% 78.03/78.07 inference(scs_inference,[],[458,5061,5218,4778,5039,4629,279,1822,77,82,80,96,97,121,23,21,33,6,7,2,4,16,20,28,34,13,5,10,26,15,18,14,29,30,17,27,8,32,9,19,25,11,22,12,24,31,134,37,57])).
% 78.03/78.07 cnf(5364,plain,
% 78.03/78.07 (~P1(a2,f14(a17,a15))),
% 78.03/78.07 inference(scs_inference,[],[502,5141,5278,4456,4780,216,322,96,97,121,23,21,33,7,6,20,4,34,28,16,5,2,26,13,17,10,18,30,15,29,27,32,14,9,22,8,11,12,19,25,24,31,155])).
% 78.03/78.07 cnf(5368,plain,
% 78.03/78.07 (~P2(f25(a15),f14(a1,a1))),
% 78.03/78.07 inference(scs_inference,[],[502,5141,5306,5278,4456,4780,4563,5158,216,322,71,96,97,121,23,21,33,7,6,20,4,34,28,16,5,2,26,13,17,10,18,30,15,29,27,32,14,9,22,8,11,12,19,25,24,31,155,37,38])).
% 78.03/78.07 cnf(5370,plain,
% 78.03/78.07 (E(f6(f14(a15,a17),x53701,x53702),f6(a16,x53701,x53702))),
% 78.03/78.07 inference(rename_variables,[],[5278])).
% 78.03/78.07 cnf(5371,plain,
% 78.03/78.07 (E(f6(x53711,f14(a15,a17),x53712),f6(x53711,a16,x53712))),
% 78.03/78.07 inference(rename_variables,[],[5296])).
% 78.03/78.07 cnf(5387,plain,
% 78.03/78.07 (P6(f14(a16,a1),a20)),
% 78.03/78.07 inference(scs_inference,[],[502,5141,5250,5306,5278,5370,5281,5282,5296,5371,5011,4456,4780,4717,4563,5158,4387,216,322,208,209,71,96,97,121,23,21,33,7,6,20,4,34,28,16,5,2,26,13,17,10,18,30,15,29,27,32,14,9,22,8,11,12,19,25,24,31,155,37,38,3,53,36,58,57,54,654,678,832,107])).
% 78.03/78.07 cnf(5389,plain,
% 78.03/78.07 (~E(a20,f14(a16,a1))),
% 78.03/78.07 inference(scs_inference,[],[502,5141,5250,5306,5278,5370,5281,5282,5296,5371,5011,4456,4780,4717,4563,5158,4387,216,322,208,209,71,96,97,121,23,21,33,7,6,20,4,34,28,16,5,2,26,13,17,10,18,30,15,29,27,32,14,9,22,8,11,12,19,25,24,31,155,37,38,3,53,36,58,57,54,654,678,832,107,101])).
% 78.03/78.07 cnf(5451,plain,
% 78.03/78.07 ($false),
% 78.03/78.07 inference(scs_inference,[],[526,1155,5368,5364,5387,5389,5287,5122,5309,846,4619,4392,1822,74,83,94,495,71,127,96,97,121,23,21,292,33,7,34,4,16,6,28,20,2,26,5,13,17,15,27,10,29,30,14,18,11,8,32,22,25,9,19,12,24,31,124,102,37,38,58,3,36]),
% 78.03/78.07 ['proof']).
% 78.03/78.07 % SZS output end Proof
% 78.03/78.07 % Total time :77.250000s
%------------------------------------------------------------------------------