%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET017+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n023.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:04 EDT 2024
% Result : Theorem 12.40s 12.50s
% Output : CNFRefutation 12.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET017+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jun 23 15:14:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.18/0.56 start to proof:theBenchmark
% 12.40/12.49 %-------------------------------------------
% 12.40/12.49 % File :CSE---1.7
% 12.40/12.49 % Problem :theBenchmark
% 12.40/12.49 % Transform :cnf
% 12.40/12.49 % Format :tptp:raw
% 12.40/12.49 % Command :java -jar mcs_scs.jar %d %s
% 12.40/12.49
% 12.40/12.49 % Result :Theorem 11.890000s
% 12.40/12.49 % Output :CNFRefutation 11.890000s
% 12.40/12.49 %-------------------------------------------
% 12.40/12.50 %------------------------------------------------------------------------------
% 12.40/12.50 % File : SET017+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 12.40/12.50 % Domain : Set Theory
% 12.40/12.50 % Problem : Left cancellation for unordered pairs
% 12.40/12.50 % Version : [Qua92] axioms : Reduced & Augmented > Complete.
% 12.40/12.50 % English :
% 12.40/12.50
% 12.40/12.50 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 12.40/12.50 % : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
% 12.40/12.50 % Source : [Qua92]
% 12.40/12.50 % Names :
% 12.40/12.50
% 12.40/12.50 % Status : Theorem
% 12.40/12.50 % Rating : 0.33 v8.2.0, 0.28 v7.5.0, 0.31 v7.4.0, 0.20 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.22 v7.0.0, 0.23 v6.4.0, 0.31 v6.3.0, 0.33 v6.2.0, 0.44 v6.1.0, 0.53 v6.0.0, 0.57 v5.5.0, 0.59 v5.4.0
% 12.40/12.50 % Syntax : Number of formulae : 44 ( 16 unt; 0 def)
% 12.40/12.50 % Number of atoms : 104 ( 21 equ)
% 12.40/12.50 % Maximal formula atoms : 4 ( 2 avg)
% 12.40/12.50 % Number of connectives : 65 ( 5 ~; 3 |; 28 &)
% 12.40/12.50 % ( 19 <=>; 10 =>; 0 <=; 0 <~>)
% 12.40/12.50 % Maximal formula depth : 7 ( 4 avg)
% 12.40/12.50 % Maximal term depth : 4 ( 1 avg)
% 12.40/12.50 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty)
% 12.40/12.50 % Number of functors : 26 ( 26 usr; 5 con; 0-3 aty)
% 12.40/12.50 % Number of variables : 89 ( 84 !; 5 ?)
% 12.40/12.50 % SPC : FOF_THM_RFO_SEQ
% 12.40/12.50
% 12.40/12.50 % Comments :
% 12.40/12.50 % Bugfixed : v5.4.0 - Bugfixes to SET005+0 axiom file.
% 12.40/12.50 %------------------------------------------------------------------------------
% 12.40/12.50 %----Include set theory axioms
% 12.40/12.50 include('Axioms/SET005+0.ax').
% 12.40/12.50 %------------------------------------------------------------------------------
% 12.40/12.50 %----UP4: Left cancellation for unordered pairs
% 12.40/12.50 fof(left_cancellation,conjecture,
% 12.40/12.50 ! [X,Y,Z] :
% 12.40/12.50 ( ( member(Y,universal_class)
% 12.40/12.50 & member(Z,universal_class)
% 12.40/12.50 & unordered_pair(X,Y) = unordered_pair(X,Z) )
% 12.40/12.50 => Y = Z ) ).
% 12.40/12.50
% 12.40/12.50 %------------------------------------------------------------------------------
% 12.40/12.50 %-------------------------------------------
% 12.40/12.50 % Proof found
% 12.40/12.50 % SZS status Theorem for theBenchmark
% 12.40/12.50 % SZS output start Proof
% 12.40/12.50 %ClaNum:122(EqnAxiom:37)
% 12.40/12.50 %VarNum:607(SingletonVarNum:169)
% 12.40/12.50 %MaxLitNum:4
% 12.40/12.50 %MaxfuncDepth:13
% 12.40/12.50 %SharedTerms:23
% 12.40/12.50 %goalClause: 41 42 44 51
% 12.40/12.50 %singleGoalClaCount:4
% 12.40/12.50 [38]P1(a1)
% 12.40/12.50 [39]P2(a9)
% 12.40/12.50 [40]P4(a1,a14)
% 12.40/12.50 [41]P4(a15,a14)
% 12.40/12.50 [42]P4(a2,a14)
% 12.40/12.50 [51]~E(a2,a15)
% 12.40/12.50 [44]E(f28(a16,a2),f28(a16,a15))
% 12.40/12.50 [45]P5(a3,f4(a14,a14))
% 12.40/12.50 [46]P5(a17,f4(a14,a14))
% 12.40/12.50 [43]P5(x431,a14)
% 12.40/12.50 [52]~P4(x521,a21)
% 12.40/12.50 [49]P5(f18(x491),f4(f4(a14,a14),a14))
% 12.40/12.50 [50]P5(f19(x501),f4(f4(a14,a14),a14))
% 12.40/12.50 [47]P4(f28(x471,x472),a14)
% 12.40/12.50 [48]P5(f5(x481,x482),f4(a14,a14))
% 12.40/12.50 [55]~P1(x551)+P5(a1,x551)
% 12.40/12.50 [56]~P1(x561)+P4(a21,x561)
% 12.40/12.50 [57]E(x571,a21)+P4(f10(x571),a14)
% 12.40/12.50 [58]P4(f10(x581),x581)+E(x581,a21)
% 12.40/12.50 [59]P3(f10(x591),x591)+E(x591,a21)
% 12.40/12.50 [60]~P4(x601,a14)+P4(f26(x601),a14)
% 12.40/12.50 [61]~P4(x611,a14)+P4(f24(x611),a14)
% 12.40/12.50 [62]~P4(x621,a22)+P4(f11(x621),a14)
% 12.40/12.50 [63]~P2(x631)+P5(x631,f4(a14,a14))
% 12.40/12.50 [94]~P4(x941,a22)+E(f28(f28(f11(x941),f11(x941)),f28(f11(x941),f28(f11(x941),f11(x941)))),x941)
% 12.40/12.50 [95]~P2(x951)+P5(f5(x951,f7(f19(f4(x951,a14)))),a22)
% 12.40/12.50 [111]~P1(x1111)+P5(f7(f7(f19(f4(f23(a17,f4(x1111,a14)),a14)))),x1111)
% 12.40/12.50 [54]~E(x541,x542)+P5(x541,x542)
% 12.40/12.50 [64]P4(x641,a14)+~P4(x641,f6(x642))
% 12.40/12.50 [65]P4(x651,a14)+~P4(x651,f7(x652))
% 12.40/12.50 [66]P4(x661,a14)+~P4(x661,f24(x662))
% 12.40/12.50 [67]P5(x671,x672)+~P4(x671,f24(x672))
% 12.40/12.50 [69]P5(x691,x692)+P4(f8(x691,x692),x691)
% 12.40/12.50 [70]P3(x701,x702)+P4(f13(x701,x702),x702)
% 12.40/12.50 [71]P3(x711,x712)+P4(f13(x711,x712),x711)
% 12.40/12.50 [72]~P4(x721,x722)+~P4(x721,f6(x722))
% 12.40/12.50 [83]~P4(x831,f26(x832))+P4(x831,f12(x831,x832))
% 12.40/12.50 [84]~P4(x841,f26(x842))+P4(f12(x841,x842),x842)
% 12.40/12.50 [88]P5(x881,x882)+~P4(f8(x881,x882),x882)
% 12.40/12.50 [92]~P4(x922,f7(x921))+~E(f23(x921,f4(f28(x922,x922),a14)),a21)
% 12.40/12.50 [102]P4(x1021,a14)+~P4(f28(f28(x1022,x1022),f28(x1022,f28(x1021,x1021))),a3)
% 12.40/12.50 [103]P4(x1031,a14)+~P4(f28(f28(x1032,x1032),f28(x1032,f28(x1031,x1031))),a17)
% 12.40/12.50 [104]P4(x1041,a14)+~P4(f28(f28(x1041,x1041),f28(x1041,f28(x1042,x1042))),a17)
% 12.40/12.50 [105]P4(x1051,x1052)+~P4(f28(f28(x1051,x1051),f28(x1051,f28(x1052,x1052))),a3)
% 12.40/12.50 [106]E(f27(x1061,f28(x1061,x1061)),x1062)+~P4(f28(f28(x1061,x1061),f28(x1061,f28(x1062,x1062))),a17)
% 12.40/12.50 [75]~P4(x751,x753)+P4(x751,f27(x752,x753))
% 12.40/12.50 [76]~P4(x761,x762)+P4(x761,f27(x762,x763))
% 12.40/12.50 [85]P4(x851,a14)+~P4(x851,f28(x852,x853))
% 12.40/12.50 [86]P4(x861,x862)+~P4(x861,f23(x863,x862))
% 12.40/12.50 [87]P4(x871,x872)+~P4(x871,f23(x872,x873))
% 12.40/12.50 [96]~P4(x961,f4(x962,x963))+E(f28(f28(f20(x961),f20(x961)),f28(f20(x961),f28(f25(x961),f25(x961)))),x961)
% 12.40/12.50 [107]P4(x1071,a14)+~P4(f28(f28(x1071,x1071),f28(x1071,f28(x1072,x1072))),f5(x1073,x1074))
% 12.40/12.50 [108]P4(x1081,x1082)+~P4(f28(f28(x1083,x1083),f28(x1083,f28(x1081,x1081))),f4(x1084,x1082))
% 12.40/12.50 [109]P4(x1091,x1092)+~P4(f28(f28(x1091,x1091),f28(x1091,f28(x1093,x1093))),f4(x1092,x1094))
% 12.40/12.50 [115]~P4(f28(f28(f28(f28(x1153,x1153),f28(x1153,f28(x1151,x1151))),f28(f28(x1153,x1153),f28(x1153,f28(x1151,x1151)))),f28(f28(f28(x1153,x1153),f28(x1153,f28(x1151,x1151))),f28(x1152,x1152))),f18(x1154))+P4(f28(f28(f28(f28(x1151,x1151),f28(x1151,f28(x1152,x1152))),f28(f28(x1151,x1151),f28(x1151,f28(x1152,x1152)))),f28(f28(f28(x1151,x1151),f28(x1151,f28(x1152,x1152))),f28(x1153,x1153))),x1154)
% 12.40/12.50 [116]~P4(f28(f28(f28(f28(x1162,x1162),f28(x1162,f28(x1161,x1161))),f28(f28(x1162,x1162),f28(x1162,f28(x1161,x1161)))),f28(f28(f28(x1162,x1162),f28(x1162,f28(x1161,x1161))),f28(x1163,x1163))),f19(x1164))+P4(f28(f28(f28(f28(x1161,x1161),f28(x1161,f28(x1162,x1162))),f28(f28(x1161,x1161),f28(x1161,f28(x1162,x1162)))),f28(f28(f28(x1161,x1161),f28(x1161,f28(x1162,x1162))),f28(x1163,x1163))),x1164)
% 12.40/12.50 [117]~P4(f28(f28(f28(f28(x1171,x1171),f28(x1171,f28(x1172,x1172))),f28(f28(x1171,x1171),f28(x1171,f28(x1172,x1172)))),f28(f28(f28(x1171,x1171),f28(x1171,f28(x1172,x1172))),f28(x1173,x1173))),f18(x1174))+P4(f28(f28(f28(f28(x1171,x1171),f28(x1171,f28(x1172,x1172))),f28(f28(x1171,x1171),f28(x1171,f28(x1172,x1172)))),f28(f28(f28(x1171,x1171),f28(x1171,f28(x1172,x1172))),f28(x1173,x1173))),f4(f4(a14,a14),a14))
% 12.40/12.50 [118]~P4(f28(f28(f28(f28(x1181,x1181),f28(x1181,f28(x1182,x1182))),f28(f28(x1181,x1181),f28(x1181,f28(x1182,x1182)))),f28(f28(f28(x1181,x1181),f28(x1181,f28(x1182,x1182))),f28(x1183,x1183))),f19(x1184))+P4(f28(f28(f28(f28(x1181,x1181),f28(x1181,f28(x1182,x1182))),f28(f28(x1181,x1181),f28(x1181,f28(x1182,x1182)))),f28(f28(f28(x1181,x1181),f28(x1181,f28(x1182,x1182))),f28(x1183,x1183))),f4(f4(a14,a14),a14))
% 12.40/12.50 [121]~P4(f28(f28(x1214,x1214),f28(x1214,f28(x1211,x1211))),f5(x1212,x1213))+P4(x1211,f7(f7(f19(f4(f23(x1212,f4(f7(f7(f19(f4(f23(x1213,f4(f28(x1214,x1214),a14)),a14)))),a14)),a14)))))
% 12.40/12.50 [110]P2(x1101)+~P5(x1101,f4(a14,a14))+~P5(f5(x1101,f7(f19(f4(x1101,a14)))),a22)
% 12.40/12.50 [113]P1(x1131)+~P4(a21,x1131)+~P5(f7(f7(f19(f4(f23(a17,f4(x1131,a14)),a14)))),x1131)
% 12.40/12.50 [114]~P4(x1141,a14)+E(x1141,a21)+P4(f26(f7(f7(f19(f4(f23(a9,f4(f28(x1141,x1141),a14)),a14))))),x1141)
% 12.40/12.50 [68]~P5(x682,x681)+~P5(x681,x682)+E(x681,x682)
% 12.40/12.50 [73]P4(x731,x732)+P4(x731,f6(x732))+~P4(x731,a14)
% 12.40/12.50 [77]~P5(x771,x772)+~P4(x771,a14)+P4(x771,f24(x772))
% 12.40/12.50 [91]P4(x912,f7(x911))+~P4(x912,a14)+E(f23(x911,f4(f28(x912,x912),a14)),a21)
% 12.40/12.50 [93]~P4(x932,a14)+P4(x931,a22)+~E(x931,f28(f28(x932,x932),f28(x932,f28(x932,x932))))
% 12.40/12.50 [99]~P4(x991,x992)+~P4(x992,a14)+P4(f28(f28(x991,x991),f28(x991,f28(x992,x992))),a3)
% 12.40/12.50 [97]~P4(x972,a14)+~P4(x971,a14)+E(f20(f28(f28(x971,x971),f28(x971,f28(x972,x972)))),x971)
% 12.40/12.50 [98]~P4(x982,a14)+~P4(x981,a14)+E(f25(f28(f28(x981,x981),f28(x981,f28(x982,x982)))),x982)
% 12.40/12.50 [112]~P2(x1121)+~P4(x1122,a14)+P4(f7(f7(f19(f4(f23(x1121,f4(x1122,a14)),a14)))),a14)
% 12.40/12.50 [74]~P4(x741,x743)+P4(x741,x742)+~P5(x743,x742)
% 12.40/12.50 [82]~P3(x823,x822)+~P4(x821,x822)+~P4(x821,x823)
% 12.40/12.50 [78]~E(x781,x783)+~P4(x781,a14)+P4(x781,f28(x782,x783))
% 12.40/12.50 [79]~E(x791,x792)+~P4(x791,a14)+P4(x791,f28(x792,x793))
% 12.40/12.51 [80]~P4(x801,x803)+~P4(x803,x802)+P4(x801,f26(x802))
% 12.40/12.51 [81]E(x811,x812)+E(x811,x813)+~P4(x811,f28(x813,x812))
% 12.40/12.51 [89]~P4(x891,x893)+~P4(x891,x892)+P4(x891,f23(x892,x893))
% 12.40/12.51 [90]P4(x901,x902)+P4(x901,x903)+~P4(x901,f27(x903,x902))
% 12.40/12.51 [100]~P4(x1002,x1004)+~P4(x1001,x1003)+P4(f28(f28(x1001,x1001),f28(x1001,f28(x1002,x1002))),f4(x1003,x1004))
% 12.40/12.51 [119]~P4(f28(f28(f28(f28(x1192,x1192),f28(x1192,f28(x1193,x1193))),f28(f28(x1192,x1192),f28(x1192,f28(x1193,x1193)))),f28(f28(f28(x1192,x1192),f28(x1192,f28(x1193,x1193))),f28(x1191,x1191))),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))),f18(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))),f4(f4(a14,a14),a14))
% 12.40/12.51 [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))),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))),f19(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))),f4(f4(a14,a14),a14))
% 12.40/12.51 [122]~P4(x1221,a14)+P4(f28(f28(x1221,x1221),f28(x1221,f28(x1222,x1222))),f5(x1223,x1224))+~P4(x1222,f7(f7(f19(f4(f23(x1223,f4(f7(f7(f19(f4(f23(x1224,f4(f28(x1221,x1221),a14)),a14)))),a14)),a14)))))
% 12.40/12.51 [101]~P4(x1012,a14)+~P4(x1011,a14)+~E(f27(x1011,f28(x1011,x1011)),x1012)+P4(f28(f28(x1011,x1011),f28(x1011,f28(x1012,x1012))),a17)
% 12.40/12.51 %EqnAxiom
% 12.40/12.51 [1]E(x11,x11)
% 12.40/12.51 [2]E(x22,x21)+~E(x21,x22)
% 12.40/12.51 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 12.40/12.51 [4]~E(x41,x42)+E(f28(x41,x43),f28(x42,x43))
% 12.40/12.51 [5]~E(x51,x52)+E(f28(x53,x51),f28(x53,x52))
% 12.40/12.51 [6]~E(x61,x62)+E(f7(x61),f7(x62))
% 12.40/12.51 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 12.40/12.51 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 12.40/12.51 [9]~E(x91,x92)+E(f19(x91),f19(x92))
% 12.40/12.51 [10]~E(x101,x102)+E(f23(x101,x103),f23(x102,x103))
% 12.40/12.51 [11]~E(x111,x112)+E(f23(x113,x111),f23(x113,x112))
% 12.40/12.51 [12]~E(x121,x122)+E(f5(x121,x123),f5(x122,x123))
% 12.40/12.51 [13]~E(x131,x132)+E(f5(x133,x131),f5(x133,x132))
% 12.40/12.51 [14]~E(x141,x142)+E(f20(x141),f20(x142))
% 12.40/12.51 [15]~E(x151,x152)+E(f18(x151),f18(x152))
% 12.40/12.51 [16]~E(x161,x162)+E(f25(x161),f25(x162))
% 12.40/12.51 [17]~E(x171,x172)+E(f11(x171),f11(x172))
% 12.40/12.51 [18]~E(x181,x182)+E(f8(x181,x183),f8(x182,x183))
% 12.40/12.51 [19]~E(x191,x192)+E(f8(x193,x191),f8(x193,x192))
% 12.40/12.51 [20]~E(x201,x202)+E(f26(x201),f26(x202))
% 12.40/12.51 [21]~E(x211,x212)+E(f27(x211,x213),f27(x212,x213))
% 12.40/12.51 [22]~E(x221,x222)+E(f27(x223,x221),f27(x223,x222))
% 12.40/12.51 [23]~E(x231,x232)+E(f10(x231),f10(x232))
% 12.40/12.51 [24]~E(x241,x242)+E(f13(x241,x243),f13(x242,x243))
% 12.40/12.51 [25]~E(x251,x252)+E(f13(x253,x251),f13(x253,x252))
% 12.40/12.51 [26]~E(x261,x262)+E(f12(x261,x263),f12(x262,x263))
% 12.40/12.51 [27]~E(x271,x272)+E(f12(x273,x271),f12(x273,x272))
% 12.40/12.51 [28]~E(x281,x282)+E(f6(x281),f6(x282))
% 12.40/12.51 [29]~E(x291,x292)+E(f24(x291),f24(x292))
% 12.40/12.51 [30]~P1(x301)+P1(x302)+~E(x301,x302)
% 12.40/12.51 [31]~P2(x311)+P2(x312)+~E(x311,x312)
% 12.40/12.51 [32]P4(x322,x323)+~E(x321,x322)+~P4(x321,x323)
% 12.40/12.51 [33]P4(x333,x332)+~E(x331,x332)+~P4(x333,x331)
% 12.40/12.51 [34]P5(x342,x343)+~E(x341,x342)+~P5(x341,x343)
% 12.40/12.51 [35]P5(x353,x352)+~E(x351,x352)+~P5(x353,x351)
% 12.40/12.51 [36]P3(x362,x363)+~E(x361,x362)+~P3(x361,x363)
% 12.40/12.51 [37]P3(x373,x372)+~E(x371,x372)+~P3(x373,x371)
% 12.40/12.51
% 12.40/12.51 %-------------------------------------------
% 12.40/12.51 cnf(123,plain,
% 12.40/12.51 (P5(x1231,x1231)),
% 12.40/12.51 inference(equality_inference,[],[54])).
% 12.40/12.51 cnf(124,plain,
% 12.40/12.51 (~P4(x1241,a14)+P4(x1241,f28(x1242,x1241))),
% 12.40/12.51 inference(equality_inference,[],[78])).
% 12.40/12.51 cnf(125,plain,
% 12.40/12.51 (~P4(x1251,a14)+P4(x1251,f28(x1251,x1252))),
% 12.40/12.51 inference(equality_inference,[],[79])).
% 12.40/12.51 cnf(128,plain,
% 12.40/12.51 (P4(a15,f28(x1281,a15))),
% 12.40/12.51 inference(scs_inference,[],[41,124])).
% 12.40/12.51 cnf(130,plain,
% 12.40/12.51 (P4(a15,f28(a15,x1301))),
% 12.40/12.51 inference(scs_inference,[],[41,124,125])).
% 12.40/12.51 cnf(134,plain,
% 12.40/12.51 (~P4(x1341,a21)),
% 12.40/12.51 inference(rename_variables,[],[52])).
% 12.40/12.51 cnf(137,plain,
% 12.40/12.51 (~P4(x1371,a21)),
% 12.40/12.51 inference(rename_variables,[],[52])).
% 12.40/12.51 cnf(140,plain,
% 12.40/12.51 (~P4(x1401,a21)),
% 12.40/12.51 inference(rename_variables,[],[52])).
% 12.40/12.51 cnf(143,plain,
% 12.40/12.51 (~P4(x1431,a21)),
% 12.40/12.51 inference(rename_variables,[],[52])).
% 12.40/12.51 cnf(145,plain,
% 12.40/12.51 (~P4(x1451,f26(a21))),
% 12.40/12.51 inference(scs_inference,[],[41,44,52,134,137,140,143,124,125,2,56,69,70,71,84])).
% 12.40/12.51 cnf(146,plain,
% 12.40/12.51 (~P4(x1461,a21)),
% 12.40/12.51 inference(rename_variables,[],[52])).
% 12.40/12.51 cnf(148,plain,
% 12.40/12.51 (~P4(f28(f28(f28(f28(x1481,x1481),f28(x1481,f28(x1482,x1482))),f28(f28(x1481,x1481),f28(x1481,f28(x1482,x1482)))),f28(f28(f28(x1481,x1481),f28(x1481,f28(x1482,x1482))),f28(x1483,x1483))),f18(a21))),
% 12.40/12.51 inference(scs_inference,[],[41,44,52,134,137,140,143,146,124,125,2,56,69,70,71,84,115])).
% 12.40/12.51 cnf(149,plain,
% 12.40/12.51 (~P4(x1491,a21)),
% 12.40/12.51 inference(rename_variables,[],[52])).
% 12.40/12.51 cnf(151,plain,
% 12.40/12.51 (~P4(f28(f28(f28(f28(x1511,x1511),f28(x1511,f28(x1512,x1512))),f28(f28(x1511,x1511),f28(x1511,f28(x1512,x1512)))),f28(f28(f28(x1511,x1511),f28(x1511,f28(x1512,x1512))),f28(x1513,x1513))),f19(a21))),
% 12.40/12.51 inference(scs_inference,[],[41,44,52,134,137,140,143,146,149,124,125,2,56,69,70,71,84,115,116])).
% 12.40/12.51 cnf(152,plain,
% 12.40/12.51 (~P4(x1521,a21)),
% 12.40/12.51 inference(rename_variables,[],[52])).
% 12.40/12.51 cnf(154,plain,
% 12.40/12.51 (P4(a15,f24(a15))),
% 12.40/12.51 inference(scs_inference,[],[41,44,123,52,134,137,140,143,146,149,124,125,2,56,69,70,71,84,115,116,77])).
% 12.40/12.51 cnf(155,plain,
% 12.40/12.51 (P5(x1551,x1551)),
% 12.40/12.51 inference(rename_variables,[],[123])).
% 12.40/12.51 cnf(158,plain,
% 12.40/12.51 (P4(f28(x1581,x1582),a14)),
% 12.40/12.51 inference(rename_variables,[],[47])).
% 12.40/12.51 cnf(166,plain,
% 12.40/12.51 (P5(f28(a16,a15),f28(a16,a2))),
% 12.40/12.51 inference(scs_inference,[],[41,44,123,155,52,134,137,140,143,146,149,152,47,158,124,125,2,56,69,70,71,84,115,116,77,78,79,32,33,34])).
% 12.40/12.51 cnf(167,plain,
% 12.40/12.51 (P5(x1671,x1671)),
% 12.40/12.51 inference(rename_variables,[],[123])).
% 12.40/12.51 cnf(168,plain,
% 12.40/12.51 (P5(f28(a16,a2),f28(a16,a15))),
% 12.40/12.51 inference(scs_inference,[],[41,44,123,155,167,52,134,137,140,143,146,149,152,47,158,124,125,2,56,69,70,71,84,115,116,77,78,79,32,33,34,35])).
% 12.40/12.51 cnf(170,plain,
% 12.40/12.51 (P4(f10(a14),a14)),
% 12.40/12.51 inference(scs_inference,[],[41,44,123,155,167,52,134,137,140,143,146,149,152,47,158,124,125,2,56,69,70,71,84,115,116,77,78,79,32,33,34,35,58])).
% 12.40/12.51 cnf(174,plain,
% 12.40/12.51 (~P4(x1741,f5(x1742,x1743))+P4(x1741,f4(a14,a14))),
% 12.40/12.51 inference(scs_inference,[],[41,44,123,155,167,52,134,137,140,143,146,149,152,48,47,158,124,125,2,56,69,70,71,84,115,116,77,78,79,32,33,34,35,58,59,74])).
% 12.40/12.51 cnf(183,plain,
% 12.40/12.51 (~P4(f28(f28(f28(f28(x1831,x1831),f28(x1831,f28(x1832,x1832))),f28(f28(x1831,x1831),f28(x1831,f28(x1832,x1832)))),f28(f28(f28(x1831,x1831),f28(x1831,f28(x1832,x1832))),f28(x1833,x1833))),f19(f18(a21)))),
% 12.40/12.51 inference(scs_inference,[],[148,116])).
% 12.40/12.51 cnf(186,plain,
% 12.40/12.51 (~P4(x1861,f26(a21))),
% 12.40/12.51 inference(rename_variables,[],[145])).
% 12.40/12.51 cnf(188,plain,
% 12.40/12.51 (P4(a2,f28(x1881,a2))),
% 12.40/12.51 inference(scs_inference,[],[42,148,145,116,69,124])).
% 12.40/12.51 cnf(191,plain,
% 12.40/12.51 (~P4(x1911,f26(a21))),
% 12.40/12.51 inference(rename_variables,[],[145])).
% 12.40/12.51 cnf(194,plain,
% 12.40/12.51 (~P4(x1941,f26(a21))),
% 12.40/12.51 inference(rename_variables,[],[145])).
% 12.40/12.51 cnf(199,plain,
% 12.40/12.51 (~P4(x1991,f26(a21))),
% 12.40/12.51 inference(rename_variables,[],[145])).
% 12.40/12.51 cnf(201,plain,
% 12.40/12.51 (~P4(x2011,f26(f26(a21)))),
% 12.40/12.51 inference(scs_inference,[],[42,148,145,186,191,194,199,116,69,124,70,71,125,56,84])).
% 12.40/12.51 cnf(209,plain,
% 12.40/12.51 (P4(a15,f28(a16,a2))),
% 12.40/12.51 inference(scs_inference,[],[42,128,123,148,145,186,191,194,199,166,116,69,124,70,71,125,56,84,115,77,74])).
% 12.40/12.51 cnf(231,plain,
% 12.40/12.51 (~P4(f28(f28(f28(f28(x2311,x2311),f28(x2311,f28(x2312,x2312))),f28(f28(x2311,x2311),f28(x2311,f28(x2312,x2312)))),f28(f28(f28(x2311,x2311),f28(x2311,f28(x2312,x2312))),f28(x2313,x2313))),f19(f19(f18(a21))))),
% 12.40/12.51 inference(scs_inference,[],[183,116])).
% 12.40/12.51 cnf(233,plain,
% 12.40/12.51 (P4(f28(x2331,x2332),f28(x2333,f28(x2331,x2332)))),
% 12.40/12.51 inference(scs_inference,[],[47,183,116,124])).
% 12.40/12.51 cnf(236,plain,
% 12.40/12.51 (~P4(x2361,f26(f26(a21)))),
% 12.40/12.51 inference(rename_variables,[],[201])).
% 12.40/12.51 cnf(239,plain,
% 12.40/12.51 (~P4(x2391,f26(f26(a21)))),
% 12.40/12.51 inference(rename_variables,[],[201])).
% 12.40/12.51 cnf(241,plain,
% 12.40/12.51 (P4(f28(x2411,x2412),f28(f28(x2411,x2412),x2413))),
% 12.40/12.51 inference(scs_inference,[],[47,183,201,236,116,124,71,69,125])).
% 12.40/12.51 cnf(244,plain,
% 12.40/12.51 (~P4(x2441,f26(f26(a21)))),
% 12.40/12.51 inference(rename_variables,[],[201])).
% 12.40/12.51 cnf(247,plain,
% 12.40/12.51 (~P4(x2471,f26(f26(a21)))),
% 12.40/12.51 inference(rename_variables,[],[201])).
% 12.40/12.51 cnf(249,plain,
% 12.40/12.51 (~P4(x2491,f26(f26(f26(a21))))),
% 12.40/12.51 inference(scs_inference,[],[47,183,201,236,239,244,247,116,124,71,69,125,70,56,84])).
% 12.40/12.51 cnf(254,plain,
% 12.40/12.51 (P4(f28(x2541,x2542),f24(f28(x2541,x2542)))),
% 12.40/12.51 inference(scs_inference,[],[123,47,183,201,236,239,244,247,116,124,71,69,125,70,56,84,115,77])).
% 12.40/12.51 cnf(267,plain,
% 12.40/12.51 (~P4(f28(f28(f28(f28(x2671,x2671),f28(x2671,f28(x2672,x2672))),f28(f28(x2671,x2671),f28(x2671,f28(x2672,x2672)))),f28(f28(f28(x2671,x2671),f28(x2671,f28(x2672,x2672))),f28(x2673,x2673))),f19(f19(f19(f18(a21)))))),
% 12.40/12.51 inference(scs_inference,[],[231,116])).
% 12.40/12.51 cnf(270,plain,
% 12.40/12.51 (~P4(x2701,f26(f26(f26(a21))))),
% 12.40/12.51 inference(rename_variables,[],[249])).
% 12.40/12.51 cnf(277,plain,
% 12.40/12.51 (~P4(x2771,f26(f26(f26(a21))))),
% 12.40/12.51 inference(rename_variables,[],[249])).
% 12.40/12.51 cnf(280,plain,
% 12.40/12.51 (~P4(x2801,f26(f26(f26(a21))))),
% 12.40/12.51 inference(rename_variables,[],[249])).
% 12.40/12.51 cnf(283,plain,
% 12.40/12.51 (~P4(x2831,f26(f26(f26(a21))))),
% 12.40/12.51 inference(rename_variables,[],[249])).
% 12.40/12.51 cnf(285,plain,
% 12.40/12.51 (~P4(x2851,f26(f26(f26(f26(a21)))))),
% 12.40/12.51 inference(scs_inference,[],[170,231,249,270,277,280,283,116,71,124,125,70,69,56,84])).
% 12.40/12.51 cnf(286,plain,
% 12.40/12.51 (~P4(x2861,f26(f26(f26(a21))))),
% 12.40/12.51 inference(rename_variables,[],[249])).
% 12.40/12.51 cnf(288,plain,
% 12.40/12.51 (~P4(f28(f28(f28(f28(x2881,x2881),f28(x2881,f28(x2882,x2882))),f28(f28(x2881,x2881),f28(x2881,f28(x2882,x2882)))),f28(f28(f28(x2881,x2881),f28(x2881,f28(x2882,x2882))),f28(x2883,x2883))),f18(f19(f19(f18(a21)))))),
% 12.40/12.51 inference(scs_inference,[],[170,231,249,270,277,280,283,116,71,124,125,70,69,56,84,115])).
% 12.40/12.51 cnf(297,plain,
% 12.40/12.51 (~E(a15,x2971)+P4(a15,f28(x2971,x2972))),
% 12.40/12.51 inference(scs_inference,[],[41,44,254,123,170,231,249,270,277,280,283,286,116,71,124,125,70,69,56,84,115,77,33,32,79])).
% 12.40/12.51 cnf(303,plain,
% 12.40/12.51 (E(a15,a2)+E(a15,a16)),
% 12.40/12.51 inference(scs_inference,[],[41,44,254,209,123,170,231,249,270,277,280,283,286,46,116,71,124,125,70,69,56,84,115,77,33,32,79,74,68,81])).
% 12.40/12.51 cnf(309,plain,
% 12.40/12.51 (~P4(f28(f28(f28(f28(x3091,x3091),f28(x3091,f28(x3092,x3092))),f28(f28(x3091,x3091),f28(x3091,f28(x3092,x3092)))),f28(f28(f28(x3091,x3091),f28(x3091,f28(x3092,x3092))),f28(x3093,x3093))),f19(f19(f19(f19(f18(a21))))))),
% 12.40/12.51 inference(scs_inference,[],[267,116])).
% 12.40/12.51 cnf(314,plain,
% 12.40/12.51 (~P4(x3141,f26(f26(f26(f26(a21)))))),
% 12.40/12.51 inference(rename_variables,[],[285])).
% 12.40/12.51 cnf(317,plain,
% 12.40/12.51 (~P4(x3171,f26(f26(f26(f26(a21)))))),
% 12.40/12.51 inference(rename_variables,[],[285])).
% 12.40/12.51 cnf(322,plain,
% 12.40/12.51 (~P4(x3221,f26(f26(f26(f26(a21)))))),
% 12.40/12.51 inference(rename_variables,[],[285])).
% 12.40/12.51 cnf(325,plain,
% 12.40/12.51 (~P4(x3251,f26(f26(f26(f26(a21)))))),
% 12.40/12.51 inference(rename_variables,[],[285])).
% 12.40/12.51 cnf(327,plain,
% 12.40/12.51 (~P4(x3271,f26(f26(f26(f26(f26(a21))))))),
% 12.40/12.51 inference(scs_inference,[],[267,285,314,317,322,325,40,116,124,70,71,125,69,56,84])).
% 12.40/12.51 cnf(328,plain,
% 12.40/12.51 (~P4(x3281,f26(f26(f26(f26(a21)))))),
% 12.40/12.51 inference(rename_variables,[],[285])).
% 12.40/12.51 cnf(330,plain,
% 12.40/12.51 (~P4(f28(f28(f28(f28(x3301,x3301),f28(x3301,f28(x3302,x3302))),f28(f28(x3301,x3301),f28(x3301,f28(x3302,x3302)))),f28(f28(f28(x3301,x3301),f28(x3301,f28(x3302,x3302))),f28(x3303,x3303))),f18(f19(f19(f19(f18(a21))))))),
% 12.40/12.51 inference(scs_inference,[],[267,285,314,317,322,325,40,116,124,70,71,125,69,56,84,115])).
% 12.40/12.51 cnf(342,plain,
% 12.40/12.51 (~E(a15,x3421)+P4(a15,f28(x3422,x3421))),
% 12.40/12.51 inference(scs_inference,[],[41,44,241,188,123,168,267,285,314,317,322,325,328,40,116,124,70,71,125,69,56,84,115,77,74,33,32,78])).
% 12.40/12.51 cnf(344,plain,
% 12.40/12.51 (E(a2,a16)),
% 12.40/12.51 inference(scs_inference,[],[41,44,51,241,188,123,168,267,285,314,317,322,325,328,40,116,124,70,71,125,69,56,84,115,77,74,33,32,78,81])).
% 12.40/12.51 cnf(346,plain,
% 12.40/12.51 (E(a16,a2)),
% 12.40/12.51 inference(scs_inference,[],[41,44,51,241,188,123,168,267,285,314,317,322,325,328,40,116,124,70,71,125,69,56,84,115,77,74,33,32,78,81,2])).
% 12.40/12.51 cnf(360,plain,
% 12.40/12.51 (~P4(f28(f28(f28(f28(x3601,x3601),f28(x3601,f28(x3602,x3602))),f28(f28(x3601,x3601),f28(x3601,f28(x3602,x3602)))),f28(f28(f28(x3601,x3601),f28(x3601,f28(x3602,x3602))),f28(x3603,x3603))),f19(f19(f19(f19(f19(f18(a21)))))))),
% 12.40/12.51 inference(scs_inference,[],[309,116])).
% 12.40/12.51 cnf(363,plain,
% 12.40/12.51 (~P4(x3631,f26(f26(f26(f26(f26(a21))))))),
% 12.40/12.51 inference(rename_variables,[],[327])).
% 12.40/12.51 cnf(366,plain,
% 12.40/12.51 (~P4(x3661,f26(f26(f26(f26(f26(a21))))))),
% 12.40/12.51 inference(rename_variables,[],[327])).
% 12.40/12.51 cnf(368,plain,
% 12.40/12.51 (P3(f26(f26(f26(f26(f26(a21))))),x3681)),
% 12.40/12.51 inference(scs_inference,[],[309,327,363,366,116,70,69,71])).
% 12.40/12.51 cnf(369,plain,
% 12.40/12.51 (~P4(x3691,f26(f26(f26(f26(f26(a21))))))),
% 12.40/12.51 inference(rename_variables,[],[327])).
% 12.40/12.51 cnf(372,plain,
% 12.40/12.51 (~P4(x3721,f26(f26(f26(f26(f26(a21))))))),
% 12.40/12.51 inference(rename_variables,[],[327])).
% 12.40/12.51 cnf(374,plain,
% 12.40/12.52 (~P4(x3741,f26(f26(f26(f26(f26(f26(a21)))))))),
% 12.40/12.52 inference(scs_inference,[],[309,327,363,366,369,372,116,70,69,71,56,84])).
% 12.40/12.52 cnf(375,plain,
% 12.40/12.52 (~P4(x3751,f26(f26(f26(f26(f26(a21))))))),
% 12.40/12.52 inference(rename_variables,[],[327])).
% 12.40/12.52 cnf(377,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x3771,x3771),f28(x3771,f28(x3772,x3772))),f28(f28(x3771,x3771),f28(x3771,f28(x3772,x3772)))),f28(f28(f28(x3771,x3771),f28(x3771,f28(x3772,x3772))),f28(x3773,x3773))),f18(f19(f19(f19(f19(f18(a21)))))))),
% 12.40/12.52 inference(scs_inference,[],[309,327,363,366,369,372,116,70,69,71,56,84,115])).
% 12.40/12.52 cnf(379,plain,
% 12.40/12.52 (P4(a2,f28(x3791,a16))),
% 12.40/12.52 inference(scs_inference,[],[42,309,327,363,366,369,372,344,116,70,69,71,56,84,115,78])).
% 12.40/12.52 cnf(383,plain,
% 12.40/12.52 (P4(a16,a14)),
% 12.40/12.52 inference(scs_inference,[],[41,42,309,327,363,366,369,372,375,344,116,70,69,71,56,84,115,78,33,32])).
% 12.40/12.52 cnf(407,plain,
% 12.40/12.52 (~P4(x4071,f26(f26(f26(f26(f26(f26(a21)))))))),
% 12.40/12.52 inference(rename_variables,[],[374])).
% 12.40/12.52 cnf(410,plain,
% 12.40/12.52 (~P4(x4101,f26(f26(f26(f26(f26(f26(a21)))))))),
% 12.40/12.52 inference(rename_variables,[],[374])).
% 12.40/12.52 cnf(413,plain,
% 12.40/12.52 (~P4(x4131,f26(f26(f26(f26(f26(f26(a21)))))))),
% 12.40/12.52 inference(rename_variables,[],[374])).
% 12.40/12.52 cnf(416,plain,
% 12.40/12.52 (~P4(x4161,f26(f26(f26(f26(f26(f26(a21)))))))),
% 12.40/12.52 inference(rename_variables,[],[374])).
% 12.40/12.52 cnf(418,plain,
% 12.40/12.52 (~P4(x4181,f26(f26(f26(f26(f26(f26(f26(a21))))))))),
% 12.40/12.52 inference(scs_inference,[],[360,374,407,410,413,416,116,70,69,71,56,84])).
% 12.40/12.52 cnf(423,plain,
% 12.40/12.52 (P4(a16,f28(a2,x4231))),
% 12.40/12.52 inference(scs_inference,[],[346,383,360,374,407,410,413,416,116,70,69,71,56,84,115,79])).
% 12.40/12.52 cnf(425,plain,
% 12.40/12.52 (P4(a16,f28(x4251,a2))),
% 12.40/12.52 inference(scs_inference,[],[346,383,360,374,407,410,413,416,116,70,69,71,56,84,115,79,78])).
% 12.40/12.52 cnf(441,plain,
% 12.40/12.52 (~P4(x4411,f26(f26(f26(f26(f26(f26(f26(a21))))))))),
% 12.40/12.52 inference(rename_variables,[],[418])).
% 12.40/12.52 cnf(444,plain,
% 12.40/12.52 (~P4(x4441,f26(f26(f26(f26(f26(f26(f26(a21))))))))),
% 12.40/12.52 inference(rename_variables,[],[418])).
% 12.40/12.52 cnf(447,plain,
% 12.40/12.52 (~P4(x4471,f26(f26(f26(f26(f26(f26(f26(a21))))))))),
% 12.40/12.52 inference(rename_variables,[],[418])).
% 12.40/12.52 cnf(450,plain,
% 12.40/12.52 (~P4(x4501,f26(f26(f26(f26(f26(f26(f26(a21))))))))),
% 12.40/12.52 inference(rename_variables,[],[418])).
% 12.40/12.52 cnf(452,plain,
% 12.40/12.52 (~P4(x4521,f26(f26(f26(f26(f26(f26(f26(f26(a21)))))))))),
% 12.40/12.52 inference(scs_inference,[],[418,441,444,447,450,377,116,69,70,56,71,84])).
% 12.40/12.52 cnf(471,plain,
% 12.40/12.52 (P3(x4711,f26(f26(f26(f26(f26(f26(f26(f26(a21)))))))))),
% 12.40/12.52 inference(scs_inference,[],[452,330,116,70])).
% 12.40/12.52 cnf(516,plain,
% 12.40/12.52 (~P4(x5161,f26(f26(f26(f26(a21)))))),
% 12.40/12.52 inference(rename_variables,[],[285])).
% 12.40/12.52 cnf(518,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x5181,x5181),f28(x5181,f28(x5182,x5182))),f28(f28(x5181,x5181),f28(x5181,f28(x5182,x5182)))),f28(f28(f28(x5181,x5181),f28(x5181,f28(x5182,x5182))),f28(x5183,x5183))),f18(f26(f26(f26(f26(a21))))))),
% 12.40/12.52 inference(scs_inference,[],[285,516,116,115])).
% 12.40/12.52 cnf(594,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x5941,x5941),f28(x5941,f28(x5942,x5942))),f28(f28(x5941,x5941),f28(x5941,f28(x5942,x5942)))),f28(f28(f28(x5941,x5941),f28(x5941,f28(x5942,x5942))),f28(x5943,x5943))),f19(f26(f26(f26(a21)))))),
% 12.40/12.52 inference(scs_inference,[],[249,116])).
% 12.40/12.52 cnf(718,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x7181,x7181),f28(x7181,f28(x7182,x7182))),f28(f28(x7181,x7181),f28(x7181,f28(x7182,x7182)))),f28(f28(f28(x7181,x7181),f28(x7181,f28(x7182,x7182))),f28(x7183,x7183))),f19(f18(f26(f26(f26(f26(a21)))))))),
% 12.40/12.52 inference(scs_inference,[],[518,116])).
% 12.40/12.52 cnf(722,plain,
% 12.40/12.52 (~E(f28(x7221,f28(x7222,x7223)),f26(f26(f26(f26(a21)))))),
% 12.40/12.52 inference(scs_inference,[],[233,285,518,116,115,33])).
% 12.40/12.52 cnf(753,plain,
% 12.40/12.52 (P4(x7531,f24(a15))+~E(a15,x7531)),
% 12.40/12.52 inference(scs_inference,[],[379,154,722,145,45,471,368,718,96,116,115,74,33,174,37,36,32])).
% 12.40/12.52 cnf(788,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x7881,x7881),f28(x7881,f28(x7882,x7882))),f28(f28(x7881,x7881),f28(x7881,f28(x7882,x7882)))),f28(f28(f28(x7881,x7881),f28(x7881,f28(x7882,x7882))),f28(x7883,x7883))),f18(f18(f19(f19(f18(a21))))))),
% 12.40/12.52 inference(scs_inference,[],[288,116,115])).
% 12.40/12.52 cnf(847,plain,
% 12.40/12.52 (~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))),f18(f18(f18(f19(f19(f18(a21)))))))),
% 12.40/12.52 inference(scs_inference,[],[788,116,115])).
% 12.40/12.52 cnf(875,plain,
% 12.40/12.52 (P4(x8751,f28(a15,x8752))+~E(a15,x8751)),
% 12.40/12.52 inference(scs_inference,[],[425,130,201,847,116,115,33,32])).
% 12.40/12.52 cnf(884,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x8841,x8841),f28(x8841,f28(x8842,x8842))),f28(f28(x8841,x8841),f28(x8841,f28(x8842,x8842)))),f28(f28(f28(x8841,x8841),f28(x8841,f28(x8842,x8842))),f28(x8843,x8843))),f18(f19(f26(f26(f26(a21))))))),
% 12.40/12.52 inference(scs_inference,[],[594,116,115])).
% 12.40/12.52 cnf(929,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x9291,x9291),f28(x9291,f28(x9292,x9292))),f28(f28(x9291,x9291),f28(x9291,f28(x9292,x9292)))),f28(f28(f28(x9291,x9291),f28(x9291,f28(x9292,x9292))),f28(x9293,x9293))),f19(f18(f19(f26(f26(f26(a21)))))))),
% 12.40/12.52 inference(scs_inference,[],[884,116])).
% 12.40/12.52 cnf(945,plain,
% 12.40/12.52 (P4(x9451,f28(x9452,a15))+~E(a15,x9451)),
% 12.40/12.52 inference(scs_inference,[],[423,128,201,929,116,115,33,32])).
% 12.40/12.52 cnf(1788,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x17881,x17881),f28(x17881,f28(x17882,x17882))),f28(f28(x17881,x17881),f28(x17881,f28(x17882,x17882)))),f28(f28(f28(x17881,x17881),f28(x17881,f28(x17882,x17882))),f28(x17883,x17883))),f18(f19(a21)))),
% 12.40/12.52 inference(scs_inference,[],[151,115])).
% 12.40/12.52 cnf(1792,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x17921,x17921),f28(x17921,f28(x17922,x17922))),f28(f28(x17921,x17921),f28(x17921,f28(x17922,x17922)))),f28(f28(f28(x17921,x17921),f28(x17921,f28(x17922,x17922))),f28(x17923,x17923))),f18(f18(f19(a21))))),
% 12.40/12.52 inference(scs_inference,[],[1788,115])).
% 12.40/12.52 cnf(1798,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x17981,x17981),f28(x17981,f28(x17982,x17982))),f28(f28(x17981,x17981),f28(x17981,f28(x17982,x17982)))),f28(f28(f28(x17981,x17981),f28(x17981,f28(x17982,x17982))),f28(x17983,x17983))),f19(f18(f18(f19(a21)))))),
% 12.40/12.52 inference(scs_inference,[],[1792,115,116])).
% 12.40/12.52 cnf(1828,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x18281,x18281),f28(x18281,f28(x18282,x18282))),f28(f28(x18281,x18281),f28(x18281,f28(x18282,x18282)))),f28(f28(f28(x18281,x18281),f28(x18281,f28(x18282,x18282))),f28(x18283,x18283))),f18(f19(f18(f18(f19(a21))))))),
% 12.40/12.52 inference(scs_inference,[],[1798,115])).
% 12.40/12.52 cnf(1832,plain,
% 12.40/12.52 (~P4(f28(f28(f28(f28(x18321,x18321),f28(x18321,f28(x18322,x18322))),f28(f28(x18321,x18321),f28(x18321,f28(x18322,x18322)))),f28(f28(f28(x18321,x18321),f28(x18321,f28(x18322,x18322))),f28(x18323,x18323))),f18(f18(f19(f18(f18(f19(a21)))))))),
% 12.40/12.52 inference(scs_inference,[],[1828,115])).
% 12.40/12.52 cnf(1836,plain,
% 12.40/12.52 (E(a15,a16)),
% 12.40/12.52 inference(scs_inference,[],[51,303,2])).
% 12.40/12.52 cnf(1852,plain,
% 12.40/12.52 ($false),
% 12.40/12.52 inference(scs_inference,[],[51,346,344,1836,1832,297,342,753,875,945,67,2,115,116,34,3]),
% 12.40/12.52 ['proof']).
% 12.40/12.52 % SZS output end Proof
% 12.40/12.52 % Total time :11.890000s
%------------------------------------------------------------------------------