%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET091+1 : TPTP v8.2.0. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n027.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 14:20:38 EDT 2024
% Result : Theorem 60.27s 60.31s
% Output : CNFRefutation 60.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SET091+1 : TPTP v8.2.0. Bugfixed v7.3.0.
% 0.00/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n027.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Sun Jun 23 14:02:09 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 60.27/60.30 %-------------------------------------------
% 60.27/60.30 % File :CSE---1.7
% 60.27/60.30 % Problem :theBenchmark
% 60.27/60.30 % Transform :cnf
% 60.27/60.30 % Format :tptp:raw
% 60.27/60.30 % Command :java -jar mcs_scs.jar %d %s
% 60.27/60.30
% 60.27/60.30 % Result :Theorem 59.680000s
% 60.27/60.30 % Output :CNFRefutation 59.680000s
% 60.27/60.30 %-------------------------------------------
% 60.27/60.31 %--------------------------------------------------------------------------
% 60.27/60.31 % File : SET091+1 : TPTP v8.2.0. Bugfixed v7.3.0.
% 60.27/60.31 % Domain : Set Theory
% 60.27/60.31 % Problem : Uniqueness of member_of when X is not a singleton of a set
% 60.27/60.31 % Version : [Qua92] axioms : Reduced & Augmented > Complete.
% 60.27/60.31 % English :
% 60.27/60.31
% 60.27/60.31 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 60.27/60.31 % : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
% 60.27/60.31 % Source : [Qua92]
% 60.27/60.31 % Names :
% 60.27/60.31
% 60.27/60.31 % Status : Theorem
% 60.27/60.31 % Rating : 0.17 v8.2.0, 0.19 v8.1.0, 0.28 v7.4.0, 0.17 v7.3.0
% 60.27/60.31 % Syntax : Number of formulae : 48 ( 16 unt; 0 def)
% 60.27/60.31 % Number of atoms : 112 ( 26 equ)
% 60.27/60.31 % Maximal formula atoms : 4 ( 2 avg)
% 60.27/60.31 % Number of connectives : 70 ( 6 ~; 5 |; 28 &)
% 60.27/60.31 % ( 19 <=>; 12 =>; 0 <=; 0 <~>)
% 60.27/60.31 % Maximal formula depth : 8 ( 4 avg)
% 60.27/60.31 % Maximal term depth : 4 ( 1 avg)
% 60.27/60.31 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty)
% 60.27/60.31 % Number of functors : 27 ( 27 usr; 5 con; 0-3 aty)
% 60.27/60.31 % Number of variables : 93 ( 87 !; 6 ?)
% 60.27/60.31 % SPC : FOF_THM_RFO_SEQ
% 60.27/60.31
% 60.27/60.31 % Comments :
% 60.27/60.31 % Bugfixed : v5.4.0 - Bugfixes to SET005+0 axiom file.
% 60.27/60.31 % : v7.3.0 - Added axioms for member_of
% 60.27/60.31 %--------------------------------------------------------------------------
% 60.27/60.31 %----Include set theory axioms
% 60.27/60.31 include('Axioms/SET005+0.ax').
% 60.27/60.31 %--------------------------------------------------------------------------
% 60.27/60.31 %----Axioms to define member_of, based on SET086+1
% 60.27/60.31 fof(member_singleton_universal,axiom,
% 60.27/60.31 ! [Y] :
% 60.27/60.31 ( member(Y,universal_class)
% 60.27/60.31 => member(member_of(singleton(Y)),universal_class) ) ).
% 60.27/60.31
% 60.27/60.31 fof(member_singleton_singleton,axiom,
% 60.27/60.31 ! [Y] :
% 60.27/60.31 ( member(Y,universal_class)
% 60.27/60.31 => singleton(member_of(singleton(Y))) = singleton(Y) ) ).
% 60.27/60.31
% 60.27/60.31 fof(member_universal_self,axiom,
% 60.27/60.31 ! [X] :
% 60.27/60.31 ( member(member_of(X),universal_class)
% 60.27/60.31 | member_of(X) = X ) ).
% 60.27/60.31
% 60.27/60.31 fof(singleton_self,axiom,
% 60.27/60.31 ! [X] :
% 60.27/60.31 ( singleton(member_of(X)) = X
% 60.27/60.31 | member_of(X) = X ) ).
% 60.27/60.31
% 60.27/60.31 %----SS8: Uniqueness of member_of when X is not a singleton of a set
% 60.27/60.31 %----Two theorems combined in one. Like SS6 it could be broken up.
% 60.27/60.31 fof(member_when_not_a_singleton,conjecture,
% 60.27/60.31 ! [X,U] :
% 60.27/60.31 ( ( ~ ? [Y] :
% 60.27/60.31 ( member(Y,universal_class)
% 60.27/60.31 & X = singleton(Y) )
% 60.27/60.31 & X = U )
% 60.27/60.31 => member_of(X) = U ) ).
% 60.27/60.31
% 60.27/60.31 %--------------------------------------------------------------------------
% 60.27/60.31 %-------------------------------------------
% 60.27/60.31 % Proof found
% 60.27/60.31 % SZS status Theorem for theBenchmark
% 60.27/60.31 % SZS output start Proof
% 60.27/60.31 %ClaNum:126(EqnAxiom:38)
% 60.27/60.31 %VarNum:628(SingletonVarNum:174)
% 60.27/60.31 %MaxLitNum:4
% 60.27/60.31 %MaxfuncDepth:13
% 60.27/60.31 %SharedTerms:19
% 60.27/60.31 %goalClause: 39 50 65
% 60.27/60.31 %singleGoalClaCount:2
% 60.27/60.31 [39]E(a1,a2)
% 60.27/60.31 [40]P1(a3)
% 60.27/60.31 [41]P2(a10)
% 60.27/60.31 [42]P4(a3,a15)
% 60.27/60.31 [44]P5(a4,f5(a15,a15))
% 60.27/60.31 [45]P5(a16,f5(a15,a15))
% 60.27/60.31 [50]~E(f20(a2),a1)
% 60.27/60.31 [43]P5(x431,a15)
% 60.27/60.31 [51]~P4(x511,a23)
% 60.27/60.31 [48]P5(f17(x481),f5(f5(a15,a15),a15))
% 60.27/60.31 [49]P5(f18(x491),f5(f5(a15,a15),a15))
% 60.27/60.31 [46]P4(f28(x461,x462),a15)
% 60.27/60.31 [47]P5(f6(x471,x472),f5(a15,a15))
% 60.27/60.31 [54]~P1(x541)+P5(a3,x541)
% 60.27/60.31 [55]~P1(x551)+P4(a23,x551)
% 60.27/60.31 [56]E(x561,a23)+P4(f11(x561),a15)
% 60.27/60.31 [57]P4(f11(x571),x571)+E(x571,a23)
% 60.27/60.31 [58]P3(f11(x581),x581)+E(x581,a23)
% 60.27/60.31 [59]E(f20(x591),x591)+P4(f20(x591),a15)
% 60.27/60.31 [61]~P4(x611,a15)+P4(f26(x611),a15)
% 60.27/60.31 [62]~P4(x621,a15)+P4(f24(x621),a15)
% 60.27/60.31 [63]~P4(x631,a21)+P4(f12(x631),a15)
% 60.27/60.31 [64]~P2(x641)+P5(x641,f5(a15,a15))
% 60.27/60.31 [65]~P4(x651,a15)+~E(f28(x651,x651),a2)
% 60.27/60.31 [60]E(f20(x601),x601)+E(f28(f20(x601),f20(x601)),x601)
% 60.27/60.31 [92]~P4(x921,a15)+P4(f20(f28(x921,x921)),a15)
% 60.27/60.31 [95]~P4(x951,a15)+E(f28(f20(f28(x951,x951)),f20(f28(x951,x951))),f28(x951,x951))
% 60.27/60.31 [98]~P4(x981,a21)+E(f28(f28(f12(x981),f12(x981)),f28(f12(x981),f28(f12(x981),f12(x981)))),x981)
% 60.27/60.31 [99]~P2(x991)+P5(f6(x991,f8(f18(f5(x991,a15)))),a21)
% 60.27/60.31 [115]~P1(x1151)+P5(f8(f8(f18(f5(f22(a16,f5(x1151,a15)),a15)))),x1151)
% 60.27/60.31 [53]~E(x531,x532)+P5(x531,x532)
% 60.27/60.31 [66]P4(x661,a15)+~P4(x661,f7(x662))
% 60.27/60.31 [67]P4(x671,a15)+~P4(x671,f8(x672))
% 60.27/60.31 [68]P4(x681,a15)+~P4(x681,f24(x682))
% 60.27/60.31 [69]P5(x691,x692)+~P4(x691,f24(x692))
% 60.27/60.31 [71]P5(x711,x712)+P4(f9(x711,x712),x711)
% 60.27/60.31 [72]P3(x721,x722)+P4(f14(x721,x722),x722)
% 60.27/60.31 [73]P3(x731,x732)+P4(f14(x731,x732),x731)
% 60.27/60.31 [74]~P4(x741,x742)+~P4(x741,f7(x742))
% 60.27/60.31 [85]~P4(x851,f26(x852))+P4(x851,f13(x851,x852))
% 60.27/60.31 [86]~P4(x861,f26(x862))+P4(f13(x861,x862),x862)
% 60.27/60.31 [90]P5(x901,x902)+~P4(f9(x901,x902),x902)
% 60.27/60.31 [96]~P4(x962,f8(x961))+~E(f22(x961,f5(f28(x962,x962),a15)),a23)
% 60.27/60.31 [106]P4(x1061,a15)+~P4(f28(f28(x1062,x1062),f28(x1062,f28(x1061,x1061))),a4)
% 60.27/60.31 [107]P4(x1071,a15)+~P4(f28(f28(x1072,x1072),f28(x1072,f28(x1071,x1071))),a16)
% 60.27/60.31 [108]P4(x1081,a15)+~P4(f28(f28(x1081,x1081),f28(x1081,f28(x1082,x1082))),a16)
% 60.27/60.31 [109]P4(x1091,x1092)+~P4(f28(f28(x1091,x1091),f28(x1091,f28(x1092,x1092))),a4)
% 60.27/60.31 [110]E(f27(x1101,f28(x1101,x1101)),x1102)+~P4(f28(f28(x1101,x1101),f28(x1101,f28(x1102,x1102))),a16)
% 60.27/60.31 [77]~P4(x771,x773)+P4(x771,f27(x772,x773))
% 60.27/60.31 [78]~P4(x781,x782)+P4(x781,f27(x782,x783))
% 60.27/60.31 [87]P4(x871,a15)+~P4(x871,f28(x872,x873))
% 60.27/60.31 [88]P4(x881,x882)+~P4(x881,f22(x883,x882))
% 60.27/60.31 [89]P4(x891,x892)+~P4(x891,f22(x892,x893))
% 60.27/60.31 [100]~P4(x1001,f5(x1002,x1003))+E(f28(f28(f19(x1001),f19(x1001)),f28(f19(x1001),f28(f25(x1001),f25(x1001)))),x1001)
% 60.27/60.31 [111]P4(x1111,a15)+~P4(f28(f28(x1111,x1111),f28(x1111,f28(x1112,x1112))),f6(x1113,x1114))
% 60.27/60.31 [112]P4(x1121,x1122)+~P4(f28(f28(x1123,x1123),f28(x1123,f28(x1121,x1121))),f5(x1124,x1122))
% 60.27/60.31 [113]P4(x1131,x1132)+~P4(f28(f28(x1131,x1131),f28(x1131,f28(x1133,x1133))),f5(x1132,x1134))
% 60.27/60.31 [119]~P4(f28(f28(f28(f28(x1193,x1193),f28(x1193,f28(x1191,x1191))),f28(f28(x1193,x1193),f28(x1193,f28(x1191,x1191)))),f28(f28(f28(x1193,x1193),f28(x1193,f28(x1191,x1191))),f28(x1192,x1192))),f17(x1194))+P4(f28(f28(f28(f28(x1191,x1191),f28(x1191,f28(x1192,x1192))),f28(f28(x1191,x1191),f28(x1191,f28(x1192,x1192)))),f28(f28(f28(x1191,x1191),f28(x1191,f28(x1192,x1192))),f28(x1193,x1193))),x1194)
% 60.27/60.31 [120]~P4(f28(f28(f28(f28(x1202,x1202),f28(x1202,f28(x1201,x1201))),f28(f28(x1202,x1202),f28(x1202,f28(x1201,x1201)))),f28(f28(f28(x1202,x1202),f28(x1202,f28(x1201,x1201))),f28(x1203,x1203))),f18(x1204))+P4(f28(f28(f28(f28(x1201,x1201),f28(x1201,f28(x1202,x1202))),f28(f28(x1201,x1201),f28(x1201,f28(x1202,x1202)))),f28(f28(f28(x1201,x1201),f28(x1201,f28(x1202,x1202))),f28(x1203,x1203))),x1204)
% 60.27/60.31 [121]~P4(f28(f28(f28(f28(x1211,x1211),f28(x1211,f28(x1212,x1212))),f28(f28(x1211,x1211),f28(x1211,f28(x1212,x1212)))),f28(f28(f28(x1211,x1211),f28(x1211,f28(x1212,x1212))),f28(x1213,x1213))),f17(x1214))+P4(f28(f28(f28(f28(x1211,x1211),f28(x1211,f28(x1212,x1212))),f28(f28(x1211,x1211),f28(x1211,f28(x1212,x1212)))),f28(f28(f28(x1211,x1211),f28(x1211,f28(x1212,x1212))),f28(x1213,x1213))),f5(f5(a15,a15),a15))
% 60.27/60.31 [122]~P4(f28(f28(f28(f28(x1221,x1221),f28(x1221,f28(x1222,x1222))),f28(f28(x1221,x1221),f28(x1221,f28(x1222,x1222)))),f28(f28(f28(x1221,x1221),f28(x1221,f28(x1222,x1222))),f28(x1223,x1223))),f18(x1224))+P4(f28(f28(f28(f28(x1221,x1221),f28(x1221,f28(x1222,x1222))),f28(f28(x1221,x1221),f28(x1221,f28(x1222,x1222)))),f28(f28(f28(x1221,x1221),f28(x1221,f28(x1222,x1222))),f28(x1223,x1223))),f5(f5(a15,a15),a15))
% 60.27/60.31 [125]~P4(f28(f28(x1254,x1254),f28(x1254,f28(x1251,x1251))),f6(x1252,x1253))+P4(x1251,f8(f8(f18(f5(f22(x1252,f5(f8(f8(f18(f5(f22(x1253,f5(f28(x1254,x1254),a15)),a15)))),a15)),a15)))))
% 60.27/60.31 [114]P2(x1141)+~P5(x1141,f5(a15,a15))+~P5(f6(x1141,f8(f18(f5(x1141,a15)))),a21)
% 60.27/60.31 [117]P1(x1171)+~P4(a23,x1171)+~P5(f8(f8(f18(f5(f22(a16,f5(x1171,a15)),a15)))),x1171)
% 60.27/60.31 [118]~P4(x1181,a15)+E(x1181,a23)+P4(f26(f8(f8(f18(f5(f22(a10,f5(f28(x1181,x1181),a15)),a15))))),x1181)
% 60.27/60.31 [70]~P5(x702,x701)+~P5(x701,x702)+E(x701,x702)
% 60.27/60.31 [75]P4(x751,x752)+P4(x751,f7(x752))+~P4(x751,a15)
% 60.27/60.31 [79]~P5(x791,x792)+~P4(x791,a15)+P4(x791,f24(x792))
% 60.27/60.32 [94]P4(x942,f8(x941))+~P4(x942,a15)+E(f22(x941,f5(f28(x942,x942),a15)),a23)
% 60.27/60.32 [97]~P4(x972,a15)+P4(x971,a21)+~E(x971,f28(f28(x972,x972),f28(x972,f28(x972,x972))))
% 60.27/60.32 [103]~P4(x1031,x1032)+~P4(x1032,a15)+P4(f28(f28(x1031,x1031),f28(x1031,f28(x1032,x1032))),a4)
% 60.27/60.32 [101]~P4(x1012,a15)+~P4(x1011,a15)+E(f19(f28(f28(x1011,x1011),f28(x1011,f28(x1012,x1012)))),x1011)
% 60.27/60.32 [102]~P4(x1022,a15)+~P4(x1021,a15)+E(f25(f28(f28(x1021,x1021),f28(x1021,f28(x1022,x1022)))),x1022)
% 60.27/60.32 [116]~P2(x1161)+~P4(x1162,a15)+P4(f8(f8(f18(f5(f22(x1161,f5(x1162,a15)),a15)))),a15)
% 60.27/60.32 [76]~P4(x761,x763)+P4(x761,x762)+~P5(x763,x762)
% 60.27/60.32 [84]~P3(x843,x842)+~P4(x841,x842)+~P4(x841,x843)
% 60.27/60.32 [80]~E(x801,x803)+~P4(x801,a15)+P4(x801,f28(x802,x803))
% 60.27/60.32 [81]~E(x811,x812)+~P4(x811,a15)+P4(x811,f28(x812,x813))
% 60.27/60.32 [82]~P4(x821,x823)+~P4(x823,x822)+P4(x821,f26(x822))
% 60.27/60.32 [83]E(x831,x832)+E(x831,x833)+~P4(x831,f28(x833,x832))
% 60.27/60.32 [91]~P4(x911,x913)+~P4(x911,x912)+P4(x911,f22(x912,x913))
% 60.27/60.32 [93]P4(x931,x932)+P4(x931,x933)+~P4(x931,f27(x933,x932))
% 60.27/60.32 [104]~P4(x1042,x1044)+~P4(x1041,x1043)+P4(f28(f28(x1041,x1041),f28(x1041,f28(x1042,x1042))),f5(x1043,x1044))
% 60.27/60.32 [123]~P4(f28(f28(f28(f28(x1232,x1232),f28(x1232,f28(x1233,x1233))),f28(f28(x1232,x1232),f28(x1232,f28(x1233,x1233)))),f28(f28(f28(x1232,x1232),f28(x1232,f28(x1233,x1233))),f28(x1231,x1231))),x1234)+P4(f28(f28(f28(f28(x1231,x1231),f28(x1231,f28(x1232,x1232))),f28(f28(x1231,x1231),f28(x1231,f28(x1232,x1232)))),f28(f28(f28(x1231,x1231),f28(x1231,f28(x1232,x1232))),f28(x1233,x1233))),f17(x1234))+~P4(f28(f28(f28(f28(x1231,x1231),f28(x1231,f28(x1232,x1232))),f28(f28(x1231,x1231),f28(x1231,f28(x1232,x1232)))),f28(f28(f28(x1231,x1231),f28(x1231,f28(x1232,x1232))),f28(x1233,x1233))),f5(f5(a15,a15),a15))
% 60.27/60.32 [124]~P4(f28(f28(f28(f28(x1242,x1242),f28(x1242,f28(x1241,x1241))),f28(f28(x1242,x1242),f28(x1242,f28(x1241,x1241)))),f28(f28(f28(x1242,x1242),f28(x1242,f28(x1241,x1241))),f28(x1243,x1243))),x1244)+P4(f28(f28(f28(f28(x1241,x1241),f28(x1241,f28(x1242,x1242))),f28(f28(x1241,x1241),f28(x1241,f28(x1242,x1242)))),f28(f28(f28(x1241,x1241),f28(x1241,f28(x1242,x1242))),f28(x1243,x1243))),f18(x1244))+~P4(f28(f28(f28(f28(x1241,x1241),f28(x1241,f28(x1242,x1242))),f28(f28(x1241,x1241),f28(x1241,f28(x1242,x1242)))),f28(f28(f28(x1241,x1241),f28(x1241,f28(x1242,x1242))),f28(x1243,x1243))),f5(f5(a15,a15),a15))
% 60.27/60.32 [126]~P4(x1261,a15)+P4(f28(f28(x1261,x1261),f28(x1261,f28(x1262,x1262))),f6(x1263,x1264))+~P4(x1262,f8(f8(f18(f5(f22(x1263,f5(f8(f8(f18(f5(f22(x1264,f5(f28(x1261,x1261),a15)),a15)))),a15)),a15)))))
% 60.27/60.32 [105]~P4(x1052,a15)+~P4(x1051,a15)+~E(f27(x1051,f28(x1051,x1051)),x1052)+P4(f28(f28(x1051,x1051),f28(x1051,f28(x1052,x1052))),a16)
% 60.27/60.32 %EqnAxiom
% 60.27/60.32 [1]E(x11,x11)
% 60.27/60.32 [2]E(x22,x21)+~E(x21,x22)
% 60.27/60.32 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.27/60.32 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 60.27/60.32 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 60.27/60.32 [6]~E(x61,x62)+E(f8(x61),f8(x62))
% 60.27/60.32 [7]~E(x71,x72)+E(f28(x71,x73),f28(x72,x73))
% 60.27/60.32 [8]~E(x81,x82)+E(f28(x83,x81),f28(x83,x82))
% 60.27/60.32 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93))
% 60.27/60.32 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102))
% 60.27/60.32 [11]~E(x111,x112)+E(f18(x111),f18(x112))
% 60.27/60.32 [12]~E(x121,x122)+E(f17(x121),f17(x122))
% 60.27/60.32 [13]~E(x131,x132)+E(f25(x131),f25(x132))
% 60.27/60.32 [14]~E(x141,x142)+E(f22(x141,x143),f22(x142,x143))
% 60.27/60.32 [15]~E(x151,x152)+E(f22(x153,x151),f22(x153,x152))
% 60.27/60.32 [16]~E(x161,x162)+E(f27(x161,x163),f27(x162,x163))
% 60.27/60.32 [17]~E(x171,x172)+E(f27(x173,x171),f27(x173,x172))
% 60.27/60.32 [18]~E(x181,x182)+E(f19(x181),f19(x182))
% 60.27/60.32 [19]~E(x191,x192)+E(f12(x191),f12(x192))
% 60.27/60.32 [20]~E(x201,x202)+E(f20(x201),f20(x202))
% 60.27/60.32 [21]~E(x211,x212)+E(f11(x211),f11(x212))
% 60.27/60.32 [22]~E(x221,x222)+E(f14(x221,x223),f14(x222,x223))
% 60.27/60.32 [23]~E(x231,x232)+E(f14(x233,x231),f14(x233,x232))
% 60.27/60.32 [24]~E(x241,x242)+E(f9(x241,x243),f9(x242,x243))
% 60.27/60.32 [25]~E(x251,x252)+E(f9(x253,x251),f9(x253,x252))
% 60.27/60.32 [26]~E(x261,x262)+E(f26(x261),f26(x262))
% 60.27/60.32 [27]~E(x271,x272)+E(f24(x271),f24(x272))
% 60.27/60.32 [28]~E(x281,x282)+E(f13(x281,x283),f13(x282,x283))
% 60.27/60.32 [29]~E(x291,x292)+E(f13(x293,x291),f13(x293,x292))
% 60.27/60.32 [30]~E(x301,x302)+E(f7(x301),f7(x302))
% 60.27/60.32 [31]~P1(x311)+P1(x312)+~E(x311,x312)
% 60.27/60.32 [32]~P2(x321)+P2(x322)+~E(x321,x322)
% 60.27/60.32 [33]P4(x332,x333)+~E(x331,x332)+~P4(x331,x333)
% 60.27/60.32 [34]P4(x343,x342)+~E(x341,x342)+~P4(x343,x341)
% 60.27/60.32 [35]P5(x352,x353)+~E(x351,x352)+~P5(x351,x353)
% 60.27/60.32 [36]P5(x363,x362)+~E(x361,x362)+~P5(x363,x361)
% 60.27/60.32 [37]P3(x372,x373)+~E(x371,x372)+~P3(x371,x373)
% 60.27/60.32 [38]P3(x383,x382)+~E(x381,x382)+~P3(x383,x381)
% 60.27/60.32
% 60.27/60.32 %-------------------------------------------
% 60.27/60.32 cnf(127,plain,
% 60.27/60.32 (P5(x1271,x1271)),
% 60.27/60.32 inference(equality_inference,[],[53])).
% 60.27/60.32 cnf(128,plain,
% 60.27/60.32 (~P4(x1281,a15)+P4(x1281,f28(x1282,x1281))),
% 60.27/60.32 inference(equality_inference,[],[80])).
% 60.27/60.32 cnf(129,plain,
% 60.27/60.32 (~P4(x1291,a15)+P4(x1291,f28(x1291,x1292))),
% 60.27/60.32 inference(equality_inference,[],[81])).
% 60.27/60.32 cnf(130,plain,
% 60.27/60.32 (~P4(x1301,a15)+P4(f28(f28(x1301,x1301),f28(x1301,f28(x1301,x1301))),a21)),
% 60.27/60.32 inference(equality_inference,[],[97])).
% 60.27/60.32 cnf(132,plain,
% 60.27/60.32 (P4(a3,f28(x1321,a3))),
% 60.27/60.32 inference(scs_inference,[],[42,128])).
% 60.27/60.32 cnf(134,plain,
% 60.27/60.32 (P4(a3,f28(a3,x1341))),
% 60.27/60.32 inference(scs_inference,[],[42,128,129])).
% 60.27/60.32 cnf(136,plain,
% 60.27/60.32 (E(a2,a1)),
% 60.27/60.32 inference(scs_inference,[],[39,42,128,129,2])).
% 60.27/60.32 cnf(137,plain,
% 60.27/60.32 (~P1(a23)),
% 60.27/60.32 inference(scs_inference,[],[39,51,42,128,129,2,55])).
% 60.27/60.32 cnf(138,plain,
% 60.27/60.33 (~P4(x1381,a23)),
% 60.27/60.33 inference(rename_variables,[],[51])).
% 60.27/60.33 cnf(140,plain,
% 60.27/60.33 (P5(a23,x1401)),
% 60.27/60.33 inference(scs_inference,[],[39,51,138,42,128,129,2,55,71])).
% 60.27/60.33 cnf(141,plain,
% 60.27/60.33 (~P4(x1411,a23)),
% 60.27/60.33 inference(rename_variables,[],[51])).
% 60.27/60.33 cnf(143,plain,
% 60.27/60.33 (P3(x1431,a23)),
% 60.27/60.33 inference(scs_inference,[],[39,51,138,141,42,128,129,2,55,71,72])).
% 60.27/60.33 cnf(144,plain,
% 60.27/60.33 (~P4(x1441,a23)),
% 60.27/60.33 inference(rename_variables,[],[51])).
% 60.27/60.33 cnf(146,plain,
% 60.27/60.33 (P3(a23,x1461)),
% 60.27/60.33 inference(scs_inference,[],[39,51,138,141,144,42,128,129,2,55,71,72,73])).
% 60.27/60.33 cnf(147,plain,
% 60.27/60.33 (~P4(x1471,a23)),
% 60.27/60.33 inference(rename_variables,[],[51])).
% 60.27/60.33 cnf(149,plain,
% 60.27/60.33 (~P4(x1491,f26(a23))),
% 60.27/60.33 inference(scs_inference,[],[39,51,138,141,144,147,42,128,129,2,55,71,72,73,86])).
% 60.27/60.33 cnf(150,plain,
% 60.27/60.33 (~P4(x1501,a23)),
% 60.27/60.33 inference(rename_variables,[],[51])).
% 60.27/60.33 cnf(152,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x1521,x1521),f28(x1521,f28(x1522,x1522))),f28(f28(x1521,x1521),f28(x1521,f28(x1522,x1522)))),f28(f28(f28(x1521,x1521),f28(x1521,f28(x1522,x1522))),f28(x1523,x1523))),f17(a23))),
% 60.27/60.33 inference(scs_inference,[],[39,51,138,141,144,147,150,42,128,129,2,55,71,72,73,86,119])).
% 60.27/60.33 cnf(153,plain,
% 60.27/60.33 (~P4(x1531,a23)),
% 60.27/60.33 inference(rename_variables,[],[51])).
% 60.27/60.33 cnf(155,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x1551,x1551),f28(x1551,f28(x1552,x1552))),f28(f28(x1551,x1551),f28(x1551,f28(x1552,x1552)))),f28(f28(f28(x1551,x1551),f28(x1551,f28(x1552,x1552))),f28(x1553,x1553))),f18(a23))),
% 60.27/60.33 inference(scs_inference,[],[39,51,138,141,144,147,150,153,42,128,129,2,55,71,72,73,86,119,120])).
% 60.27/60.33 cnf(156,plain,
% 60.27/60.33 (~P4(x1561,a23)),
% 60.27/60.33 inference(rename_variables,[],[51])).
% 60.27/60.33 cnf(158,plain,
% 60.27/60.33 (~E(f20(a2),a2)),
% 60.27/60.33 inference(scs_inference,[],[39,50,51,138,141,144,147,150,153,42,128,129,2,55,71,72,73,86,119,120,3])).
% 60.27/60.33 cnf(159,plain,
% 60.27/60.33 (~E(a15,a23)),
% 60.27/60.33 inference(scs_inference,[],[39,50,51,138,141,144,147,150,153,156,42,128,129,2,55,71,72,73,86,119,120,3,34])).
% 60.27/60.33 cnf(162,plain,
% 60.27/60.33 (P5(x1621,x1621)),
% 60.27/60.33 inference(rename_variables,[],[127])).
% 60.27/60.33 cnf(164,plain,
% 60.27/60.33 (P5(x1641,x1641)),
% 60.27/60.33 inference(rename_variables,[],[127])).
% 60.27/60.33 cnf(165,plain,
% 60.27/60.33 (P4(a3,f24(a3))),
% 60.27/60.33 inference(scs_inference,[],[39,50,127,162,164,51,138,141,144,147,150,153,156,42,128,129,2,55,71,72,73,86,119,120,3,34,35,36,79])).
% 60.27/60.33 cnf(168,plain,
% 60.27/60.33 (P4(f11(a15),a15)),
% 60.27/60.33 inference(scs_inference,[],[39,50,127,162,164,51,138,141,144,147,150,153,156,42,128,129,2,55,71,72,73,86,119,120,3,34,35,36,79,57])).
% 60.27/60.33 cnf(170,plain,
% 60.27/60.33 (P3(f11(a15),a15)),
% 60.27/60.33 inference(scs_inference,[],[39,50,127,162,164,51,138,141,144,147,150,153,156,42,128,129,2,55,71,72,73,86,119,120,3,34,35,36,79,57,58])).
% 60.27/60.33 cnf(184,plain,
% 60.27/60.33 (P3(x1841,f26(a23))),
% 60.27/60.33 inference(scs_inference,[],[149,72])).
% 60.27/60.33 cnf(185,plain,
% 60.27/60.33 (~P4(x1851,f26(a23))),
% 60.27/60.33 inference(rename_variables,[],[149])).
% 60.27/60.33 cnf(187,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x1871,x1871),f28(x1871,f28(x1872,x1872))),f28(f28(x1871,x1871),f28(x1871,f28(x1872,x1872)))),f28(f28(f28(x1871,x1871),f28(x1871,f28(x1872,x1872))),f28(x1873,x1873))),f18(f17(a23)))),
% 60.27/60.33 inference(scs_inference,[],[152,149,72,120])).
% 60.27/60.33 cnf(189,plain,
% 60.27/60.33 (P4(f11(a15),f28(x1891,f11(a15)))),
% 60.27/60.33 inference(scs_inference,[],[168,152,149,72,120,128])).
% 60.27/60.33 cnf(191,plain,
% 60.27/60.33 (P4(f11(a15),f28(f11(a15),x1911))),
% 60.27/60.33 inference(scs_inference,[],[168,152,149,72,120,128,129])).
% 60.27/60.33 cnf(193,plain,
% 60.27/60.33 (P5(f26(a23),x1931)),
% 60.27/60.33 inference(scs_inference,[],[168,152,149,185,72,120,128,129,71])).
% 60.27/60.33 cnf(194,plain,
% 60.27/60.33 (~P4(x1941,f26(a23))),
% 60.27/60.33 inference(rename_variables,[],[149])).
% 60.27/60.33 cnf(196,plain,
% 60.27/60.33 (~P4(x1961,f26(f26(a23)))),
% 60.27/60.33 inference(scs_inference,[],[168,152,149,185,194,72,120,128,129,71,86])).
% 60.27/60.33 cnf(197,plain,
% 60.27/60.33 (~P4(x1971,f26(a23))),
% 60.27/60.33 inference(rename_variables,[],[149])).
% 60.27/60.33 cnf(202,plain,
% 60.27/60.33 (~P4(x2021,f26(a23))),
% 60.27/60.33 inference(rename_variables,[],[149])).
% 60.27/60.33 cnf(204,plain,
% 60.27/60.33 (P3(f26(a23),x2041)),
% 60.27/60.33 inference(scs_inference,[],[168,152,149,185,194,197,202,72,120,128,129,71,86,119,55,73])).
% 60.27/60.33 cnf(207,plain,
% 60.27/60.33 (P4(f11(a15),f24(f11(a15)))),
% 60.27/60.33 inference(scs_inference,[],[168,127,152,149,185,194,197,202,72,120,128,129,71,86,119,55,73,79])).
% 60.27/60.33 cnf(232,plain,
% 60.27/60.33 (P3(x2321,f26(f26(a23)))),
% 60.27/60.33 inference(scs_inference,[],[196,72])).
% 60.27/60.33 cnf(233,plain,
% 60.27/60.33 (~P4(x2331,f26(f26(a23)))),
% 60.27/60.33 inference(rename_variables,[],[196])).
% 60.27/60.33 cnf(235,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x2351,x2351),f28(x2351,f28(x2352,x2352))),f28(f28(x2351,x2351),f28(x2351,f28(x2352,x2352)))),f28(f28(f28(x2351,x2351),f28(x2351,f28(x2352,x2352))),f28(x2353,x2353))),f18(f18(f17(a23))))),
% 60.27/60.33 inference(scs_inference,[],[187,196,72,120])).
% 60.27/60.33 cnf(237,plain,
% 60.27/60.33 (~P4(x2371,f26(f26(f26(a23))))),
% 60.27/60.33 inference(scs_inference,[],[187,196,233,72,120,86])).
% 60.27/60.33 cnf(238,plain,
% 60.27/60.33 (~P4(x2381,f26(f26(a23)))),
% 60.27/60.33 inference(rename_variables,[],[196])).
% 60.27/60.33 cnf(240,plain,
% 60.27/60.33 (P4(f28(x2401,x2402),f28(x2403,f28(x2401,x2402)))),
% 60.27/60.33 inference(scs_inference,[],[46,187,196,233,72,120,86,128])).
% 60.27/60.33 cnf(242,plain,
% 60.27/60.33 (P5(f26(f26(a23)),x2421)),
% 60.27/60.33 inference(scs_inference,[],[46,187,196,233,238,72,120,86,128,71])).
% 60.27/60.33 cnf(243,plain,
% 60.27/60.33 (~P4(x2431,f26(f26(a23)))),
% 60.27/60.33 inference(rename_variables,[],[196])).
% 60.27/60.33 cnf(245,plain,
% 60.27/60.33 (P4(f28(x2451,x2452),f28(f28(x2451,x2452),x2453))),
% 60.27/60.33 inference(scs_inference,[],[46,187,196,233,238,72,120,86,128,71,129])).
% 60.27/60.33 cnf(248,plain,
% 60.27/60.33 (~P4(x2481,f26(f26(a23)))),
% 60.27/60.33 inference(rename_variables,[],[196])).
% 60.27/60.33 cnf(250,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x2501,x2501),f28(x2501,f28(x2502,x2502))),f28(f28(x2501,x2501),f28(x2501,f28(x2502,x2502)))),f28(f28(f28(x2501,x2501),f28(x2501,f28(x2502,x2502))),f28(x2503,x2503))),f17(f18(f17(a23))))),
% 60.27/60.33 inference(scs_inference,[],[46,187,196,233,238,243,72,120,86,128,71,129,55,119])).
% 60.27/60.33 cnf(252,plain,
% 60.27/60.33 (P3(f26(f26(a23)),x2521)),
% 60.27/60.33 inference(scs_inference,[],[46,187,196,233,238,243,248,72,120,86,128,71,129,55,119,73])).
% 60.27/60.33 cnf(255,plain,
% 60.27/60.33 (P4(f28(x2551,x2552),f24(f28(x2551,x2552)))),
% 60.27/60.33 inference(scs_inference,[],[127,46,187,196,233,238,243,248,72,120,86,128,71,129,55,119,73,79])).
% 60.27/60.33 cnf(267,plain,
% 60.27/60.33 (P3(x2671,f26(f26(f26(a23))))),
% 60.27/60.33 inference(scs_inference,[],[237,72])).
% 60.27/60.33 cnf(268,plain,
% 60.27/60.33 (~P4(x2681,f26(f26(f26(a23))))),
% 60.27/60.33 inference(rename_variables,[],[237])).
% 60.27/60.33 cnf(271,plain,
% 60.27/60.33 (~P4(x2711,f26(a23))),
% 60.27/60.33 inference(rename_variables,[],[149])).
% 60.27/60.33 cnf(273,plain,
% 60.27/60.33 (~P4(x2731,f26(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(scs_inference,[],[149,237,268,72,120,86])).
% 60.27/60.33 cnf(274,plain,
% 60.27/60.33 (~P4(x2741,f26(f26(f26(a23))))),
% 60.27/60.33 inference(rename_variables,[],[237])).
% 60.27/60.33 cnf(276,plain,
% 60.27/60.33 (P5(f26(f26(f26(a23))),x2761)),
% 60.27/60.33 inference(scs_inference,[],[149,237,268,274,72,120,86,71])).
% 60.27/60.33 cnf(277,plain,
% 60.27/60.33 (~P4(x2771,f26(f26(f26(a23))))),
% 60.27/60.33 inference(rename_variables,[],[237])).
% 60.27/60.33 cnf(280,plain,
% 60.27/60.33 (~P4(x2801,f26(a23))),
% 60.27/60.33 inference(rename_variables,[],[149])).
% 60.27/60.33 cnf(282,plain,
% 60.27/60.33 (P3(f26(f26(f26(a23))),x2821)),
% 60.27/60.33 inference(scs_inference,[],[149,271,237,268,274,277,72,120,86,71,119,73])).
% 60.27/60.33 cnf(283,plain,
% 60.27/60.33 (~P4(x2831,f26(f26(f26(a23))))),
% 60.27/60.33 inference(rename_variables,[],[237])).
% 60.27/60.33 cnf(288,plain,
% 60.27/60.33 (~E(f28(x2881,f28(x2882,x2883)),f26(a23))),
% 60.27/60.33 inference(scs_inference,[],[240,149,271,280,237,268,274,277,283,72,120,86,71,119,73,55,34])).
% 60.27/60.33 cnf(290,plain,
% 60.27/60.33 (~P4(f26(a23),a21)),
% 60.27/60.33 inference(scs_inference,[],[240,149,271,280,237,268,274,277,283,72,120,86,71,119,73,55,34,98])).
% 60.27/60.33 cnf(298,plain,
% 60.27/60.33 (~P4(f26(a23),f5(x2981,x2982))),
% 60.27/60.33 inference(scs_inference,[],[288,100])).
% 60.27/60.33 cnf(301,plain,
% 60.27/60.33 (P3(x3011,f26(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(scs_inference,[],[288,273,100,72])).
% 60.27/60.33 cnf(302,plain,
% 60.27/60.33 (~P4(x3021,f26(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(rename_variables,[],[273])).
% 60.27/60.33 cnf(304,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x3041,x3041),f28(x3041,f28(x3042,x3042))),f28(f28(x3041,x3041),f28(x3041,f28(x3042,x3042)))),f28(f28(f28(x3041,x3041),f28(x3041,f28(x3042,x3042))),f28(x3043,x3043))),f18(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(scs_inference,[],[288,273,302,100,72,120])).
% 60.27/60.33 cnf(305,plain,
% 60.27/60.33 (~P4(x3051,f26(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(rename_variables,[],[273])).
% 60.27/60.33 cnf(307,plain,
% 60.27/60.33 (~P4(x3071,f26(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(scs_inference,[],[288,273,302,305,100,72,120,86])).
% 60.27/60.33 cnf(308,plain,
% 60.27/60.33 (~P4(x3081,f26(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(rename_variables,[],[273])).
% 60.27/60.33 cnf(310,plain,
% 60.27/60.33 (P3(f26(f26(f26(f26(a23)))),x3101)),
% 60.27/60.33 inference(scs_inference,[],[288,273,302,305,308,100,72,120,86,73])).
% 60.27/60.33 cnf(311,plain,
% 60.27/60.33 (~P4(x3111,f26(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(rename_variables,[],[273])).
% 60.27/60.33 cnf(313,plain,
% 60.27/60.33 (P5(f26(f26(f26(f26(a23)))),x3131)),
% 60.27/60.33 inference(scs_inference,[],[288,273,302,305,308,311,100,72,120,86,73,71])).
% 60.27/60.33 cnf(314,plain,
% 60.27/60.33 (~P4(x3141,f26(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(rename_variables,[],[273])).
% 60.27/60.33 cnf(316,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x3161,x3161),f28(x3161,f28(x3162,x3162))),f28(f28(x3161,x3161),f28(x3161,f28(x3162,x3162)))),f28(f28(f28(x3161,x3161),f28(x3161,f28(x3162,x3162))),f28(x3163,x3163))),f17(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(scs_inference,[],[288,273,302,305,308,311,314,100,72,120,86,73,71,119])).
% 60.27/60.33 cnf(317,plain,
% 60.27/60.33 (~P4(x3171,f26(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(rename_variables,[],[273])).
% 60.27/60.33 cnf(322,plain,
% 60.27/60.33 (~P4(f26(a23),a16)),
% 60.27/60.33 inference(scs_inference,[],[288,45,273,302,305,308,311,314,317,100,72,120,86,73,71,119,55,76])).
% 60.27/60.33 cnf(324,plain,
% 60.27/60.33 (~E(a15,f26(a23))),
% 60.27/60.33 inference(scs_inference,[],[168,288,45,149,273,302,305,308,311,314,317,100,72,120,86,73,71,119,55,76,34])).
% 60.27/60.33 cnf(333,plain,
% 60.27/60.33 (P3(x3331,f26(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(scs_inference,[],[307,72])).
% 60.27/60.33 cnf(334,plain,
% 60.27/60.33 (~P4(x3341,f26(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(rename_variables,[],[307])).
% 60.27/60.33 cnf(336,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x3361,x3361),f28(x3361,f28(x3362,x3362))),f28(f28(x3361,x3361),f28(x3361,f28(x3362,x3362)))),f28(f28(f28(x3361,x3361),f28(x3361,f28(x3362,x3362))),f28(x3363,x3363))),f18(f18(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[304,307,72,120])).
% 60.27/60.33 cnf(338,plain,
% 60.27/60.33 (P5(f26(f26(f26(f26(f26(a23))))),x3381)),
% 60.27/60.33 inference(scs_inference,[],[304,307,334,72,120,71])).
% 60.27/60.33 cnf(339,plain,
% 60.27/60.33 (~P4(x3391,f26(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(rename_variables,[],[307])).
% 60.27/60.33 cnf(341,plain,
% 60.27/60.33 (~P4(x3411,f26(f26(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[304,307,334,339,72,120,71,86])).
% 60.27/60.33 cnf(342,plain,
% 60.27/60.33 (~P4(x3421,f26(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(rename_variables,[],[307])).
% 60.27/60.33 cnf(344,plain,
% 60.27/60.33 (P3(f26(f26(f26(f26(f26(a23))))),x3441)),
% 60.27/60.33 inference(scs_inference,[],[304,307,334,339,342,72,120,71,86,73])).
% 60.27/60.33 cnf(347,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x3471,x3471),f28(x3471,f28(x3472,x3472))),f28(f28(x3471,x3471),f28(x3471,f28(x3472,x3472)))),f28(f28(f28(x3471,x3471),f28(x3471,f28(x3472,x3472))),f28(x3473,x3473))),f17(f18(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[304,307,334,339,342,72,120,71,86,73,119])).
% 60.27/60.33 cnf(364,plain,
% 60.27/60.33 (P3(x3641,f26(f26(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[341,72])).
% 60.27/60.33 cnf(365,plain,
% 60.27/60.33 (~P4(x3651,f26(f26(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(rename_variables,[],[341])).
% 60.27/60.33 cnf(369,plain,
% 60.27/60.33 (P5(f26(f26(f26(f26(f26(f26(a23)))))),x3691)),
% 60.27/60.33 inference(scs_inference,[],[336,341,365,72,120,71])).
% 60.27/60.33 cnf(370,plain,
% 60.27/60.33 (~P4(x3701,f26(f26(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(rename_variables,[],[341])).
% 60.27/60.33 cnf(372,plain,
% 60.27/60.33 (P3(f26(f26(f26(f26(f26(f26(a23)))))),x3721)),
% 60.27/60.33 inference(scs_inference,[],[336,341,365,370,72,120,71,73])).
% 60.27/60.33 cnf(373,plain,
% 60.27/60.33 (~P4(x3731,f26(f26(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(rename_variables,[],[341])).
% 60.27/60.33 cnf(375,plain,
% 60.27/60.33 (~P4(x3751,f26(f26(f26(f26(f26(f26(f26(a23))))))))),
% 60.27/60.33 inference(scs_inference,[],[336,341,365,370,373,72,120,71,73,86])).
% 60.27/60.33 cnf(376,plain,
% 60.27/60.33 (~P4(x3761,f26(f26(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(rename_variables,[],[341])).
% 60.27/60.33 cnf(383,plain,
% 60.27/60.33 (~P4(f26(a23),a4)),
% 60.27/60.33 inference(scs_inference,[],[44,336,341,365,370,373,376,298,72,120,71,73,86,119,55,76])).
% 60.27/60.33 cnf(395,plain,
% 60.27/60.33 (P3(x3951,f26(f26(f26(f26(f26(f26(f26(a23))))))))),
% 60.27/60.33 inference(scs_inference,[],[375,72])).
% 60.27/60.33 cnf(396,plain,
% 60.27/60.33 (~P4(x3961,f26(f26(f26(f26(f26(f26(f26(a23))))))))),
% 60.27/60.33 inference(rename_variables,[],[375])).
% 60.27/60.33 cnf(402,plain,
% 60.27/60.33 (P5(f26(f26(f26(f26(f26(f26(f26(a23))))))),x4021)),
% 60.27/60.33 inference(scs_inference,[],[375,396,347,72,120,119,71])).
% 60.27/60.33 cnf(403,plain,
% 60.27/60.33 (~P4(x4031,f26(f26(f26(f26(f26(f26(f26(a23))))))))),
% 60.27/60.33 inference(rename_variables,[],[375])).
% 60.27/60.33 cnf(405,plain,
% 60.27/60.33 (~P4(x4051,f26(f26(f26(f26(f26(f26(f26(f26(a23)))))))))),
% 60.27/60.33 inference(scs_inference,[],[375,396,403,347,72,120,119,71,86])).
% 60.27/60.33 cnf(406,plain,
% 60.27/60.33 (~P4(x4061,f26(f26(f26(f26(f26(f26(f26(a23))))))))),
% 60.27/60.33 inference(rename_variables,[],[375])).
% 60.27/60.33 cnf(408,plain,
% 60.27/60.33 (P3(f26(f26(f26(f26(f26(f26(f26(a23))))))),x4081)),
% 60.27/60.33 inference(scs_inference,[],[375,396,403,406,347,72,120,119,71,86,73])).
% 60.27/60.33 cnf(427,plain,
% 60.27/60.33 (~P4(x4271,f26(f26(f26(f26(f26(f26(f26(f26(a23)))))))))),
% 60.27/60.33 inference(rename_variables,[],[405])).
% 60.27/60.33 cnf(429,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x4291,x4291),f28(x4291,f28(x4292,x4292))),f28(f28(x4291,x4291),f28(x4291,f28(x4292,x4292)))),f28(f28(f28(x4291,x4291),f28(x4291,f28(x4292,x4292))),f28(x4293,x4293))),f18(f17(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[405,316,72,120])).
% 60.27/60.33 cnf(434,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x4341,x4341),f28(x4341,f28(x4342,x4342))),f28(f28(x4341,x4341),f28(x4341,f28(x4342,x4342)))),f28(f28(f28(x4341,x4341),f28(x4341,f28(x4342,x4342))),f28(x4343,x4343))),f17(f17(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[405,427,316,72,120,73,119])).
% 60.27/60.33 cnf(452,plain,
% 60.27/60.33 (~P4(x4521,f26(f26(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(rename_variables,[],[341])).
% 60.27/60.33 cnf(457,plain,
% 60.27/60.33 (~E(a15,f26(f26(f26(f26(f26(f26(f26(a23))))))))),
% 60.27/60.33 inference(scs_inference,[],[168,375,341,452,120,119,34])).
% 60.27/60.33 cnf(459,plain,
% 60.27/60.33 (P3(x4591,x4592)+~E(a23,x4591)),
% 60.27/60.33 inference(scs_inference,[],[168,146,375,341,452,120,119,34,37])).
% 60.27/60.33 cnf(470,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x4701,x4701),f28(x4701,f28(x4702,x4702))),f28(f28(x4701,x4701),f28(x4701,f28(x4702,x4702)))),f28(f28(f28(x4701,x4701),f28(x4701,f28(x4702,x4702))),f28(x4703,x4703))),f18(f26(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[307,120])).
% 60.27/60.33 cnf(471,plain,
% 60.27/60.33 (~P4(x4711,f26(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(rename_variables,[],[307])).
% 60.27/60.33 cnf(473,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x4731,x4731),f28(x4731,f28(x4732,x4732))),f28(f28(x4731,x4731),f28(x4731,f28(x4732,x4732)))),f28(f28(f28(x4731,x4731),f28(x4731,f28(x4732,x4732))),f28(x4733,x4733))),f17(f26(f26(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[307,471,120,119])).
% 60.27/60.33 cnf(474,plain,
% 60.27/60.33 (~P4(x4741,f26(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(rename_variables,[],[307])).
% 60.27/60.33 cnf(478,plain,
% 60.27/60.33 (P3(x4781,x4782)+~E(a23,x4782)),
% 60.27/60.33 inference(scs_inference,[],[168,143,307,471,474,120,119,34,38])).
% 60.27/60.33 cnf(481,plain,
% 60.27/60.33 (P4(x4811,f28(f28(x4812,x4813),x4814))+~E(f28(x4812,x4813),x4811)),
% 60.27/60.33 inference(scs_inference,[],[168,245,46,143,307,471,474,120,119,34,38,81,33])).
% 60.27/60.33 cnf(484,plain,
% 60.27/60.33 (P5(x4841,x4842)+~E(a23,x4841)),
% 60.27/60.33 inference(scs_inference,[],[168,136,245,46,140,43,143,307,471,474,120,119,34,38,81,33,32,36,35])).
% 60.27/60.33 cnf(490,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x4901,x4901),f28(x4901,f28(x4902,x4902))),f28(f28(x4901,x4901),f28(x4901,f28(x4902,x4902)))),f28(f28(f28(x4901,x4901),f28(x4901,f28(x4902,x4902))),f28(x4903,x4903))),f18(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(scs_inference,[],[237,120])).
% 60.27/60.33 cnf(491,plain,
% 60.27/60.33 (~P4(x4911,f26(f26(f26(a23))))),
% 60.27/60.33 inference(rename_variables,[],[237])).
% 60.27/60.33 cnf(493,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x4931,x4931),f28(x4931,f28(x4932,x4932))),f28(f28(x4931,x4931),f28(x4931,f28(x4932,x4932)))),f28(f28(f28(x4931,x4931),f28(x4931,f28(x4932,x4932))),f28(x4933,x4933))),f17(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(scs_inference,[],[237,491,120,119])).
% 60.27/60.33 cnf(510,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x5101,x5101),f28(x5101,f28(x5102,x5102))),f28(f28(x5101,x5101),f28(x5101,f28(x5102,x5102)))),f28(f28(f28(x5101,x5101),f28(x5101,f28(x5102,x5102))),f28(x5103,x5103))),f18(f26(f26(a23))))),
% 60.27/60.33 inference(scs_inference,[],[196,120])).
% 60.27/60.33 cnf(511,plain,
% 60.27/60.33 (~P4(x5111,f26(f26(a23)))),
% 60.27/60.33 inference(rename_variables,[],[196])).
% 60.27/60.33 cnf(514,plain,
% 60.27/60.33 (~P4(x5141,f26(f26(a23)))),
% 60.27/60.33 inference(rename_variables,[],[196])).
% 60.27/60.33 cnf(518,plain,
% 60.27/60.33 (P4(x5181,f28(x5182,f28(x5183,x5184)))+~E(f28(x5183,x5184),x5181)),
% 60.27/60.33 inference(scs_inference,[],[168,240,196,511,514,120,119,34,33])).
% 60.27/60.33 cnf(528,plain,
% 60.27/60.33 (~E(f28(f28(x5281,x5282),x5283),a23)),
% 60.27/60.33 inference(scs_inference,[],[245,51,429,120,119,34])).
% 60.27/60.33 cnf(530,plain,
% 60.27/60.33 (~P4(a23,f5(x5301,x5302))),
% 60.27/60.33 inference(scs_inference,[],[245,51,429,120,119,34,100])).
% 60.27/60.33 cnf(545,plain,
% 60.27/60.33 (~E(f28(f28(x5451,x5452),x5453),a23)),
% 60.27/60.33 inference(rename_variables,[],[528])).
% 60.27/60.33 cnf(549,plain,
% 60.27/60.33 (P3(f11(f28(f28(x5491,x5492),x5493)),f28(f28(x5491,x5492),x5493))),
% 60.27/60.33 inference(scs_inference,[],[528,545,98,57,58])).
% 60.27/60.33 cnf(557,plain,
% 60.27/60.33 (~P4(a23,a16)),
% 60.27/60.33 inference(scs_inference,[],[528,545,45,434,530,98,57,58,55,120,119,76])).
% 60.27/60.33 cnf(577,plain,
% 60.27/60.33 (~P4(a23,f17(x5771))),
% 60.27/60.33 inference(scs_inference,[],[48,470,557,530,55,120,119,76])).
% 60.27/60.33 cnf(582,plain,
% 60.27/60.33 (P4(f11(f28(x5821,f28(x5822,x5823))),f28(x5821,f28(x5822,x5823)))),
% 60.27/60.33 inference(scs_inference,[],[240,51,48,470,557,530,55,120,119,76,34,57])).
% 60.27/60.33 cnf(584,plain,
% 60.27/60.33 (P3(f11(f28(x5841,f28(x5842,x5843))),f28(x5841,f28(x5842,x5843)))),
% 60.27/60.33 inference(scs_inference,[],[240,51,48,470,557,530,55,120,119,76,34,57,58])).
% 60.27/60.33 cnf(601,plain,
% 60.27/60.33 (~P4(a23,a4)),
% 60.27/60.33 inference(scs_inference,[],[44,473,577,530,55,120,119,76])).
% 60.27/60.33 cnf(614,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x6141,x6141),f28(x6141,f28(x6142,x6142))),f28(f28(x6141,x6141),f28(x6141,f28(x6142,x6142)))),f28(f28(f28(x6141,x6141),f28(x6141,f28(x6142,x6142))),f28(x6143,x6143))),f18(f18(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(scs_inference,[],[490,601,55,120])).
% 60.27/60.33 cnf(616,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x6161,x6161),f28(x6161,f28(x6162,x6162))),f28(f28(x6161,x6161),f28(x6161,f28(x6162,x6162)))),f28(f28(f28(x6161,x6161),f28(x6161,f28(x6162,x6162))),f28(x6163,x6163))),f17(f18(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(scs_inference,[],[490,601,55,120,119])).
% 60.27/60.33 cnf(618,plain,
% 60.27/60.33 (~P4(a23,f6(x6181,x6182))),
% 60.27/60.33 inference(scs_inference,[],[47,490,601,530,55,120,119,76])).
% 60.27/60.33 cnf(632,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x6321,x6321),f28(x6321,f28(x6322,x6322))),f28(f28(x6321,x6321),f28(x6321,f28(x6322,x6322)))),f28(f28(f28(x6321,x6321),f28(x6321,f28(x6322,x6322))),f28(x6323,x6323))),f18(f18(f18(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[614,618,55,120])).
% 60.27/60.33 cnf(634,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x6341,x6341),f28(x6341,f28(x6342,x6342))),f28(f28(x6341,x6341),f28(x6341,f28(x6342,x6342)))),f28(f28(f28(x6341,x6341),f28(x6341,f28(x6342,x6342))),f28(x6343,x6343))),f17(f18(f18(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[614,618,55,120,119])).
% 60.27/60.33 cnf(636,plain,
% 60.27/60.33 (~E(f28(f28(x6361,x6362),x6363),f26(f26(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(scs_inference,[],[245,307,614,618,55,120,119,34])).
% 60.27/60.33 cnf(651,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x6511,x6511),f28(x6511,f28(x6512,x6512))),f28(f28(x6511,x6511),f28(x6511,f28(x6512,x6512)))),f28(f28(f28(x6511,x6511),f28(x6511,f28(x6512,x6512))),f28(x6513,x6513))),f17(f18(f18(f18(f26(f26(f26(a23))))))))),
% 60.27/60.33 inference(scs_inference,[],[636,632,100,120,119])).
% 60.27/60.33 cnf(653,plain,
% 60.27/60.33 (~E(f28(x6531,f28(x6532,x6533)),f26(f26(f26(f26(a23)))))),
% 60.27/60.33 inference(scs_inference,[],[240,636,273,632,100,120,119,34])).
% 60.27/60.33 cnf(668,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x6681,x6681),f28(x6681,f28(x6682,x6682))),f28(f28(x6681,x6681),f28(x6681,f28(x6682,x6682)))),f28(f28(f28(x6681,x6681),f28(x6681,f28(x6682,x6682))),f28(x6683,x6683))),f18(f17(f18(f18(f26(f26(f26(a23))))))))),
% 60.27/60.33 inference(scs_inference,[],[653,634,100,120])).
% 60.27/60.33 cnf(670,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x6701,x6701),f28(x6701,f28(x6702,x6702))),f28(f28(x6701,x6701),f28(x6701,f28(x6702,x6702)))),f28(f28(f28(x6701,x6701),f28(x6701,f28(x6702,x6702))),f28(x6703,x6703))),f17(f17(f18(f18(f26(f26(f26(a23))))))))),
% 60.27/60.33 inference(scs_inference,[],[653,634,100,120,119])).
% 60.27/60.33 cnf(686,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x6861,x6861),f28(x6861,f28(x6862,x6862))),f28(f28(x6861,x6861),f28(x6861,f28(x6862,x6862)))),f28(f28(f28(x6861,x6861),f28(x6861,f28(x6862,x6862))),f28(x6863,x6863))),f18(f17(f18(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[616,120])).
% 60.27/60.33 cnf(688,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x6881,x6881),f28(x6881,f28(x6882,x6882))),f28(f28(x6881,x6881),f28(x6881,f28(x6882,x6882)))),f28(f28(f28(x6881,x6881),f28(x6881,f28(x6882,x6882))),f28(x6883,x6883))),f17(f17(f18(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[616,120,119])).
% 60.27/60.33 cnf(690,plain,
% 60.27/60.33 (~E(f28(f28(x6901,x6902),x6903),f26(f26(a23)))),
% 60.27/60.33 inference(scs_inference,[],[245,196,616,120,119,34])).
% 60.27/60.33 cnf(709,plain,
% 60.27/60.33 (~E(f24(a3),f26(a23))),
% 60.27/60.33 inference(scs_inference,[],[690,149,165,686,98,120,119,34])).
% 60.27/60.33 cnf(712,plain,
% 60.27/60.33 (P5(x7121,x7122)+~E(f26(a23),x7121)),
% 60.27/60.33 inference(scs_inference,[],[136,690,149,193,165,686,98,120,119,34,31,35])).
% 60.27/60.33 cnf(724,plain,
% 60.27/60.33 (P5(x7241,x7242)+~E(f26(f26(a23)),x7241)),
% 60.27/60.33 inference(scs_inference,[],[168,341,242,688,120,119,34,35])).
% 60.27/60.33 cnf(732,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x7321,x7321),f28(x7321,f28(x7322,x7322))),f28(f28(x7321,x7321),f28(x7321,f28(x7322,x7322)))),f28(f28(f28(x7321,x7321),f28(x7321,f28(x7322,x7322))),f28(x7323,x7323))),f18(f17(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(scs_inference,[],[493,120])).
% 60.27/60.33 cnf(734,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x7341,x7341),f28(x7341,f28(x7342,x7342))),f28(f28(x7341,x7341),f28(x7341,f28(x7342,x7342)))),f28(f28(f28(x7341,x7341),f28(x7341,f28(x7342,x7342))),f28(x7343,x7343))),f17(f17(f26(f26(f26(a23))))))),
% 60.27/60.33 inference(scs_inference,[],[493,120,119])).
% 60.27/60.33 cnf(738,plain,
% 60.27/60.33 (P3(x7381,x7382)+~E(f26(a23),x7382)),
% 60.27/60.33 inference(scs_inference,[],[240,307,184,493,120,119,34,38])).
% 60.27/60.33 cnf(740,plain,
% 60.27/60.33 (P3(x7401,x7402)+~E(f26(a23),x7401)),
% 60.27/60.33 inference(scs_inference,[],[240,307,204,184,48,493,120,119,34,38,36,37])).
% 60.27/60.33 cnf(741,plain,
% 60.27/60.33 (P5(x7411,x7412)+~E(f26(f26(f26(a23))),x7411)),
% 60.27/60.33 inference(scs_inference,[],[240,307,276,204,184,48,493,120,119,34,38,36,37,35])).
% 60.27/60.33 cnf(750,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x7501,x7501),f28(x7501,f28(x7502,x7502))),f28(f28(x7501,x7501),f28(x7501,f28(x7502,x7502)))),f28(f28(f28(x7501,x7501),f28(x7501,f28(x7502,x7502))),f28(x7503,x7503))),f18(f18(f17(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[732,120])).
% 60.27/60.33 cnf(752,plain,
% 60.27/60.33 (~P4(f28(f28(f28(f28(x7521,x7521),f28(x7521,f28(x7522,x7522))),f28(f28(x7521,x7521),f28(x7521,f28(x7522,x7522)))),f28(f28(f28(x7521,x7521),f28(x7521,f28(x7522,x7522))),f28(x7523,x7523))),f17(f18(f17(f26(f26(f26(a23)))))))),
% 60.27/60.33 inference(scs_inference,[],[732,120,119])).
% 60.27/60.33 cnf(754,plain,
% 60.27/60.33 (~E(f28(x7541,f28(x7542,x7543)),f26(f26(f26(a23))))),
% 60.27/60.33 inference(scs_inference,[],[240,237,732,120,119,34])).
% 60.27/60.33 cnf(758,plain,
% 60.27/60.33 (P3(x7581,x7582)+~E(f26(f26(f26(a23))),x7581)),
% 60.27/60.33 inference(scs_inference,[],[240,237,282,732,120,119,34,98,37])).
% 60.27/60.33 cnf(759,plain,
% 60.27/60.33 (P3(x7591,x7592)+~E(f26(f26(f26(a23))),x7592)),
% 60.27/60.33 inference(scs_inference,[],[240,237,267,282,732,120,119,34,98,37,38])).
% 60.27/60.33 cnf(761,plain,
% 60.27/60.33 (P5(x7611,x7612)+~E(f26(f26(f26(f26(a23)))),x7611)),
% 60.27/60.33 inference(scs_inference,[],[240,237,313,44,267,282,732,120,119,34,98,37,38,36,35])).
% 60.27/60.33 cnf(779,plain,
% 60.27/60.33 (P3(x7791,x7792)+~E(f26(f26(a23)),x7792)),
% 60.27/60.33 inference(scs_inference,[],[245,754,273,232,750,100,120,119,34,38])).
% 60.27/60.33 cnf(780,plain,
% 60.27/60.33 (P3(x7801,x7802)+~E(f26(f26(a23)),x7801)),
% 60.27/60.33 inference(scs_inference,[],[245,754,273,232,252,750,100,120,119,34,38,37])).
% 60.27/60.33 cnf(782,plain,
% 60.27/60.33 (P5(x7821,x7822)+~E(f26(f26(f26(f26(f26(a23))))),x7821)),
% 60.27/60.33 inference(scs_inference,[],[245,754,273,338,47,232,252,750,100,120,119,34,38,37,36,35])).
% 60.27/60.33 cnf(797,plain,
% 60.27/60.33 (P3(x7971,x7972)+~E(f26(f26(f26(f26(a23)))),x7971)),
% 60.27/60.33 inference(scs_inference,[],[240,196,310,752,120,119,34,37])).
% 60.27/60.33 cnf(798,plain,
% 60.27/60.33 (P3(x7981,x7982)+~E(f26(f26(f26(f26(a23)))),x7982)),
% 60.27/60.33 inference(scs_inference,[],[240,196,301,310,752,120,119,34,37,38])).
% 60.27/60.33 cnf(800,plain,
% 60.27/60.33 (P5(x8001,x8002)+~E(f26(f26(f26(f26(f26(f26(a23)))))),x8001)),
% 60.27/60.33 inference(scs_inference,[],[240,196,369,49,301,310,752,120,119,34,37,38,36,35])).
% 60.27/60.33 cnf(808,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x8081,x8081),f28(x8081,f28(x8082,x8082))),f28(f28(x8081,x8081),f28(x8081,f28(x8082,x8082)))),f28(f28(f28(x8081,x8081),f28(x8081,f28(x8082,x8082))),f28(x8083,x8083))),f18(f17(f17(f26(f26(f26(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[734,120])).
% 60.27/60.34 cnf(810,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x8101,x8101),f28(x8101,f28(x8102,x8102))),f28(f28(x8101,x8101),f28(x8101,f28(x8102,x8102)))),f28(f28(f28(x8101,x8101),f28(x8101,f28(x8102,x8102))),f28(x8103,x8103))),f17(f17(f17(f26(f26(f26(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[734,120,119])).
% 60.27/60.34 cnf(812,plain,
% 60.27/60.34 (P3(x8121,x8122)+~E(f26(f26(f26(f26(f26(a23))))),x8122)),
% 60.27/60.34 inference(scs_inference,[],[333,734,120,119,38])).
% 60.27/60.34 cnf(813,plain,
% 60.27/60.34 (P3(x8131,x8132)+~E(f26(f26(f26(f26(f26(a23))))),x8131)),
% 60.27/60.34 inference(scs_inference,[],[333,344,734,120,119,38,37])).
% 60.27/60.34 cnf(824,plain,
% 60.27/60.34 (P3(x8241,x8242)+~E(f26(f26(f26(f26(f26(f26(a23)))))),x8241)),
% 60.27/60.34 inference(scs_inference,[],[372,808,120,119,37])).
% 60.27/60.34 cnf(825,plain,
% 60.27/60.34 (P3(x8251,x8252)+~E(f26(f26(f26(f26(f26(f26(a23)))))),x8252)),
% 60.27/60.34 inference(scs_inference,[],[364,372,808,120,119,37,38])).
% 60.27/60.34 cnf(826,plain,
% 60.27/60.34 (P4(x8261,a15)+~E(f28(x8262,x8263),x8261)),
% 60.27/60.34 inference(scs_inference,[],[46,364,372,808,120,119,37,38,33])).
% 60.27/60.34 cnf(827,plain,
% 60.27/60.34 (P5(x8271,x8272)+~E(f26(f26(f26(f26(f26(f26(f26(a23))))))),x8271)),
% 60.27/60.34 inference(scs_inference,[],[46,402,364,372,808,120,119,37,38,33,35])).
% 60.27/60.34 cnf(836,plain,
% 60.27/60.34 (P3(x8361,x8362)+~E(f26(f26(f26(f26(f26(f26(f26(a23))))))),x8362)),
% 60.27/60.34 inference(scs_inference,[],[395,810,120,119,38])).
% 60.27/60.34 cnf(837,plain,
% 60.27/60.34 (P3(x8371,x8372)+~E(f26(f26(f26(f26(f26(f26(f26(a23))))))),x8371)),
% 60.27/60.34 inference(scs_inference,[],[395,408,810,120,119,38,37])).
% 60.27/60.34 cnf(839,plain,
% 60.27/60.34 (P4(x8391,f24(f28(x8392,x8393)))+~E(f28(x8392,x8393),x8391)),
% 60.27/60.34 inference(scs_inference,[],[255,48,395,408,810,120,119,38,37,35,33])).
% 60.27/60.34 cnf(845,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x8451,x8451),f28(x8451,f28(x8452,x8452))),f28(f28(x8451,x8451),f28(x8451,f28(x8452,x8452)))),f28(f28(f28(x8451,x8451),f28(x8451,f28(x8452,x8452))),f28(x8453,x8453))),f18(f18(f18(f17(a23)))))),
% 60.27/60.34 inference(scs_inference,[],[235,120])).
% 60.27/60.34 cnf(847,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x8471,x8471),f28(x8471,f28(x8472,x8472))),f28(f28(x8471,x8471),f28(x8471,f28(x8472,x8472)))),f28(f28(f28(x8471,x8471),f28(x8471,f28(x8472,x8472))),f28(x8473,x8473))),f17(f18(f18(f17(a23)))))),
% 60.27/60.34 inference(scs_inference,[],[235,120,119])).
% 60.27/60.34 cnf(857,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x8571,x8571),f28(x8571,f28(x8572,x8572))),f28(f28(x8571,x8571),f28(x8571,f28(x8572,x8572)))),f28(f28(f28(x8571,x8571),f28(x8571,f28(x8572,x8572))),f28(x8573,x8573))),f18(f18(f18(f18(f17(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[845,120])).
% 60.27/60.34 cnf(862,plain,
% 60.27/60.34 (P3(x8621,f28(x8622,f28(x8623,x8624)))+~E(f11(f28(x8622,f28(x8623,x8624))),x8621)),
% 60.27/60.34 inference(scs_inference,[],[584,845,120,119,38,37])).
% 60.27/60.34 cnf(869,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x8691,x8691),f28(x8691,f28(x8692,x8692))),f28(f28(x8691,x8691),f28(x8691,f28(x8692,x8692)))),f28(f28(f28(x8691,x8691),f28(x8691,f28(x8692,x8692))),f28(x8693,x8693))),f18(f18(f18(f18(f18(f17(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[857,120])).
% 60.27/60.34 cnf(871,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x8711,x8711),f28(x8711,f28(x8712,x8712))),f28(f28(x8711,x8711),f28(x8711,f28(x8712,x8712)))),f28(f28(f28(x8711,x8711),f28(x8711,f28(x8712,x8712))),f28(x8713,x8713))),f17(f18(f18(f18(f18(f17(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[857,120,119])).
% 60.27/60.34 cnf(873,plain,
% 60.27/60.34 (P3(x8731,a15)+~E(f11(a15),x8731)),
% 60.27/60.34 inference(scs_inference,[],[170,857,120,119,37])).
% 60.27/60.34 cnf(881,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x8811,x8811),f28(x8811,f28(x8812,x8812))),f28(f28(x8811,x8811),f28(x8811,f28(x8812,x8812)))),f28(f28(f28(x8811,x8811),f28(x8811,f28(x8812,x8812))),f28(x8813,x8813))),f18(f18(f18(f18(f18(f18(f17(a23))))))))),
% 60.27/60.34 inference(scs_inference,[],[869,120])).
% 60.27/60.34 cnf(886,plain,
% 60.27/60.34 (P3(x8861,f28(f28(x8862,x8863),x8864))+~E(f11(f28(f28(x8862,x8863),x8864)),x8861)),
% 60.27/60.34 inference(scs_inference,[],[869,549,120,119,38,37])).
% 60.27/60.34 cnf(893,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x8931,x8931),f28(x8931,f28(x8932,x8932))),f28(f28(x8931,x8931),f28(x8931,f28(x8932,x8932)))),f28(f28(f28(x8931,x8931),f28(x8931,f28(x8932,x8932))),f28(x8933,x8933))),f18(f17(f18(f18(f18(f18(f17(a23))))))))),
% 60.27/60.34 inference(scs_inference,[],[871,120])).
% 60.27/60.34 cnf(911,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9111,x9111),f28(x9111,f28(x9112,x9112))),f28(f28(x9111,x9111),f28(x9111,f28(x9112,x9112)))),f28(f28(f28(x9111,x9111),f28(x9111,f28(x9112,x9112))),f28(x9113,x9113))),f17(f17(f18(f18(f17(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[847,120,119])).
% 60.27/60.34 cnf(927,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9271,x9271),f28(x9271,f28(x9272,x9272))),f28(f28(x9271,x9271),f28(x9271,f28(x9272,x9272)))),f28(f28(f28(x9271,x9271),f28(x9271,f28(x9272,x9272))),f28(x9273,x9273))),f17(f17(f17(f18(f18(f17(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[911,120,119])).
% 60.27/60.34 cnf(935,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9351,x9351),f28(x9351,f28(x9352,x9352))),f28(f28(x9351,x9351),f28(x9351,f28(x9352,x9352)))),f28(f28(f28(x9351,x9351),f28(x9351,f28(x9352,x9352))),f28(x9353,x9353))),f17(f17(f17(f17(f18(f18(f17(a23))))))))),
% 60.27/60.34 inference(scs_inference,[],[927,120,119])).
% 60.27/60.34 cnf(938,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9381,x9381),f28(x9381,f28(x9382,x9382))),f28(f28(x9381,x9381),f28(x9381,f28(x9382,x9382)))),f28(f28(f28(x9381,x9381),f28(x9381,f28(x9382,x9382))),f28(x9383,x9383))),f18(f17(f18(f17(a23)))))),
% 60.27/60.34 inference(scs_inference,[],[250,120])).
% 60.27/60.34 cnf(940,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9401,x9401),f28(x9401,f28(x9402,x9402))),f28(f28(x9401,x9401),f28(x9401,f28(x9402,x9402)))),f28(f28(f28(x9401,x9401),f28(x9401,f28(x9402,x9402))),f28(x9403,x9403))),f17(f17(f18(f17(a23)))))),
% 60.27/60.34 inference(scs_inference,[],[250,120,119])).
% 60.27/60.34 cnf(942,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9421,x9421),f28(x9421,f28(x9422,x9422))),f28(f28(x9421,x9421),f28(x9421,f28(x9422,x9422)))),f28(f28(f28(x9421,x9421),f28(x9421,f28(x9422,x9422))),f28(x9423,x9423))),f18(f18(f17(f18(f17(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[938,120])).
% 60.27/60.34 cnf(946,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9461,x9461),f28(x9461,f28(x9462,x9462))),f28(f28(x9461,x9461),f28(x9461,f28(x9462,x9462)))),f28(f28(f28(x9461,x9461),f28(x9461,f28(x9462,x9462))),f28(x9463,x9463))),f18(f18(f18(f17(f18(f17(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[942,120])).
% 60.27/60.34 cnf(950,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9501,x9501),f28(x9501,f28(x9502,x9502))),f28(f28(x9501,x9501),f28(x9501,f28(x9502,x9502)))),f28(f28(f28(x9501,x9501),f28(x9501,f28(x9502,x9502))),f28(x9503,x9503))),f18(f18(f18(f18(f17(f18(f17(a23))))))))),
% 60.27/60.34 inference(scs_inference,[],[946,120])).
% 60.27/60.34 cnf(952,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9521,x9521),f28(x9521,f28(x9522,x9522))),f28(f28(x9521,x9521),f28(x9521,f28(x9522,x9522)))),f28(f28(f28(x9521,x9521),f28(x9521,f28(x9522,x9522))),f28(x9523,x9523))),f17(f18(f18(f18(f17(f18(f17(a23))))))))),
% 60.27/60.34 inference(scs_inference,[],[946,120,119])).
% 60.27/60.34 cnf(972,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9721,x9721),f28(x9721,f28(x9722,x9722))),f28(f28(x9721,x9721),f28(x9721,f28(x9722,x9722)))),f28(f28(f28(x9721,x9721),f28(x9721,f28(x9722,x9722))),f28(x9723,x9723))),f17(f17(f17(f18(f17(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[940,120,119])).
% 60.27/60.34 cnf(988,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9881,x9881),f28(x9881,f28(x9882,x9882))),f28(f28(x9881,x9881),f28(x9881,f28(x9882,x9882)))),f28(f28(f28(x9881,x9881),f28(x9881,f28(x9882,x9882))),f28(x9883,x9883))),f17(f17(f17(f17(f18(f17(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[972,120,119])).
% 60.27/60.34 cnf(994,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9941,x9941),f28(x9941,f28(x9942,x9942))),f28(f28(x9941,x9941),f28(x9941,f28(x9942,x9942)))),f28(f28(f28(x9941,x9941),f28(x9941,f28(x9942,x9942))),f28(x9943,x9943))),f18(f17(f17(f17(f17(f18(f17(a23))))))))),
% 60.27/60.34 inference(scs_inference,[],[988,120])).
% 60.27/60.34 cnf(998,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x9981,x9981),f28(x9981,f28(x9982,x9982))),f28(f28(x9981,x9981),f28(x9981,f28(x9982,x9982)))),f28(f28(f28(x9981,x9981),f28(x9981,f28(x9982,x9982))),f28(x9983,x9983))),f18(f18(f26(f26(a23)))))),
% 60.27/60.34 inference(scs_inference,[],[510,120])).
% 60.27/60.34 cnf(1002,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x10021,x10021),f28(x10021,f28(x10022,x10022))),f28(f28(x10021,x10021),f28(x10021,f28(x10022,x10022)))),f28(f28(f28(x10021,x10021),f28(x10021,f28(x10022,x10022))),f28(x10023,x10023))),f18(f18(f18(f26(f26(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[998,120])).
% 60.27/60.34 cnf(1006,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x10061,x10061),f28(x10061,f28(x10062,x10062))),f28(f28(x10061,x10061),f28(x10061,f28(x10062,x10062)))),f28(f28(f28(x10061,x10061),f28(x10061,f28(x10062,x10062))),f28(x10063,x10063))),f18(f18(f18(f18(f26(f26(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[1002,120])).
% 60.27/60.34 cnf(1010,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x10101,x10101),f28(x10101,f28(x10102,x10102))),f28(f28(x10101,x10101),f28(x10101,f28(x10102,x10102)))),f28(f28(f28(x10101,x10101),f28(x10101,f28(x10102,x10102))),f28(x10103,x10103))),f18(f18(f18(f18(f18(f26(f26(a23))))))))),
% 60.27/60.34 inference(scs_inference,[],[1006,120])).
% 60.27/60.34 cnf(1499,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x14991,x14991),f28(x14991,f28(x14992,x14992))),f28(f28(x14991,x14991),f28(x14991,f28(x14992,x14992)))),f28(f28(f28(x14991,x14991),f28(x14991,f28(x14992,x14992))),f28(x14993,x14993))),f17(f18(a23)))),
% 60.27/60.34 inference(scs_inference,[],[155,120,119])).
% 60.27/60.34 cnf(1627,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x16271,x16271),f28(x16271,f28(x16272,x16272))),f28(f28(x16271,x16271),f28(x16271,f28(x16272,x16272)))),f28(f28(f28(x16271,x16271),f28(x16271,f28(x16272,x16272))),f28(x16273,x16273))),f18(f17(f18(a23))))),
% 60.27/60.34 inference(scs_inference,[],[1499,120])).
% 60.27/60.34 cnf(1629,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x16291,x16291),f28(x16291,f28(x16292,x16292))),f28(f28(x16291,x16291),f28(x16291,f28(x16292,x16292)))),f28(f28(f28(x16291,x16291),f28(x16291,f28(x16292,x16292))),f28(x16293,x16293))),f17(f17(f18(a23))))),
% 60.27/60.34 inference(scs_inference,[],[1499,120,119])).
% 60.27/60.34 cnf(1631,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x16311,x16311),f28(x16311,f28(x16312,x16312))),f28(f28(x16311,x16311),f28(x16311,f28(x16312,x16312)))),f28(f28(f28(x16311,x16311),f28(x16311,f28(x16312,x16312))),f28(x16313,x16313))),f17(f18(f17(f18(a23)))))),
% 60.27/60.34 inference(scs_inference,[],[1627,119])).
% 60.27/60.34 cnf(1633,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x16331,x16331),f28(x16331,f28(x16332,x16332))),f28(f28(x16331,x16331),f28(x16331,f28(x16332,x16332)))),f28(f28(f28(x16331,x16331),f28(x16331,f28(x16332,x16332))),f28(x16333,x16333))),f18(f18(f17(f18(a23)))))),
% 60.27/60.34 inference(scs_inference,[],[1627,119,120])).
% 60.27/60.34 cnf(1637,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x16371,x16371),f28(x16371,f28(x16372,x16372))),f28(f28(x16371,x16371),f28(x16371,f28(x16372,x16372)))),f28(f28(f28(x16371,x16371),f28(x16371,f28(x16372,x16372))),f28(x16373,x16373))),f17(f17(f18(f17(f18(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[1631,120,119])).
% 60.27/60.34 cnf(1653,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x16531,x16531),f28(x16531,f28(x16532,x16532))),f28(f28(x16531,x16531),f28(x16531,f28(x16532,x16532)))),f28(f28(f28(x16531,x16531),f28(x16531,f28(x16532,x16532))),f28(x16533,x16533))),f17(f17(f17(f18(f17(f18(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[1637,120,119])).
% 60.27/60.34 cnf(1667,plain,
% 60.27/60.34 (P3(f11(f28(f11(a15),x16671)),f28(f11(a15),x16671))),
% 60.27/60.34 inference(scs_inference,[],[191,51,1653,119,120,34,57,58])).
% 60.27/60.34 cnf(1669,plain,
% 60.27/60.34 (P3(x16691,f28(f11(a15),x16692))+~E(f11(f28(f11(a15),x16692)),x16691)),
% 60.27/60.34 inference(scs_inference,[],[191,51,1653,119,120,34,57,58,37])).
% 60.27/60.34 cnf(1679,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x16791,x16791),f28(x16791,f28(x16792,x16792))),f28(f28(x16791,x16791),f28(x16791,f28(x16792,x16792)))),f28(f28(f28(x16791,x16791),f28(x16791,f28(x16792,x16792))),f28(x16793,x16793))),f17(f18(f18(f17(f18(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[1633,119])).
% 60.27/60.34 cnf(1692,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x16921,x16921),f28(x16921,f28(x16922,x16922))),f28(f28(x16921,x16921),f28(x16921,f28(x16922,x16922)))),f28(f28(f28(x16921,x16921),f28(x16921,f28(x16922,x16922))),f28(x16923,x16923))),f17(f17(f18(f18(f17(f18(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[1679,119])).
% 60.27/60.34 cnf(1694,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x16941,x16941),f28(x16941,f28(x16942,x16942))),f28(f28(x16941,x16941),f28(x16941,f28(x16942,x16942)))),f28(f28(f28(x16941,x16941),f28(x16941,f28(x16942,x16942))),f28(x16943,x16943))),f18(f17(f18(f18(f17(f18(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[1679,119,120])).
% 60.27/60.34 cnf(1706,plain,
% 60.27/60.34 (P3(f11(f28(a3,x17061)),f28(a3,x17061))),
% 60.27/60.34 inference(scs_inference,[],[134,51,1692,119,120,34,57,58])).
% 60.27/60.34 cnf(1722,plain,
% 60.27/60.34 (P3(x17221,f28(a3,x17222))+~E(f11(f28(a3,x17222)),x17221)),
% 60.27/60.34 inference(scs_inference,[],[189,375,1694,1706,119,120,34,37])).
% 60.27/60.34 cnf(1748,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x17481,x17481),f28(x17481,f28(x17482,x17482))),f28(f28(x17481,x17481),f28(x17481,f28(x17482,x17482)))),f28(f28(f28(x17481,x17481),f28(x17481,f28(x17482,x17482))),f28(x17483,x17483))),f18(f17(f17(f18(a23)))))),
% 60.27/60.34 inference(scs_inference,[],[1629,119,120])).
% 60.27/60.34 cnf(1782,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x17821,x17821),f28(x17821,f28(x17822,x17822))),f28(f28(x17821,x17821),f28(x17821,f28(x17822,x17822)))),f28(f28(f28(x17821,x17821),f28(x17821,f28(x17822,x17822))),f28(x17823,x17823))),f17(f18(f17(f17(f18(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[1748,119])).
% 60.27/60.34 cnf(1784,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x17841,x17841),f28(x17841,f28(x17842,x17842))),f28(f28(x17841,x17841),f28(x17841,f28(x17842,x17842)))),f28(f28(f28(x17841,x17841),f28(x17841,f28(x17842,x17842))),f28(x17843,x17843))),f18(f18(f17(f17(f18(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[1748,119,120])).
% 60.27/60.34 cnf(1787,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x17871,x17871),f28(x17871,f28(x17872,x17872))),f28(f28(x17871,x17871),f28(x17871,f28(x17872,x17872)))),f28(f28(f28(x17871,x17871),f28(x17871,f28(x17872,x17872))),f28(x17873,x17873))),f17(f17(f18(f17(f17(f18(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[1782,119])).
% 60.27/60.34 cnf(1789,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x17891,x17891),f28(x17891,f28(x17892,x17892))),f28(f28(x17891,x17891),f28(x17891,f28(x17892,x17892)))),f28(f28(f28(x17891,x17891),f28(x17891,f28(x17892,x17892))),f28(x17893,x17893))),f18(f17(f18(f17(f17(f18(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[1782,119,120])).
% 60.27/60.34 cnf(1791,plain,
% 60.27/60.34 (~P3(f28(f28(x17911,x17912),x17913),f28(f28(x17911,x17912),x17913))),
% 60.27/60.34 inference(scs_inference,[],[245,1782,119,120,84])).
% 60.27/60.34 cnf(1793,plain,
% 60.27/60.34 (~E(f26(a23),f28(f28(x17931,x17932),x17933))),
% 60.27/60.34 inference(scs_inference,[],[245,204,1782,119,120,84,37])).
% 60.27/60.34 cnf(1795,plain,
% 60.27/60.34 (~E(a23,f28(f28(x17951,x17952),x17953))),
% 60.27/60.34 inference(scs_inference,[],[245,143,204,1782,119,120,84,37,38])).
% 60.27/60.34 cnf(1808,plain,
% 60.27/60.34 (~P3(f28(x18081,f28(x18082,x18083)),f28(x18081,f28(x18082,x18083)))),
% 60.27/60.34 inference(scs_inference,[],[240,1791,1787,886,119,120,84])).
% 60.27/60.34 cnf(1810,plain,
% 60.27/60.34 (~P5(f28(f28(x18101,x18102),x18103),a23)),
% 60.27/60.34 inference(scs_inference,[],[240,140,1791,1787,1795,886,119,120,84,70])).
% 60.27/60.34 cnf(1821,plain,
% 60.27/60.34 (~P3(f28(x18211,f28(x18212,x18213)),f28(x18211,f28(x18212,x18213)))),
% 60.27/60.34 inference(rename_variables,[],[1808])).
% 60.27/60.34 cnf(1827,plain,
% 60.27/60.34 (~P3(f28(x18271,a3),f28(x18271,a3))),
% 60.27/60.34 inference(scs_inference,[],[132,1808,1821,1789,1722,862,119,120,84])).
% 60.27/60.34 cnf(1829,plain,
% 60.27/60.34 (~P5(f28(f28(x18291,x18292),x18293),f26(a23))),
% 60.27/60.34 inference(scs_inference,[],[132,193,1808,1821,1789,1793,1722,862,119,120,84,70])).
% 60.27/60.34 cnf(1834,plain,
% 60.27/60.34 (~E(f26(a23),f28(x18341,f28(x18342,x18343)))),
% 60.27/60.34 inference(scs_inference,[],[132,193,313,204,1808,1821,1789,1793,1810,1722,862,119,120,84,70,35,37])).
% 60.27/60.34 cnf(1836,plain,
% 60.27/60.34 (~E(a23,f28(x18361,f28(x18362,x18363)))),
% 60.27/60.34 inference(scs_inference,[],[132,193,313,143,204,1808,1821,1789,1793,1810,1722,862,119,120,84,70,35,37,38])).
% 60.27/60.34 cnf(1840,plain,
% 60.27/60.34 (~P3(f28(x18401,a3),f28(x18401,a3))),
% 60.27/60.34 inference(rename_variables,[],[1827])).
% 60.27/60.34 cnf(1841,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x18411,x18411),f28(x18411,f28(x18412,x18412))),f28(f28(x18411,x18411),f28(x18411,f28(x18412,x18412)))),f28(f28(f28(x18411,x18411),f28(x18411,f28(x18412,x18412))),f28(x18413,x18413))),f17(f18(f18(f17(f17(f18(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[1784,1827,1722,119])).
% 60.27/60.34 cnf(1843,plain,
% 60.27/60.34 (~P4(f28(f28(f28(f28(x18431,x18431),f28(x18431,f28(x18432,x18432))),f28(f28(x18431,x18431),f28(x18431,f28(x18432,x18432)))),f28(f28(f28(x18431,x18431),f28(x18431,f28(x18432,x18432))),f28(x18433,x18433))),f18(f18(f18(f17(f17(f18(a23)))))))),
% 60.27/60.34 inference(scs_inference,[],[1784,1827,1722,119,120])).
% 60.27/60.34 cnf(1845,plain,
% 60.27/60.34 (~P3(f28(x18451,f11(a15)),f28(x18451,f11(a15)))),
% 60.27/60.34 inference(scs_inference,[],[189,1784,1827,1722,119,120,84])).
% 60.27/60.34 cnf(1847,plain,
% 60.27/60.34 (~P5(f28(x18471,f28(x18472,x18473)),a23)),
% 60.27/60.34 inference(scs_inference,[],[189,140,1784,1827,1836,1722,119,120,84,70])).
% 60.27/60.34 cnf(1852,plain,
% 60.27/60.34 (~E(f26(a23),f28(x18521,a3))),
% 60.27/60.34 inference(scs_inference,[],[189,140,338,204,1784,1827,1840,1829,1836,1722,119,120,84,70,35,37])).
% 60.27/60.34 cnf(1854,plain,
% 60.27/60.34 (~E(a23,f28(x18541,a3))),
% 60.27/60.34 inference(scs_inference,[],[189,140,338,143,204,1784,1827,1840,1829,1836,1722,119,120,84,70,35,37,38])).
% 60.27/60.34 cnf(1858,plain,
% 60.27/60.34 (~P3(f28(x18581,f11(a15)),f28(x18581,f11(a15)))),
% 60.27/60.34 inference(rename_variables,[],[1845])).
% 60.27/60.34 cnf(1865,plain,
% 60.27/60.34 (~P5(f28(x18651,a3),a23)),
% 60.27/60.34 inference(scs_inference,[],[168,140,1841,1845,1854,1722,119,120,84,70])).
% 60.27/60.34 cnf(1868,plain,
% 60.27/60.34 (~E(f26(f26(a23)),f28(x18681,f28(x18682,x18683)))),
% 60.27/60.34 inference(scs_inference,[],[168,140,242,1841,1845,1847,1854,1722,119,120,84,70,35])).
% 60.27/60.34 cnf(1872,plain,
% 60.27/60.34 (~E(a23,f28(x18721,f11(a15)))),
% 60.27/60.34 inference(scs_inference,[],[168,140,242,143,204,1841,1845,1858,1847,1854,1722,119,120,84,70,35,37,38])).
% 60.27/60.34 cnf(1874,plain,
% 60.27/60.34 (~E(f11(a15),a15)),
% 60.27/60.34 inference(scs_inference,[],[168,140,242,143,204,1841,1845,1858,1847,1854,1722,119,120,84,70,35,37,38,873])).
% 60.27/60.34 cnf(1894,plain,
% 60.27/60.34 (~P5(f28(x18941,f11(a15)),a23)),
% 60.27/60.34 inference(scs_inference,[],[191,140,1843,1872,119,120,84,70])).
% 60.27/60.34 cnf(1897,plain,
% 60.27/60.34 (~E(f26(f26(f26(a23))),f28(x18971,a3))),
% 60.27/60.34 inference(scs_inference,[],[191,140,276,1843,1872,1865,119,120,84,70,35])).
% 60.27/60.34 cnf(1906,plain,
% 60.27/60.34 (P4(f11(f28(x19061,f11(a15))),f28(x19061,f11(a15)))),
% 60.27/60.34 inference(scs_inference,[],[191,140,276,310,267,1808,1843,1872,1865,119,120,84,70,35,38,37,53,1669,57])).
% 60.27/60.34 cnf(1931,plain,
% 60.27/60.34 (~E(f11(f28(a3,x19311)),f28(a3,x19311))),
% 60.27/60.34 inference(scs_inference,[],[134,193,242,333,372,1808,1834,1894,84,70,35,38,37,1722])).
% 60.27/60.34 cnf(1960,plain,
% 60.27/60.34 (~E(f26(f26(f26(f26(f26(f26(f26(a23))))))),f28(f28(x19601,x19602),x19603))),
% 60.27/60.34 inference(scs_inference,[],[193,402,165,1810,1852,84,70,35])).
% 60.27/60.34 cnf(1981,plain,
% 60.27/60.34 (P4(f11(f24(f28(x19811,x19812))),f24(f28(x19811,x19812)))),
% 60.27/60.34 inference(scs_inference,[],[1868,255,242,207,51,84,70,34,57])).
% 60.27/60.34 cnf(2015,plain,
% 60.27/60.34 (~E(f24(a3),a23)),
% 60.27/60.34 inference(scs_inference,[],[1897,276,165,51,70,34])).
% 60.27/60.34 cnf(2104,plain,
% 60.27/60.34 (~E(f24(f11(a15)),a23)),
% 60.27/60.34 inference(scs_inference,[],[1960,402,207,51,70,34])).
% 60.27/60.34 cnf(2106,plain,
% 60.27/60.34 (P4(f11(f24(f11(a15))),f24(f11(a15)))),
% 60.27/60.34 inference(scs_inference,[],[1960,402,207,51,70,34,57])).
% 60.27/60.34 cnf(2118,plain,
% 60.27/60.34 (~P5(a15,f11(a15))),
% 60.27/60.34 inference(scs_inference,[],[43,1874,70])).
% 60.27/60.34 cnf(2190,plain,
% 60.27/60.34 (~P4(x21901,f26(f26(f26(f26(f26(f26(f26(f26(f26(a23))))))))))),
% 60.27/60.34 inference(scs_inference,[],[405,86])).
% 60.27/60.34 cnf(2207,plain,
% 60.27/60.34 (P3(f26(f26(f26(f26(f26(f26(f26(f26(f26(a23))))))))),x22071)),
% 60.27/60.34 inference(scs_inference,[],[2190,73])).
% 60.27/60.34 cnf(2208,plain,
% 60.27/60.34 (~P4(x22081,f26(f26(f26(f26(f26(f26(f26(f26(f26(a23))))))))))),
% 60.27/60.34 inference(rename_variables,[],[2190])).
% 60.27/60.34 cnf(2210,plain,
% 60.27/60.34 (P5(f26(f26(f26(f26(f26(f26(f26(f26(f26(a23))))))))),x22101)),
% 60.27/60.34 inference(scs_inference,[],[2190,2208,73,71])).
% 60.27/60.34 cnf(2211,plain,
% 60.27/60.34 (~P4(x22111,f26(f26(f26(f26(f26(f26(f26(f26(f26(a23))))))))))),
% 60.27/60.34 inference(rename_variables,[],[2190])).
% 60.27/60.34 cnf(2213,plain,
% 60.27/60.34 (P3(x22131,f26(f26(f26(f26(f26(f26(f26(f26(f26(a23))))))))))),
% 60.27/60.34 inference(scs_inference,[],[2190,2208,2211,73,71,72])).
% 60.27/60.34 cnf(2291,plain,
% 60.27/60.34 (P4(f11(f28(x22911,f28(x22912,x22913))),a15)),
% 60.27/60.34 inference(scs_inference,[],[1847,56,53])).
% 60.27/60.34 cnf(2294,plain,
% 60.27/60.34 (P4(f11(f28(x22941,f28(x22942,x22943))),f28(x22944,f11(f28(x22941,f28(x22942,x22943)))))),
% 60.27/60.34 inference(scs_inference,[],[2291,129,128])).
% 60.27/60.34 cnf(2300,plain,
% 60.27/60.34 (P4(f11(f28(x23001,f28(x23002,x23003))),f24(f11(f28(x23001,f28(x23002,x23003)))))),
% 60.27/60.34 inference(scs_inference,[],[127,2291,651,129,128,119,120,79])).
% 60.27/60.34 cnf(2307,plain,
% 60.27/60.34 (~E(f26(f26(f26(f26(a23)))),f28(x23071,f11(a15)))),
% 60.27/60.34 inference(scs_inference,[],[127,2291,313,149,1894,651,129,128,119,120,79,84,34,35])).
% 60.27/60.34 cnf(2322,plain,
% 60.27/60.34 (~P5(f28(x23221,f11(a15)),f26(f26(f26(f26(a23)))))),
% 60.27/60.34 inference(scs_inference,[],[2294,2307,313,668,119,120,84,70])).
% 60.27/60.34 cnf(2327,plain,
% 60.27/60.34 (~E(f26(f26(f26(f26(f26(a23))))),f28(x23271,a3))),
% 60.27/60.34 inference(scs_inference,[],[240,2294,2307,338,313,341,1865,668,119,120,84,70,34,35])).
% 60.27/60.34 cnf(2342,plain,
% 60.27/60.34 (~P3(f24(f11(f28(x23421,f28(x23422,x23423)))),f24(f11(f28(x23421,f28(x23422,x23423)))))),
% 60.27/60.34 inference(scs_inference,[],[2300,670,119,120,84])).
% 60.27/60.34 cnf(2344,plain,
% 60.27/60.34 (~P5(f28(x23441,a3),f26(f26(f26(f26(f26(a23))))))),
% 60.27/60.34 inference(scs_inference,[],[2327,338,2300,670,119,120,84,70])).
% 60.27/60.34 cnf(2456,plain,
% 60.27/60.34 (P4(f26(f11(a15)),a15)),
% 60.27/60.34 inference(scs_inference,[],[159,61,57])).
% 60.27/60.34 cnf(2465,plain,
% 60.27/60.34 (P4(f26(f11(a15)),f24(f26(f11(a15))))),
% 60.27/60.34 inference(scs_inference,[],[127,2456,881,129,128,119,120,79])).
% 60.27/60.34 cnf(2498,plain,
% 60.27/60.34 (~P3(f24(f26(f11(a15))),f24(f26(f11(a15))))),
% 60.27/60.34 inference(scs_inference,[],[893,2465,119,120,84])).
% 60.27/60.34 cnf(2602,plain,
% 60.27/60.34 (P4(f24(f20(a2)),a15)),
% 60.27/60.34 inference(scs_inference,[],[158,62,59])).
% 60.27/60.34 cnf(2605,plain,
% 60.27/60.34 (P4(f24(f20(a2)),f28(x26051,f24(f20(a2))))),
% 60.27/60.34 inference(scs_inference,[],[2602,129,128])).
% 60.27/60.34 cnf(2611,plain,
% 60.27/60.34 (P4(f24(f20(a2)),f24(f24(f20(a2))))),
% 60.27/60.34 inference(scs_inference,[],[127,2602,935,129,128,119,120,79])).
% 60.27/60.34 cnf(2626,plain,
% 60.27/60.34 (~P3(f28(x26261,f24(f20(a2))),f28(x26261,f24(f20(a2))))),
% 60.27/60.34 inference(scs_inference,[],[2605,950,119,120,84])).
% 60.27/60.34 cnf(2640,plain,
% 60.27/60.34 (~P3(f24(f24(f20(a2))),f24(f24(f20(a2))))),
% 60.27/60.34 inference(scs_inference,[],[952,2611,119,120,84])).
% 60.27/60.34 cnf(2753,plain,
% 60.27/60.34 (P4(f12(f28(f28(f11(a15),f11(a15)),f28(f11(a15),f28(f11(a15),f11(a15))))),a15)),
% 60.27/60.34 inference(scs_inference,[],[168,63,130])).
% 60.27/60.34 cnf(2762,plain,
% 60.27/60.34 (P4(f12(f28(f28(f11(a15),f11(a15)),f28(f11(a15),f28(f11(a15),f11(a15))))),f24(f12(f28(f28(f11(a15),f11(a15)),f28(f11(a15),f28(f11(a15),f11(a15)))))))),
% 60.27/60.34 inference(scs_inference,[],[127,2753,994,129,128,119,120,79])).
% 60.27/60.34 cnf(2791,plain,
% 60.27/60.34 (~P3(f24(f12(f28(f28(f11(a15),f11(a15)),f28(f11(a15),f28(f11(a15),f11(a15)))))),f24(f12(f28(f28(f11(a15),f11(a15)),f28(f11(a15),f28(f11(a15),f11(a15)))))))),
% 60.27/60.34 inference(scs_inference,[],[2762,1010,119,120,84])).
% 60.27/60.34 cnf(2985,plain,
% 60.27/60.34 (~P4(f28(x29851,x29852),f7(a15))),
% 60.27/60.34 inference(scs_inference,[],[255,74,68])).
% 60.27/60.34 cnf(3087,plain,
% 60.27/60.34 (P4(f20(a2),a15)),
% 60.27/60.34 inference(scs_inference,[],[39,41,290,2498,2640,2118,2104,2106,158,2753,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59])).
% 60.27/60.34 cnf(3094,plain,
% 60.27/60.34 (E(f5(a1,x30941),f5(a2,x30941))),
% 60.27/60.34 inference(scs_inference,[],[39,41,290,2498,2640,2118,2104,2106,158,2753,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59,65,724,779,780,4])).
% 60.27/60.34 cnf(3097,plain,
% 60.27/60.34 (E(f28(x30971,a1),f28(x30971,a2))),
% 60.27/60.34 inference(scs_inference,[],[39,41,290,2498,2640,2118,2104,2106,158,2753,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59,65,724,779,780,4,5,7,8])).
% 60.27/60.34 cnf(3116,plain,
% 60.27/60.34 (E(f28(f20(a2),f20(a2)),a2)),
% 60.27/60.34 inference(scs_inference,[],[39,41,290,2498,2640,2118,2104,2106,158,2753,2602,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59,65,724,779,780,4,5,7,8,9,10,14,15,16,17,22,23,24,25,28,29,92,741,758,759,839,60])).
% 60.27/60.34 cnf(3163,plain,
% 60.27/60.34 (P4(f14(f24(f26(f11(a15))),f24(f26(f11(a15)))),f24(f26(f11(a15))))),
% 60.27/60.34 inference(scs_inference,[],[39,41,290,709,2498,2640,2344,2322,2118,2104,2106,1981,40,1906,158,2753,2602,46,196,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59,65,724,779,780,4,5,7,8,9,10,14,15,16,17,22,23,24,25,28,29,92,741,758,759,839,60,481,518,761,797,798,99,782,812,813,109,800,824,825,130,112,113,827,836,837,95,115,459,478,484,87,2,68,53,69,57,90,73])).
% 60.27/60.34 cnf(3165,plain,
% 60.27/60.34 (P4(f9(f28(x31651,a3),f26(f26(f26(f26(f26(a23)))))),f28(x31651,a3))),
% 60.27/60.34 inference(scs_inference,[],[39,41,290,709,2498,2640,2344,2322,2118,2104,2106,1981,40,1906,158,2753,2602,46,196,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59,65,724,779,780,4,5,7,8,9,10,14,15,16,17,22,23,24,25,28,29,92,741,758,759,839,60,481,518,761,797,798,99,782,812,813,109,800,824,825,130,112,113,827,836,837,95,115,459,478,484,87,2,68,53,69,57,90,73,71])).
% 60.27/60.34 cnf(3169,plain,
% 60.27/60.34 (P4(a23,a3)),
% 60.27/60.34 inference(scs_inference,[],[39,41,290,709,2498,2640,2344,2322,2118,2104,2106,1981,40,1906,158,2753,2602,46,196,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59,65,724,779,780,4,5,7,8,9,10,14,15,16,17,22,23,24,25,28,29,92,741,758,759,839,60,481,518,761,797,798,99,782,812,813,109,800,824,825,130,112,113,827,836,837,95,115,459,478,484,87,2,68,53,69,57,90,73,71,72,55])).
% 60.27/60.34 cnf(3186,plain,
% 60.27/60.34 (P4(f28(x31861,x31862),a15)),
% 60.27/60.34 inference(rename_variables,[],[46])).
% 60.27/60.34 cnf(3193,plain,
% 60.27/60.34 (P4(f11(f28(x31931,f28(x31932,x31933))),f28(x31931,f28(x31932,x31933)))),
% 60.27/60.34 inference(rename_variables,[],[582])).
% 60.27/60.34 cnf(3194,plain,
% 60.27/60.34 (P4(f28(x31941,x31942),a15)),
% 60.27/60.34 inference(rename_variables,[],[46])).
% 60.27/60.34 cnf(3204,plain,
% 60.27/60.34 (~P5(a15,f7(a15))),
% 60.27/60.34 inference(scs_inference,[],[39,41,290,709,2985,1931,2498,2640,2344,2322,2118,2207,2213,2210,2104,2106,1981,1667,40,582,3193,1906,158,165,2753,2602,46,3186,3194,196,42,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59,65,724,779,780,4,5,7,8,9,10,14,15,16,17,22,23,24,25,28,29,92,741,758,759,839,60,481,518,761,797,798,99,782,812,813,109,800,824,825,130,112,113,827,836,837,95,115,459,478,484,87,2,68,53,69,57,90,73,71,72,55,91,93,103,104,101,102,116,75,35,38,82,3,84,37,76])).
% 60.27/60.34 cnf(3205,plain,
% 60.27/60.34 (P4(f28(x32051,x32052),a15)),
% 60.27/60.34 inference(rename_variables,[],[46])).
% 60.27/60.34 cnf(3212,plain,
% 60.27/60.34 (~E(a3,a23)),
% 60.27/60.34 inference(scs_inference,[],[39,41,137,290,324,709,2985,1931,2498,2640,457,2344,2322,2118,2207,2213,2210,2104,2106,1981,1667,40,582,3193,1906,158,402,165,2753,2602,46,3186,3194,196,42,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59,65,724,779,780,4,5,7,8,9,10,14,15,16,17,22,23,24,25,28,29,92,741,758,759,839,60,481,518,761,797,798,99,782,812,813,109,800,824,825,130,112,113,827,836,837,95,115,459,478,484,87,2,68,53,69,57,90,73,71,72,55,91,93,103,104,101,102,116,75,35,38,82,3,84,37,76,70,83,31])).
% 60.27/60.34 cnf(3216,plain,
% 60.27/60.34 (P4(a2,a15)),
% 60.27/60.34 inference(scs_inference,[],[39,41,137,290,324,709,2985,1931,2498,2640,457,2344,2322,2118,2207,2213,2210,2104,2106,1981,1667,40,582,3193,1906,158,402,165,2753,2602,46,3186,3194,3205,196,42,74,77,78,88,89,712,738,740,56,61,62,64,6,11,12,13,18,19,20,21,26,27,30,59,65,724,779,780,4,5,7,8,9,10,14,15,16,17,22,23,24,25,28,29,92,741,758,759,839,60,481,518,761,797,798,99,782,812,813,109,800,824,825,130,112,113,827,836,837,95,115,459,478,484,87,2,68,53,69,57,90,73,71,72,55,91,93,103,104,101,102,116,75,35,38,82,3,84,37,76,70,83,31,33,34,826])).
% 60.27/60.34 cnf(3236,plain,
% 60.27/60.34 (P4(f26(a2),a15)),
% 60.27/60.34 inference(scs_inference,[],[3169,3216,74,61])).
% 60.27/60.34 cnf(3330,plain,
% 60.27/60.34 (P4(f14(f28(x33301,f24(f20(a2))),f28(x33301,f24(f20(a2)))),f28(x33301,f24(f20(a2))))),
% 60.27/60.34 inference(scs_inference,[],[3169,3212,3216,322,3094,3097,3204,3163,2342,3165,2791,2626,273,74,61,109,88,113,77,56,95,112,65,78,87,62,740,130,839,23,759,27,30,7,481,797,6,21,92,12,478,836,17,2,19,18,5,758,89,68,26,24,782,20,29,518,837,15,22,10,825,9,8,28,780,4,738,812,14,53,813,798,459,11,761,13,25,16,827,824,779,800,57,69,73,90,72])).
% 60.27/60.34 cnf(3423,plain,
% 60.27/60.34 ($false),
% 60.27/60.34 inference(scs_inference,[],[383,3087,3236,3330,3116,2015,88,78,113,87,74,112,62,77,56,109,130,61,65]),
% 60.27/60.34 ['proof']).
% 60.27/60.34 % SZS output end Proof
% 60.27/60.34 % Total time :59.680000s
%------------------------------------------------------------------------------