%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CSR004+2 : TPTP v8.2.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n018.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:50 EDT 2024
% Result : Theorem 0.57s 0.68s
% Output : CNFRefutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : CSR004+2 : TPTP v8.2.0. Bugfixed v3.1.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n018.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu Jun 20 00:15:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.48/0.60 start to proof:theBenchmark
% 0.57/0.67 %-------------------------------------------
% 0.57/0.67 % File :CSE---1.7
% 0.57/0.67 % Problem :theBenchmark
% 0.57/0.67 % Transform :cnf
% 0.57/0.67 % Format :tptp:raw
% 0.57/0.67 % Command :java -jar mcs_scs.jar %d %s
% 0.57/0.67
% 0.57/0.67 % Result :Theorem 0.000000s
% 0.57/0.67 % Output :CNFRefutation 0.000000s
% 0.57/0.67 %-------------------------------------------
% 0.57/0.67 %--------------------------------------------------------------------------
% 0.57/0.67 % File : CSR004+2 : TPTP v8.2.0. Bugfixed v3.1.0.
% 0.57/0.67 % Domain : Commonsense Reasoning
% 0.57/0.67 % Problem : Overflow happens at time 3
% 0.57/0.67 % Version : [Mue04] axioms : Augmented > Especial.
% 0.57/0.67 % English :
% 0.57/0.67
% 0.57/0.67 % Refs : [MS05] Mueller & Sutcliffe (2005), Reasoning in the Event Cal
% 0.57/0.67 % : [Mue04] Mueller (2004), A Tool for Satisfiability-based Common
% 0.57/0.67 % : [MS02] Miller & Shanahan (2002), Some Alternative Formulation
% 0.57/0.67 % Source : [MS05]
% 0.57/0.67 % Names :
% 0.57/0.67
% 0.57/0.67 % Status : Theorem
% 0.57/0.67 % Rating : 0.11 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.10 v6.0.0, 0.09 v5.5.0, 0.07 v5.4.0, 0.11 v5.3.0, 0.15 v5.2.0, 0.10 v5.0.0, 0.04 v4.1.0, 0.09 v4.0.0, 0.08 v3.7.0, 0.05 v3.4.0, 0.11 v3.3.0, 0.07 v3.2.0, 0.09 v3.1.0
% 0.57/0.67 % Syntax : Number of formulae : 57 ( 27 unt; 0 def)
% 0.57/0.67 % Number of atoms : 138 ( 40 equ)
% 0.57/0.67 % Maximal formula atoms : 11 ( 2 avg)
% 0.57/0.67 % Number of connectives : 109 ( 28 ~; 8 |; 43 &)
% 0.57/0.67 % ( 18 <=>; 12 =>; 0 <=; 0 <~>)
% 0.57/0.67 % Maximal formula depth : 12 ( 4 avg)
% 0.57/0.67 % Maximal term depth : 2 ( 1 avg)
% 0.57/0.67 % Number of predicates : 13 ( 12 usr; 0 prp; 2-4 aty)
% 0.57/0.67 % Number of functors : 17 ( 17 usr; 15 con; 0-2 aty)
% 0.57/0.67 % Number of variables : 86 ( 74 !; 12 ?)
% 0.57/0.67 % SPC : FOF_THM_RFO_SEQ
% 0.57/0.67
% 0.57/0.67 % Comments :
% 0.57/0.67 %--------------------------------------------------------------------------
% 0.57/0.67 %----Include standard discrete event calculus axioms
% 0.57/0.67 include('Axioms/CSR001+0.ax').
% 0.57/0.67 %----Include kitchen sink scenario axioms
% 0.57/0.67 include('Axioms/CSR001+1.ax').
% 0.57/0.67 %--------------------------------------------------------------------------
% 0.57/0.67 fof(plus0_0,axiom,
% 0.57/0.67 plus(n0,n0) = n0 ).
% 0.57/0.67
% 0.57/0.67 fof(plus0_1,axiom,
% 0.57/0.67 plus(n0,n1) = n1 ).
% 0.57/0.67
% 0.57/0.67 fof(plus0_2,axiom,
% 0.57/0.67 plus(n0,n2) = n2 ).
% 0.57/0.67
% 0.57/0.67 fof(plus0_3,axiom,
% 0.57/0.67 plus(n0,n3) = n3 ).
% 0.57/0.67
% 0.57/0.67 fof(plus1_1,axiom,
% 0.57/0.67 plus(n1,n1) = n2 ).
% 0.57/0.67
% 0.57/0.67 fof(plus1_2,axiom,
% 0.57/0.67 plus(n1,n2) = n3 ).
% 0.57/0.67
% 0.57/0.67 fof(plus1_3,axiom,
% 0.57/0.67 plus(n1,n3) = n4 ).
% 0.57/0.67
% 0.57/0.67 fof(plus2_2,axiom,
% 0.57/0.67 plus(n2,n2) = n4 ).
% 0.57/0.67
% 0.57/0.67 fof(plus2_3,axiom,
% 0.57/0.67 plus(n2,n3) = n5 ).
% 0.57/0.67
% 0.57/0.67 fof(plus3_3,axiom,
% 0.57/0.67 plus(n3,n3) = n6 ).
% 0.57/0.67
% 0.57/0.67 fof(symmetry_of_plus,axiom,
% 0.57/0.67 ! [X,Y] : plus(X,Y) = plus(Y,X) ).
% 0.57/0.67
% 0.57/0.67 fof(less_or_equal,axiom,
% 0.57/0.67 ! [X,Y] :
% 0.57/0.67 ( less_or_equal(X,Y)
% 0.57/0.67 <=> ( less(X,Y)
% 0.57/0.67 | X = Y ) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less0,axiom,
% 0.57/0.67 ~ ? [X] : less(X,n0) ).
% 0.57/0.67
% 0.57/0.67 fof(less1,axiom,
% 0.57/0.67 ! [X] :
% 0.57/0.67 ( less(X,n1)
% 0.57/0.67 <=> less_or_equal(X,n0) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less2,axiom,
% 0.57/0.67 ! [X] :
% 0.57/0.67 ( less(X,n2)
% 0.57/0.67 <=> less_or_equal(X,n1) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less3,axiom,
% 0.57/0.67 ! [X] :
% 0.57/0.67 ( less(X,n3)
% 0.57/0.67 <=> less_or_equal(X,n2) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less4,axiom,
% 0.57/0.67 ! [X] :
% 0.57/0.67 ( less(X,n4)
% 0.57/0.67 <=> less_or_equal(X,n3) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less5,axiom,
% 0.57/0.67 ! [X] :
% 0.57/0.67 ( less(X,n5)
% 0.57/0.67 <=> less_or_equal(X,n4) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less6,axiom,
% 0.57/0.67 ! [X] :
% 0.57/0.67 ( less(X,n6)
% 0.57/0.67 <=> less_or_equal(X,n5) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less7,axiom,
% 0.57/0.67 ! [X] :
% 0.57/0.67 ( less(X,n7)
% 0.57/0.67 <=> less_or_equal(X,n6) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less8,axiom,
% 0.57/0.67 ! [X] :
% 0.57/0.67 ( less(X,n8)
% 0.57/0.67 <=> less_or_equal(X,n7) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less9,axiom,
% 0.57/0.67 ! [X] :
% 0.57/0.67 ( less(X,n9)
% 0.57/0.67 <=> less_or_equal(X,n8) ) ).
% 0.57/0.67
% 0.57/0.67 fof(less_property,axiom,
% 0.57/0.67 ! [X,Y] :
% 0.57/0.67 ( less(X,Y)
% 0.57/0.67 <=> ( ~ less(Y,X)
% 0.57/0.67 & Y != X ) ) ).
% 0.57/0.67
% 0.57/0.67 %----Initial conditions
% 0.57/0.67 fof(waterLevel_0,hypothesis,
% 0.57/0.67 holdsAt(waterLevel(n0),n0) ).
% 0.57/0.67
% 0.57/0.67 fof(not_filling_0,hypothesis,
% 0.57/0.67 ~ holdsAt(filling,n0) ).
% 0.57/0.67
% 0.57/0.67 fof(not_spilling_0,hypothesis,
% 0.57/0.67 ~ holdsAt(spilling,n0) ).
% 0.57/0.67
% 0.57/0.67 fof(not_released_waterLevel_0,hypothesis,
% 0.57/0.67 ! [Height] : ~ releasedAt(waterLevel(Height),n0) ).
% 0.57/0.67
% 0.57/0.67 fof(not_released_filling_0,hypothesis,
% 0.57/0.67 ~ releasedAt(filling,n0) ).
% 0.57/0.67
% 0.57/0.67 fof(not_released_spilling_0,hypothesis,
% 0.57/0.67 ~ releasedAt(spilling,n0) ).
% 0.57/0.67
% 0.57/0.67 fof(waterLevel_3,lemma,
% 0.57/0.67 holdsAt(waterLevel(n3),n3) ).
% 0.57/0.67
% 0.57/0.67 fof(filling_3,lemma,
% 0.57/0.67 holdsAt(filling,n3) ).
% 0.57/0.68
% 0.57/0.68 fof(overflow_3,conjecture,
% 0.57/0.68 happens(overflow,n3) ).
% 0.57/0.68
% 0.57/0.68 %--------------------------------------------------------------------------
% 0.57/0.68 %-------------------------------------------
% 0.57/0.68 % Proof found
% 0.57/0.68 % SZS status Theorem for theBenchmark
% 0.57/0.68 % SZS output start Proof
% 0.57/0.68 %ClaNum:208(EqnAxiom:70)
% 0.57/0.68 %VarNum:619(SingletonVarNum:232)
% 0.57/0.68 %MaxLitNum:6
% 0.57/0.68 %MaxfuncDepth:2
% 0.57/0.68 %SharedTerms:49
% 0.57/0.68 %goalClause: 91
% 0.57/0.68 %singleGoalClaCount:1
% 0.57/0.68 [81]P1(a2,a16)
% 0.57/0.68 [85]~E(a21,a26)
% 0.57/0.68 [86]~E(a27,a2)
% 0.57/0.68 [87]~E(a28,a26)
% 0.57/0.68 [88]~E(a28,a21)
% 0.57/0.68 [91]~P2(a21,a16)
% 0.57/0.68 [92]~P1(a2,a1)
% 0.57/0.68 [93]~P1(a27,a1)
% 0.57/0.68 [94]~P5(a2,a1)
% 0.57/0.68 [95]~P5(a27,a1)
% 0.57/0.68 [71]E(f14(a1,a1),a1)
% 0.57/0.68 [72]E(f14(a1,a15),a15)
% 0.57/0.68 [73]E(f14(a1,a16),a16)
% 0.57/0.68 [74]E(f14(a1,a17),a17)
% 0.57/0.68 [75]E(f14(a15,a15),a17)
% 0.57/0.68 [76]E(f14(a15,a16),a18)
% 0.57/0.68 [77]E(f14(a15,a17),a16)
% 0.57/0.68 [78]E(f14(a16,a16),a19)
% 0.57/0.68 [79]E(f14(a17,a16),a20)
% 0.57/0.68 [80]E(f14(a17,a17),a18)
% 0.57/0.68 [82]P1(f25(a1),a1)
% 0.57/0.68 [83]P1(f25(a16),a16)
% 0.57/0.68 [96]~P6(x961,a1)
% 0.57/0.68 [89]~E(f25(x891),a2)
% 0.57/0.68 [90]~E(f25(x901),a27)
% 0.57/0.68 [97]~P5(f25(x971),a1)
% 0.57/0.68 [84]E(f14(x841,x842),f14(x842,x841))
% 0.57/0.68 [105]~P8(x1051,a1)+P6(x1051,a15)
% 0.57/0.68 [106]~P8(x1061,a17)+P6(x1061,a16)
% 0.57/0.68 [107]~P8(x1071,a15)+P6(x1071,a17)
% 0.57/0.68 [108]~P8(x1081,a16)+P6(x1081,a18)
% 0.57/0.68 [109]~P8(x1091,a18)+P6(x1091,a20)
% 0.57/0.68 [110]~P8(x1101,a20)+P6(x1101,a19)
% 0.57/0.68 [111]~P8(x1111,a19)+P6(x1111,a22)
% 0.57/0.68 [112]~P8(x1121,a22)+P6(x1121,a23)
% 0.57/0.68 [113]~P8(x1131,a23)+P6(x1131,a24)
% 0.57/0.68 [114]~P6(x1141,a15)+P8(x1141,a1)
% 0.57/0.68 [115]~P6(x1151,a17)+P8(x1151,a15)
% 0.57/0.68 [116]~P6(x1161,a18)+P8(x1161,a16)
% 0.57/0.68 [117]~P6(x1171,a16)+P8(x1171,a17)
% 0.57/0.68 [118]~P6(x1181,a20)+P8(x1181,a18)
% 0.57/0.68 [119]~P6(x1191,a19)+P8(x1191,a20)
% 0.57/0.68 [120]~P6(x1201,a22)+P8(x1201,a19)
% 0.57/0.68 [121]~P6(x1211,a23)+P8(x1211,a22)
% 0.57/0.68 [122]~P6(x1221,a24)+P8(x1221,a23)
% 0.57/0.68 [99]~E(x991,x992)+P8(x991,x992)
% 0.57/0.68 [103]~P6(x1032,x1031)+~E(x1031,x1032)
% 0.57/0.68 [123]~P6(x1231,x1232)+P8(x1231,x1232)
% 0.57/0.68 [129]~P6(x1292,x1291)+~P6(x1291,x1292)
% 0.57/0.68 [98]E(x981,x982)+~E(f25(x981),f25(x982))
% 0.57/0.68 [137]~P10(x1371,x1372,x1373)+E(x1371,a26)
% 0.57/0.68 [138]~P9(x1382,x1381,x1383)+E(x1381,a2)
% 0.57/0.68 [152]~P3(x1522,x1521,x1523)+P7(x1521,x1522,x1523)
% 0.57/0.68 [153]~P7(x1532,x1531,x1533)+P3(x1531,x1532,x1533)
% 0.57/0.68 [171]~P11(x1711,x1712,x1713)+P6(x1711,f7(x1711,x1712,x1713))
% 0.57/0.68 [172]~P12(x1721,x1723,x1722)+P6(x1721,f9(x1721,x1722,x1723))
% 0.57/0.68 [173]~P11(x1731,x1732,x1733)+P6(f7(x1731,x1732,x1733),x1733)
% 0.57/0.68 [174]~P12(x1741,x1743,x1742)+P6(f9(x1741,x1742,x1743),x1742)
% 0.57/0.68 [183]~P11(x1831,x1832,x1833)+P2(f8(x1831,x1832,x1833),f7(x1831,x1832,x1833))
% 0.57/0.68 [184]~P12(x1841,x1843,x1842)+P2(f10(x1841,x1842,x1843),f9(x1841,x1842,x1843))
% 0.57/0.68 [193]~P11(x1931,x1932,x1933)+P9(f8(x1931,x1932,x1933),x1932,f7(x1931,x1932,x1933))
% 0.57/0.68 [194]~P12(x1941,x1943,x1942)+P7(f10(x1941,x1942,x1943),x1943,f9(x1941,x1942,x1943))
% 0.57/0.68 [150]~P10(x1501,x1502,x1503)+E(f25(f13(x1501,x1502)),x1502)
% 0.57/0.68 [100]P2(x1001,x1002)+~E(x1002,a1)+~E(x1001,a26)
% 0.57/0.68 [101]~P2(x1012,x1011)+E(x1011,a1)+E(x1012,a21)
% 0.57/0.68 [102]~P2(x1021,x1022)+E(x1021,a21)+E(x1021,a26)
% 0.57/0.68 [104]P6(x1042,x1041)+P6(x1041,x1042)+E(x1041,x1042)
% 0.57/0.68 [124]~P2(x1241,x1242)+E(x1241,a26)+P1(a2,x1242)
% 0.57/0.68 [125]~P2(x1252,x1251)+P1(a2,x1251)+E(x1251,a1)
% 0.57/0.68 [126]P6(x1261,x1262)+~P8(x1261,x1262)+E(x1261,x1262)
% 0.57/0.68 [127]~P2(x1271,x1272)+E(x1271,a26)+P1(f25(a16),x1272)
% 0.57/0.68 [128]~P2(x1282,x1281)+E(x1281,a1)+P1(f25(a16),x1281)
% 0.57/0.68 [148]~P5(x1481,x1482)+P2(f3(x1481,x1482),x1482)+P5(x1481,f14(x1482,a15))
% 0.57/0.68 [149]P5(x1491,x1492)+P2(f12(x1491,x1492),x1492)+~P5(x1491,f14(x1492,a15))
% 0.57/0.68 [157]P5(x1571,x1572)+P10(f12(x1571,x1572),x1571,x1572)+~P5(x1571,f14(x1572,a15))
% 0.57/0.68 [130]P9(x1301,x1302,x1303)+~E(x1302,a2)+~E(x1301,a21)
% 0.57/0.68 [131]P9(x1311,x1312,x1313)+~E(x1312,a2)+~E(x1311,a28)
% 0.57/0.68 [132]P3(x1321,x1322,x1323)+~E(x1321,a2)+~E(x1322,a26)
% 0.57/0.68 [133]P3(x1331,x1332,x1333)+~E(x1331,a27)+~E(x1332,a21)
% 0.57/0.68 [141]~P9(x1411,x1412,x1413)+E(x1411,a28)+E(x1411,a21)
% 0.57/0.68 [136]E(x1361,x1362)+~P1(f25(x1361),x1363)+~P1(f25(x1362),x1363)
% 0.57/0.68 [154]~P7(x1543,x1541,x1542)+~P2(x1543,x1542)+P1(x1541,f14(x1542,a15))
% 0.57/0.68 [155]~P10(x1553,x1551,x1552)+~P2(x1553,x1552)+P5(x1551,f14(x1552,a15))
% 0.57/0.68 [158]~P2(x1581,x1582)+~P9(x1581,x1583,x1582)+~P5(x1583,f14(x1582,a15))
% 0.57/0.68 [159]~P2(x1591,x1592)+~P7(x1591,x1593,x1592)+~P5(x1593,f14(x1592,a15))
% 0.57/0.68 [160]~P2(x1601,x1602)+~P9(x1601,x1603,x1602)+~P1(x1603,f14(x1602,a15))
% 0.57/0.68 [135]P10(x1351,x1352,x1353)+~E(x1351,a26)+~E(x1352,f25(x1354))
% 0.57/0.68 [178]~P1(f25(x1784),x1781)+P13(a2,x1781,f25(x1782),x1783)+~E(x1782,f14(x1784,x1783))
% 0.57/0.68 [134]P2(x1341,x1342)+~E(x1341,a21)+~P1(a2,x1342)+~P1(f25(a16),x1342)
% 0.57/0.68 [151]~P1(x1511,x1512)+P2(f4(x1511,x1512),x1512)+P5(x1511,f14(x1512,a15))+P1(x1511,f14(x1512,a15))
% 0.57/0.68 [156]P1(x1561,x1562)+P2(f11(x1561,x1562),x1562)+~P1(x1561,f14(x1562,a15))+P5(x1561,f14(x1562,a15))
% 0.57/0.68 [161]~P1(x1611,x1612)+P9(f4(x1611,x1612),x1611,x1612)+P5(x1611,f14(x1612,a15))+P1(x1611,f14(x1612,a15))
% 0.57/0.68 [162]P1(x1621,x1622)+P7(f11(x1621,x1622),x1621,x1622)+~P1(x1621,f14(x1622,a15))+P5(x1621,f14(x1622,a15))
% 0.57/0.68 [177]~P5(x1771,x1772)+P9(f3(x1771,x1772),x1771,x1772)+P7(f3(x1771,x1772),x1771,x1772)+P5(x1771,f14(x1772,a15))
% 0.57/0.68 [142]~P3(x1421,x1422,x1423)+E(x1422,a28)+E(x1421,a2)+E(x1422,a21)
% 0.57/0.68 [143]~P3(x1432,x1431,x1433)+E(x1431,a21)+E(x1431,a28)+E(x1431,a26)
% 0.57/0.68 [163]~P3(x1631,x1632,x1633)+E(x1631,a2)+E(x1632,a21)+E(f25(f5(x1633,x1632,x1631)),x1631)
% 0.57/0.68 [164]~P3(x1643,x1641,x1642)+E(x1641,a21)+E(x1641,a26)+E(f25(f5(x1642,x1641,x1643)),x1643)
% 0.57/0.68 [185]~P3(x1851,x1852,x1853)+E(x1851,a2)+E(x1852,a21)+P1(f25(f5(x1853,x1852,x1851)),x1853)
% 0.57/0.68 [186]~P3(x1863,x1861,x1862)+E(x1861,a21)+E(x1861,a26)+P1(f25(f5(x1862,x1861,x1863)),x1862)
% 0.57/0.68 [146]P3(x1461,x1462,x1463)+~E(x1462,a21)+~E(x1461,f25(x1464))+~P1(f25(x1464),x1463)
% 0.57/0.68 [147]P3(x1471,x1472,x1473)+~E(x1472,a28)+~E(x1471,f25(x1474))+~P1(f25(x1474),x1473)
% 0.57/0.68 [166]~P3(x1662,x1661,x1663)+E(x1661,a28)+E(x1661,a26)+E(x1662,a27)+E(f25(f6(x1663,x1661,x1662)),x1662)
% 0.57/0.68 [168]~P3(x1682,x1681,x1683)+E(x1682,a27)+E(x1681,a28)+E(x1682,a2)+E(f25(f6(x1683,x1681,x1682)),x1682)
% 0.57/0.68 [180]~P3(x1802,x1801,x1803)+E(x1801,a26)+E(x1802,a27)+E(f25(f6(x1803,x1801,x1802)),x1802)+E(f25(f5(x1803,x1801,x1802)),x1802)
% 0.57/0.68 [182]~P3(x1821,x1823,x1822)+E(x1821,a27)+E(x1821,a2)+E(f25(f6(x1822,x1823,x1821)),x1821)+E(f25(f5(x1822,x1823,x1821)),x1821)
% 0.57/0.68 [187]~P3(x1871,x1872,x1873)+E(x1871,a27)+E(x1871,a2)+E(x1872,a28)+P1(f25(f6(x1873,x1872,x1871)),x1873)
% 0.57/0.68 [190]~P3(x1901,x1902,x1903)+E(x1902,a28)+E(x1901,a27)+E(x1902,a26)+P1(f25(f6(x1903,x1902,x1901)),x1903)
% 0.57/0.68 [196]~P3(x1962,x1961,x1963)+E(x1961,a26)+E(x1962,a27)+P1(f25(f5(x1963,x1961,x1962)),x1963)+E(f25(f6(x1963,x1961,x1962)),x1962)
% 0.57/0.68 [197]~P3(x1971,x1973,x1972)+E(x1971,a27)+E(x1971,a2)+P1(f25(f6(x1972,x1973,x1971)),x1972)+E(f25(f5(x1972,x1973,x1971)),x1971)
% 0.57/0.68 [200]~P3(x2001,x2002,x2003)+E(x2001,a27)+E(x2002,a26)+P1(f25(f6(x2003,x2002,x2001)),x2003)+E(f25(f5(x2003,x2002,x2001)),x2001)
% 0.57/0.68 [202]~P3(x2021,x2023,x2022)+E(x2021,a27)+E(x2021,a2)+P1(f25(f5(x2022,x2023,x2021)),x2022)+E(f25(f6(x2022,x2023,x2021)),x2021)
% 0.57/0.68 [203]~P3(x2031,x2033,x2032)+E(x2031,a27)+E(x2031,a2)+P1(f25(f6(x2032,x2033,x2031)),x2032)+P1(f25(f5(x2032,x2033,x2031)),x2032)
% 0.57/0.68 [205]~P3(x2051,x2052,x2053)+E(x2051,a27)+E(x2052,a26)+P1(f25(f6(x2053,x2052,x2051)),x2053)+P1(f25(f5(x2053,x2052,x2051)),x2053)
% 0.57/0.68 [175]~P6(x1751,x1755)+~P6(x1755,x1753)+~P9(x1754,x1752,x1755)+P11(x1751,x1752,x1753)+~P2(x1754,x1755)
% 0.57/0.68 [176]~P6(x1761,x1765)+~P6(x1765,x1763)+~P7(x1764,x1762,x1765)+P12(x1761,x1762,x1763)+~P2(x1764,x1765)
% 0.57/0.68 [207]~P7(x2075,x2074,x2072)+~P13(x2074,x2072,x2071,x2073)+~P2(x2075,x2072)+P11(x2072,x2074,f14(x2072,x2073))+~P6(a1,x2073)+P1(x2071,f14(x2072,x2073))
% 0.57/0.68 [208]~P9(x2085,x2084,x2082)+~P4(x2084,x2082,x2081,x2083)+~P2(x2085,x2082)+P12(x2082,x2084,f14(x2082,x2083))+~P6(a1,x2083)+P1(x2081,f14(x2082,x2083))
% 0.57/0.68 %EqnAxiom
% 0.57/0.68 [1]E(x11,x11)
% 0.57/0.68 [2]E(x22,x21)+~E(x21,x22)
% 0.57/0.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.57/0.68 [4]~E(x41,x42)+E(f14(x41,x43),f14(x42,x43))
% 0.57/0.68 [5]~E(x51,x52)+E(f14(x53,x51),f14(x53,x52))
% 0.57/0.68 [6]~E(x61,x62)+E(f25(x61),f25(x62))
% 0.57/0.68 [7]~E(x71,x72)+E(f6(x71,x73,x74),f6(x72,x73,x74))
% 0.57/0.68 [8]~E(x81,x82)+E(f6(x83,x81,x84),f6(x83,x82,x84))
% 0.57/0.68 [9]~E(x91,x92)+E(f6(x93,x94,x91),f6(x93,x94,x92))
% 0.57/0.68 [10]~E(x101,x102)+E(f5(x101,x103,x104),f5(x102,x103,x104))
% 0.57/0.68 [11]~E(x111,x112)+E(f5(x113,x111,x114),f5(x113,x112,x114))
% 0.57/0.68 [12]~E(x121,x122)+E(f5(x123,x124,x121),f5(x123,x124,x122))
% 0.57/0.68 [13]~E(x131,x132)+E(f4(x131,x133),f4(x132,x133))
% 0.57/0.68 [14]~E(x141,x142)+E(f4(x143,x141),f4(x143,x142))
% 0.57/0.68 [15]~E(x151,x152)+E(f9(x151,x153,x154),f9(x152,x153,x154))
% 0.57/0.68 [16]~E(x161,x162)+E(f9(x163,x161,x164),f9(x163,x162,x164))
% 0.57/0.68 [17]~E(x171,x172)+E(f9(x173,x174,x171),f9(x173,x174,x172))
% 0.57/0.68 [18]~E(x181,x182)+E(f7(x181,x183,x184),f7(x182,x183,x184))
% 0.57/0.68 [19]~E(x191,x192)+E(f7(x193,x191,x194),f7(x193,x192,x194))
% 0.57/0.68 [20]~E(x201,x202)+E(f7(x203,x204,x201),f7(x203,x204,x202))
% 0.57/0.68 [21]~E(x211,x212)+E(f3(x211,x213),f3(x212,x213))
% 0.57/0.68 [22]~E(x221,x222)+E(f3(x223,x221),f3(x223,x222))
% 0.57/0.68 [23]~E(x231,x232)+E(f11(x231,x233),f11(x232,x233))
% 0.57/0.68 [24]~E(x241,x242)+E(f11(x243,x241),f11(x243,x242))
% 0.57/0.68 [25]~E(x251,x252)+E(f12(x251,x253),f12(x252,x253))
% 0.57/0.68 [26]~E(x261,x262)+E(f12(x263,x261),f12(x263,x262))
% 0.57/0.68 [27]~E(x271,x272)+E(f13(x271,x273),f13(x272,x273))
% 0.57/0.68 [28]~E(x281,x282)+E(f13(x283,x281),f13(x283,x282))
% 0.57/0.68 [29]~E(x291,x292)+E(f8(x291,x293,x294),f8(x292,x293,x294))
% 0.57/0.68 [30]~E(x301,x302)+E(f8(x303,x301,x304),f8(x303,x302,x304))
% 0.57/0.68 [31]~E(x311,x312)+E(f8(x313,x314,x311),f8(x313,x314,x312))
% 0.57/0.68 [32]~E(x321,x322)+E(f10(x321,x323,x324),f10(x322,x323,x324))
% 0.57/0.68 [33]~E(x331,x332)+E(f10(x333,x331,x334),f10(x333,x332,x334))
% 0.57/0.68 [34]~E(x341,x342)+E(f10(x343,x344,x341),f10(x343,x344,x342))
% 0.57/0.68 [35]P1(x352,x353)+~E(x351,x352)+~P1(x351,x353)
% 0.57/0.68 [36]P1(x363,x362)+~E(x361,x362)+~P1(x363,x361)
% 0.57/0.68 [37]P4(x372,x373,x374,x375)+~E(x371,x372)+~P4(x371,x373,x374,x375)
% 0.57/0.68 [38]P4(x383,x382,x384,x385)+~E(x381,x382)+~P4(x383,x381,x384,x385)
% 0.57/0.68 [39]P4(x393,x394,x392,x395)+~E(x391,x392)+~P4(x393,x394,x391,x395)
% 0.57/0.68 [40]P4(x403,x404,x405,x402)+~E(x401,x402)+~P4(x403,x404,x405,x401)
% 0.57/0.68 [41]P9(x412,x413,x414)+~E(x411,x412)+~P9(x411,x413,x414)
% 0.57/0.68 [42]P9(x423,x422,x424)+~E(x421,x422)+~P9(x423,x421,x424)
% 0.57/0.68 [43]P9(x433,x434,x432)+~E(x431,x432)+~P9(x433,x434,x431)
% 0.57/0.68 [44]P2(x442,x443)+~E(x441,x442)+~P2(x441,x443)
% 0.57/0.68 [45]P2(x453,x452)+~E(x451,x452)+~P2(x453,x451)
% 0.57/0.68 [46]P6(x462,x463)+~E(x461,x462)+~P6(x461,x463)
% 0.57/0.68 [47]P6(x473,x472)+~E(x471,x472)+~P6(x473,x471)
% 0.57/0.68 [48]P3(x482,x483,x484)+~E(x481,x482)+~P3(x481,x483,x484)
% 0.57/0.68 [49]P3(x493,x492,x494)+~E(x491,x492)+~P3(x493,x491,x494)
% 0.57/0.68 [50]P3(x503,x504,x502)+~E(x501,x502)+~P3(x503,x504,x501)
% 0.57/0.68 [51]P5(x512,x513)+~E(x511,x512)+~P5(x511,x513)
% 0.57/0.68 [52]P5(x523,x522)+~E(x521,x522)+~P5(x523,x521)
% 0.57/0.68 [53]P11(x532,x533,x534)+~E(x531,x532)+~P11(x531,x533,x534)
% 0.57/0.68 [54]P11(x543,x542,x544)+~E(x541,x542)+~P11(x543,x541,x544)
% 0.57/0.68 [55]P11(x553,x554,x552)+~E(x551,x552)+~P11(x553,x554,x551)
% 0.57/0.68 [56]P12(x562,x563,x564)+~E(x561,x562)+~P12(x561,x563,x564)
% 0.57/0.68 [57]P12(x573,x572,x574)+~E(x571,x572)+~P12(x573,x571,x574)
% 0.57/0.68 [58]P12(x583,x584,x582)+~E(x581,x582)+~P12(x583,x584,x581)
% 0.57/0.68 [59]P7(x592,x593,x594)+~E(x591,x592)+~P7(x591,x593,x594)
% 0.57/0.68 [60]P7(x603,x602,x604)+~E(x601,x602)+~P7(x603,x601,x604)
% 0.57/0.68 [61]P7(x613,x614,x612)+~E(x611,x612)+~P7(x613,x614,x611)
% 0.57/0.68 [62]P8(x622,x623)+~E(x621,x622)+~P8(x621,x623)
% 0.57/0.68 [63]P8(x633,x632)+~E(x631,x632)+~P8(x633,x631)
% 0.57/0.68 [64]P10(x642,x643,x644)+~E(x641,x642)+~P10(x641,x643,x644)
% 0.57/0.68 [65]P10(x653,x652,x654)+~E(x651,x652)+~P10(x653,x651,x654)
% 0.57/0.68 [66]P10(x663,x664,x662)+~E(x661,x662)+~P10(x663,x664,x661)
% 0.57/0.68 [67]P13(x672,x673,x674,x675)+~E(x671,x672)+~P13(x671,x673,x674,x675)
% 0.57/0.68 [68]P13(x683,x682,x684,x685)+~E(x681,x682)+~P13(x683,x681,x684,x685)
% 0.57/0.68 [69]P13(x693,x694,x692,x695)+~E(x691,x692)+~P13(x693,x694,x691,x695)
% 0.57/0.68 [70]P13(x703,x704,x705,x702)+~E(x701,x702)+~P13(x703,x704,x705,x701)
% 0.57/0.68
% 0.57/0.68 %-------------------------------------------
% 0.57/0.68 cnf(212,plain,
% 0.57/0.68 (P2(a21,x2121)+~P1(a2,x2121)+~P1(f25(a16),x2121)),
% 0.57/0.68 inference(equality_inference,[],[134])).
% 0.57/0.68 cnf(214,plain,
% 0.57/0.68 ($false),
% 0.57/0.68 inference(scs_inference,[],[91,81,83,212]),
% 0.57/0.68 ['proof']).
% 0.57/0.68 % SZS output end Proof
% 0.57/0.68 % Total time :0.000000s
%------------------------------------------------------------------------------