%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG001-4 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n014.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:00:33 EDT 2024
% Result : Unsatisfiable 0.51s 0.69s
% Output : CNFRefutation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : RNG001-4 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n014.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Jun 18 14:36:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.50/0.56 start to proof:theBenchmark
% 0.51/0.68 %-------------------------------------------
% 0.51/0.68 % File :CSE---1.7
% 0.51/0.68 % Problem :theBenchmark
% 0.51/0.68 % Transform :cnf
% 0.51/0.68 % Format :tptp:raw
% 0.51/0.68 % Command :java -jar mcs_scs.jar %d %s
% 0.51/0.68
% 0.51/0.68 % Result :Theorem 0.090000s
% 0.51/0.68 % Output :CNFRefutation 0.090000s
% 0.51/0.68 %-------------------------------------------
% 0.51/0.69 %--------------------------------------------------------------------------
% 0.51/0.69 % File : RNG001-4 : TPTP v8.2.0. Released v1.0.0.
% 0.51/0.69 % Domain : Ring Theory
% 0.51/0.69 % Problem : X.additive_identity = additive_identity for any X
% 0.51/0.69 % Version : [MOW76] axioms : Augmented.
% 0.51/0.69 % English :
% 0.51/0.69
% 0.51/0.69 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 0.51/0.69 % Source : [MOW76]
% 0.51/0.69 % Names : R1 [MOW76]
% 0.51/0.69
% 0.51/0.69 % Status : Unsatisfiable
% 0.51/0.69 % Rating : 0.00 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.25 v5.2.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.00 v2.0.0
% 0.51/0.69 % Syntax : Number of clauses : 20 ( 7 unt; 0 nHn; 14 RR)
% 0.51/0.69 % Number of literals : 57 ( 4 equ; 38 neg)
% 0.51/0.69 % Maximal clause size : 5 ( 2 avg)
% 0.51/0.69 % Maximal term depth : 2 ( 1 avg)
% 0.51/0.69 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 0.51/0.69 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 0.51/0.69 % Number of variables : 79 ( 0 sgn)
% 0.51/0.69 % SPC : CNF_UNS_RFO_SEQ_HRN
% 0.51/0.69
% 0.51/0.69 % Comments : Includes left and right cancellation lemmas.
% 0.51/0.69 %--------------------------------------------------------------------------
% 0.51/0.69 %----Include ring theory axioms
% 0.51/0.69 include('Axioms/RNG001-0.ax').
% 0.51/0.69 %--------------------------------------------------------------------------
% 0.51/0.69 cnf(cancellation1,axiom,
% 0.51/0.69 ( ~ sum(X,Y,Z)
% 0.51/0.69 | ~ sum(X,W,Z)
% 0.51/0.69 | Y = W ) ).
% 0.51/0.69
% 0.51/0.69 cnf(cancellation2,axiom,
% 0.51/0.69 ( ~ sum(X,Y,Z)
% 0.51/0.69 | ~ sum(W,Y,Z)
% 0.51/0.69 | X = W ) ).
% 0.51/0.69
% 0.51/0.69 cnf(prove_a_times_additive_id_is_additive_id,negated_conjecture,
% 0.51/0.69 ~ product(a,additive_identity,additive_identity) ).
% 0.51/0.69
% 0.51/0.69 %--------------------------------------------------------------------------
% 0.51/0.69 %-------------------------------------------
% 0.51/0.69 % Proof found
% 0.51/0.69 % SZS status Theorem for theBenchmark
% 0.51/0.69 % SZS output start Proof
% 0.51/0.69 %ClaNum:34(EqnAxiom:14)
% 0.51/0.69 %VarNum:162(SingletonVarNum:79)
% 0.51/0.69 %MaxLitNum:5
% 0.51/0.69 %MaxfuncDepth:1
% 0.51/0.69 %SharedTerms:3
% 0.51/0.69 %goalClause: 21
% 0.51/0.69 %singleGoalClaCount:1
% 0.51/0.69 [21]~P2(a3,a1,a1)
% 0.51/0.69 [15]P1(x151,a1,x151)
% 0.51/0.69 [16]P1(a1,x161,x161)
% 0.51/0.69 [17]P1(x171,f4(x171),a1)
% 0.51/0.69 [18]P1(f4(x181),x181,a1)
% 0.51/0.69 [19]P1(x191,x192,f2(x191,x192))
% 0.51/0.69 [20]P2(x201,x202,f5(x201,x202))
% 0.51/0.69 [22]~P1(x222,x221,x223)+P1(x221,x222,x223)
% 0.51/0.69 [23]~P1(x233,x234,x231)+E(x231,x232)+~P1(x233,x234,x232)
% 0.51/0.69 [24]~P2(x243,x244,x241)+E(x241,x242)+~P2(x243,x244,x242)
% 0.51/0.69 [25]~P1(x253,x251,x254)+E(x251,x252)+~P1(x253,x252,x254)
% 0.51/0.69 [26]~P1(x261,x263,x264)+E(x261,x262)+~P1(x262,x263,x264)
% 0.51/0.69 [27]~P1(x276,x274,x271)+P1(x271,x272,x273)+~P1(x274,x272,x275)+~P1(x276,x275,x273)
% 0.51/0.69 [28]~P1(x281,x286,x284)+P1(x281,x282,x283)+~P1(x284,x285,x283)+~P1(x286,x285,x282)
% 0.51/0.69 [29]~P2(x296,x294,x291)+P2(x291,x292,x293)+~P2(x294,x292,x295)+~P2(x296,x295,x293)
% 0.51/0.69 [30]~P2(x301,x306,x304)+P2(x301,x302,x303)+~P2(x304,x305,x303)+~P2(x306,x305,x302)
% 0.51/0.69 [31]~P2(x317,x315,x312)+~P2(x317,x314,x311)+P1(x311,x312,x313)+~P1(x314,x315,x316)+~P2(x317,x316,x313)
% 0.51/0.69 [32]~P2(x325,x327,x322)+~P2(x324,x327,x321)+P1(x321,x322,x323)+~P1(x324,x325,x326)+~P2(x326,x327,x323)
% 0.51/0.69 [33]~P2(x337,x332,x335)+~P2(x336,x332,x334)+P2(x331,x332,x333)+~P1(x334,x335,x333)+~P1(x336,x337,x331)
% 0.51/0.69 [34]~P2(x341,x347,x345)+~P2(x341,x346,x344)+P2(x341,x342,x343)+~P1(x344,x345,x343)+~P1(x346,x347,x342)
% 0.51/0.69 %EqnAxiom
% 0.51/0.69 [1]E(x11,x11)
% 0.51/0.69 [2]E(x22,x21)+~E(x21,x22)
% 0.51/0.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.51/0.69 [4]~E(x41,x42)+E(f4(x41),f4(x42))
% 0.51/0.69 [5]~E(x51,x52)+E(f5(x51,x53),f5(x52,x53))
% 0.51/0.69 [6]~E(x61,x62)+E(f5(x63,x61),f5(x63,x62))
% 0.51/0.69 [7]~E(x71,x72)+E(f2(x71,x73),f2(x72,x73))
% 0.51/0.69 [8]~E(x81,x82)+E(f2(x83,x81),f2(x83,x82))
% 0.51/0.69 [9]P1(x92,x93,x94)+~E(x91,x92)+~P1(x91,x93,x94)
% 0.51/0.69 [10]P1(x103,x102,x104)+~E(x101,x102)+~P1(x103,x101,x104)
% 0.51/0.69 [11]P1(x113,x114,x112)+~E(x111,x112)+~P1(x113,x114,x111)
% 0.51/0.69 [12]P2(x122,x123,x124)+~E(x121,x122)+~P2(x121,x123,x124)
% 0.51/0.69 [13]P2(x133,x132,x134)+~E(x131,x132)+~P2(x133,x131,x134)
% 0.51/0.69 [14]P2(x143,x144,x142)+~E(x141,x142)+~P2(x143,x144,x141)
% 0.51/0.69
% 0.51/0.70 %-------------------------------------------
% 0.51/0.70 cnf(35,plain,
% 0.51/0.70 (E(x351,f2(x351,a1))),
% 0.51/0.70 inference(scs_inference,[],[15,19,23])).
% 0.51/0.70 cnf(36,plain,
% 0.51/0.70 (P1(x361,x362,f2(x361,x362))),
% 0.51/0.70 inference(rename_variables,[],[19])).
% 0.51/0.70 cnf(38,plain,
% 0.51/0.70 (E(f2(a1,x381),x381)),
% 0.51/0.70 inference(scs_inference,[],[15,16,19,36,23,25])).
% 0.51/0.70 cnf(39,plain,
% 0.51/0.70 (P1(x391,x392,f2(x391,x392))),
% 0.51/0.70 inference(rename_variables,[],[19])).
% 0.51/0.70 cnf(40,plain,
% 0.51/0.70 (P1(a1,x401,x401)),
% 0.51/0.70 inference(rename_variables,[],[16])).
% 0.51/0.70 cnf(42,plain,
% 0.51/0.70 (E(f2(x421,a1),x421)),
% 0.51/0.70 inference(scs_inference,[],[15,16,19,36,39,23,25,26])).
% 0.51/0.70 cnf(43,plain,
% 0.51/0.70 (P1(x431,x432,f2(x431,x432))),
% 0.51/0.70 inference(rename_variables,[],[19])).
% 0.51/0.70 cnf(44,plain,
% 0.51/0.70 (P1(x441,a1,x441)),
% 0.51/0.70 inference(rename_variables,[],[15])).
% 0.51/0.70 cnf(46,plain,
% 0.51/0.70 (E(f2(f2(a1,x461),a1),x461)),
% 0.51/0.70 inference(scs_inference,[],[15,16,19,36,39,23,25,26,3])).
% 0.51/0.70 cnf(47,plain,
% 0.51/0.70 (~E(f5(a3,a1),a1)),
% 0.51/0.70 inference(scs_inference,[],[21,15,16,19,36,39,20,23,25,26,3,14])).
% 0.51/0.70 cnf(48,plain,
% 0.51/0.70 (P2(x481,x482,f5(x481,x482))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(49,plain,
% 0.51/0.70 (P1(x491,f2(a1,a1),x491)),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,16,19,36,39,43,20,23,25,26,3,14,28])).
% 0.51/0.70 cnf(50,plain,
% 0.51/0.70 (P1(x501,x502,f2(x501,x502))),
% 0.51/0.70 inference(rename_variables,[],[19])).
% 0.51/0.70 cnf(53,plain,
% 0.51/0.70 (P1(x531,x532,f2(x531,x532))),
% 0.51/0.70 inference(rename_variables,[],[19])).
% 0.51/0.70 cnf(54,plain,
% 0.51/0.70 (P1(x541,a1,x541)),
% 0.51/0.70 inference(rename_variables,[],[15])).
% 0.51/0.70 cnf(56,plain,
% 0.51/0.70 (P2(x561,x562,f5(x561,x562))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(58,plain,
% 0.51/0.70 (P2(x581,a1,f2(f5(x581,a1),f5(x581,a1)))),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,16,19,36,39,43,50,53,20,48,56,23,25,26,3,14,28,33,34])).
% 0.51/0.70 cnf(60,plain,
% 0.51/0.70 (P1(x601,a1,x601)),
% 0.51/0.70 inference(rename_variables,[],[15])).
% 0.51/0.70 cnf(62,plain,
% 0.51/0.70 (P2(x621,x622,f5(x621,x622))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(64,plain,
% 0.51/0.70 (P1(f5(x641,a1),f5(x641,a1),f5(x641,a1))),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,60,16,19,36,39,43,50,53,20,48,56,62,23,25,26,3,14,28,33,34,31])).
% 0.51/0.70 cnf(67,plain,
% 0.51/0.70 (P2(x671,x672,f5(x671,x672))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(68,plain,
% 0.51/0.70 (P1(x681,a1,x681)),
% 0.51/0.70 inference(rename_variables,[],[15])).
% 0.51/0.70 cnf(70,plain,
% 0.51/0.70 (P1(f5(a1,x701),f5(a1,x701),f5(a1,x701))),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,60,68,16,19,36,39,43,50,53,20,48,56,62,67,23,25,26,3,14,28,33,34,31,32])).
% 0.51/0.70 cnf(72,plain,
% 0.51/0.70 (P2(x721,x722,f5(x721,x722))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(73,plain,
% 0.51/0.70 (P2(x731,x732,f5(x731,x732))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(76,plain,
% 0.51/0.70 (E(x761,f2(a1,x761))),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,60,68,16,19,36,39,43,50,53,20,48,56,62,67,23,25,26,3,14,28,33,34,31,32,2])).
% 0.51/0.70 cnf(77,plain,
% 0.51/0.70 (P2(f2(a1,a1),x771,f2(f5(a1,x771),f5(a1,x771)))),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,60,68,16,19,36,39,43,50,53,20,48,56,62,67,23,25,26,3,14,28,33,34,31,32,2,12])).
% 0.51/0.70 cnf(78,plain,
% 0.51/0.70 (E(f5(a1,x781),f2(f5(a1,x781),f5(a1,x781)))),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,60,68,16,19,36,39,43,50,53,20,48,56,62,67,73,23,25,26,3,14,28,33,34,31,32,2,12,24])).
% 0.51/0.70 cnf(79,plain,
% 0.51/0.70 (P2(x791,x792,f5(x791,x792))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(81,plain,
% 0.51/0.70 (P1(f2(a1,a1),x811,x811)),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,60,68,16,40,19,36,39,43,50,53,20,48,56,62,67,73,23,25,26,3,14,28,33,34,31,32,2,12,24,9])).
% 0.51/0.70 cnf(83,plain,
% 0.51/0.70 (P1(x831,f4(x831),f2(a1,a1))),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,60,68,16,40,19,36,39,43,50,53,20,48,56,62,67,73,17,23,25,26,3,14,28,33,34,31,32,2,12,24,9,10,11])).
% 0.51/0.70 cnf(85,plain,
% 0.51/0.70 (P2(f5(x851,x851),x851,f5(x851,f5(x851,x851)))),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,60,68,16,40,19,36,39,43,50,53,20,48,56,62,67,73,79,72,17,23,25,26,3,14,28,33,34,31,32,2,12,24,9,10,11,13,29])).
% 0.51/0.70 cnf(87,plain,
% 0.51/0.70 (P2(x871,x872,f5(x871,x872))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(88,plain,
% 0.51/0.70 (P2(x881,x882,f5(x881,x882))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(90,plain,
% 0.51/0.70 (P2(x901,f5(x901,x901),f5(f5(x901,x901),x901))),
% 0.51/0.70 inference(scs_inference,[],[21,15,44,54,60,68,16,40,19,36,39,43,50,53,20,48,56,62,67,73,79,88,87,72,17,23,25,26,3,14,28,33,34,31,32,2,12,24,9,10,11,13,29,30])).
% 0.51/0.70 cnf(96,plain,
% 0.51/0.70 (E(f2(f5(a1,x961),f5(a1,x961)),f5(a1,x961))),
% 0.51/0.70 inference(scs_inference,[],[78,2])).
% 0.51/0.70 cnf(97,plain,
% 0.51/0.70 (E(x971,f4(f4(x971)))),
% 0.51/0.70 inference(scs_inference,[],[18,17,78,2,25])).
% 0.51/0.70 cnf(98,plain,
% 0.51/0.70 (P1(x981,f4(x981),a1)),
% 0.51/0.70 inference(rename_variables,[],[17])).
% 0.51/0.70 cnf(102,plain,
% 0.51/0.70 (~E(f2(f5(a3,a1),f5(a3,a1)),a1)),
% 0.51/0.70 inference(scs_inference,[],[21,85,58,18,17,35,78,2,25,13,14])).
% 0.51/0.70 cnf(105,plain,
% 0.51/0.70 (P1(f4(x1051),x1051,a1)),
% 0.51/0.70 inference(rename_variables,[],[18])).
% 0.51/0.70 cnf(109,plain,
% 0.51/0.70 (P1(f4(x1091),x1091,f2(a1,a1))),
% 0.51/0.70 inference(scs_inference,[],[21,85,90,58,18,105,17,98,35,78,2,25,13,14,26,12,11])).
% 0.51/0.70 cnf(110,plain,
% 0.51/0.70 (E(x1101,f2(x1101,a1))),
% 0.51/0.70 inference(rename_variables,[],[35])).
% 0.51/0.70 cnf(111,plain,
% 0.51/0.70 (E(a1,f4(f2(a1,a1)))),
% 0.51/0.70 inference(scs_inference,[],[21,85,90,58,18,105,17,98,81,35,78,2,25,13,14,26,12,11,23])).
% 0.51/0.70 cnf(115,plain,
% 0.51/0.70 (E(f2(a1,x1151),f2(x1151,a1))),
% 0.51/0.70 inference(scs_inference,[],[21,85,90,58,18,105,17,98,81,35,110,38,78,2,25,13,14,26,12,11,23,3])).
% 0.51/0.70 cnf(134,plain,
% 0.51/0.70 (E(f4(f2(a1,a1)),a1)),
% 0.51/0.70 inference(scs_inference,[],[18,49,46,2,26])).
% 0.51/0.70 cnf(135,plain,
% 0.51/0.70 (P1(x1351,f2(a1,a1),x1351)),
% 0.51/0.70 inference(rename_variables,[],[49])).
% 0.51/0.70 cnf(136,plain,
% 0.51/0.70 (P1(f4(x1361),x1361,a1)),
% 0.51/0.70 inference(rename_variables,[],[18])).
% 0.51/0.70 cnf(138,plain,
% 0.51/0.70 (E(a1,f4(a1))),
% 0.51/0.70 inference(scs_inference,[],[18,17,49,46,16,2,26,23])).
% 0.51/0.70 cnf(140,plain,
% 0.51/0.70 (P1(x1401,f4(x1401),a1)),
% 0.51/0.70 inference(rename_variables,[],[17])).
% 0.51/0.70 cnf(142,plain,
% 0.51/0.70 (E(f4(a1),f2(a1,a1))),
% 0.51/0.70 inference(scs_inference,[],[18,17,140,49,135,46,16,2,26,23,25])).
% 0.51/0.70 cnf(143,plain,
% 0.51/0.70 (P1(x1431,f2(a1,a1),x1431)),
% 0.51/0.70 inference(rename_variables,[],[49])).
% 0.51/0.70 cnf(146,plain,
% 0.51/0.70 (P1(f4(x1461),x1461,f4(f4(a1)))),
% 0.51/0.70 inference(scs_inference,[],[18,136,17,140,97,49,135,46,16,2,26,23,25,11])).
% 0.51/0.70 cnf(147,plain,
% 0.51/0.70 (E(x1471,f4(f4(x1471)))),
% 0.51/0.70 inference(rename_variables,[],[97])).
% 0.51/0.70 cnf(149,plain,
% 0.51/0.70 (P2(x1491,x1492,f5(x1491,x1492))),
% 0.51/0.70 inference(rename_variables,[],[20])).
% 0.51/0.70 cnf(150,plain,
% 0.51/0.70 (~E(f2(f5(a3,a1),f5(a3,a1)),f2(a1,a1))),
% 0.51/0.70 inference(scs_inference,[],[18,136,17,140,97,147,49,135,42,46,102,16,20,2,26,23,25,11,12,3])).
% 0.51/0.70 cnf(154,plain,
% 0.51/0.70 (P1(f4(f4(x1541)),f2(a1,a1),x1541)),
% 0.51/0.70 inference(scs_inference,[],[18,136,17,140,97,147,49,135,143,42,46,102,16,20,149,2,26,23,25,11,12,3,13,9])).
% 0.51/0.70 cnf(181,plain,
% 0.51/0.70 (E(f2(a1,a1),f4(f2(a1,a1)))),
% 0.51/0.70 inference(scs_inference,[],[154,115,109,2,25])).
% 0.51/0.70 cnf(183,plain,
% 0.51/0.70 (P1(f4(f4(x1831)),f2(a1,a1),x1831)),
% 0.51/0.70 inference(rename_variables,[],[154])).
% 0.51/0.70 cnf(187,plain,
% 0.51/0.70 (P1(f4(x1871),x1871,a1)),
% 0.51/0.70 inference(rename_variables,[],[18])).
% 0.51/0.70 cnf(193,plain,
% 0.51/0.70 (E(x1931,f2(a1,x1931))),
% 0.51/0.70 inference(rename_variables,[],[76])).
% 0.51/0.70 cnf(195,plain,
% 0.51/0.70 (P2(f2(a1,a1),x1951,f5(a1,x1951))),
% 0.51/0.70 inference(scs_inference,[],[77,18,187,70,154,150,96,76,115,142,109,15,19,2,25,26,23,11,3,14])).
% 0.51/0.70 cnf(198,plain,
% 0.51/0.70 (E(x1981,f2(a1,x1981))),
% 0.51/0.70 inference(rename_variables,[],[76])).
% 0.51/0.70 cnf(201,plain,
% 0.51/0.70 (P1(a1,f4(f4(x2011)),x2011)),
% 0.51/0.70 inference(scs_inference,[],[77,18,187,70,154,183,83,150,96,76,193,198,115,142,109,15,19,2,25,26,23,11,3,14,9,10,27])).
% 0.51/0.70 cnf(224,plain,
% 0.51/0.70 (E(f2(f5(x2241,a1),f5(x2241,a1)),f5(x2241,a1))),
% 0.51/0.70 inference(scs_inference,[],[58,181,20,2,24])).
% 0.51/0.70 cnf(234,plain,
% 0.51/0.70 (E(f5(x2341,a1),f2(a1,a1))),
% 0.51/0.70 inference(scs_inference,[],[58,64,17,181,201,81,20,19,2,24,25,23,26])).
% 0.51/0.70 cnf(239,plain,
% 0.51/0.70 (P2(f4(f2(a1,a1)),x2391,f5(a1,x2391))),
% 0.51/0.70 inference(scs_inference,[],[58,64,18,17,181,111,195,134,47,201,81,20,19,2,24,25,23,26,11,3,12])).
% 0.51/0.70 cnf(242,plain,
% 0.51/0.70 (P1(x2421,f4(f2(a1,a1)),x2421)),
% 0.51/0.70 inference(scs_inference,[],[58,64,18,17,181,111,195,146,134,47,201,49,81,20,19,2,24,25,23,26,11,3,12,9,10])).
% 0.51/0.70 cnf(263,plain,
% 0.51/0.70 (E(f5(x2631,a1),f2(a1,a1))),
% 0.51/0.70 inference(rename_variables,[],[234])).
% 0.51/0.70 cnf(267,plain,
% 0.51/0.70 (E(f5(x2671,a1),f2(a1,a1))),
% 0.51/0.70 inference(rename_variables,[],[234])).
% 0.51/0.70 cnf(268,plain,
% 0.51/0.70 ($false),
% 0.51/0.70 inference(scs_inference,[],[58,239,70,242,138,224,234,263,267,150,81,2,26,25,14,13,11,3]),
% 0.51/0.70 ['proof']).
% 0.51/0.70 % SZS output end Proof
% 0.51/0.70 % Total time :0.090000s
%------------------------------------------------------------------------------