%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL197-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/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 : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:18:47 AM UTC 2026
% Result : Unsatisfiable 184.52s 184.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL197-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n027.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 13:37:43 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.44 start to proof:theBenchmark
% 184.52/184.74 %-------------------------------------------
% 184.52/184.74 % File :CSE---1.7
% 184.52/184.74 % Problem :theBenchmark
% 184.52/184.74 % Transform :cnf
% 184.52/184.74 % Format :tptp:raw
% 184.52/184.74 % Command :java -jar mcs_scs.jar %d %s
% 184.52/184.74
% 184.52/184.74 % Result :Theorem 184.167350s
% 184.52/184.74 % Output :CNFRefutation 184.167350s
% 184.52/184.74 %-------------------------------------------
% 184.52/184.74 %--------------------------------------------------------------------------
% 184.52/184.74 % File : LCL197-3 : TPTP v9.3.1. Released v2.3.0.
% 184.52/184.74 % Domain : Logic Calculi (Propositional)
% 184.52/184.74 % Problem : Principia Mathematica 2.41
% 184.52/184.74 % Version : [WR27] axioms.
% 184.52/184.74 % English :
% 184.52/184.74
% 184.52/184.74 % Refs : [WR27] Whitehead & Russell (1927), Principia Mathematica
% 184.52/184.74 % Source : [WR27]
% 184.52/184.74 % Names : Problem 2.41 [WR27]
% 184.52/184.74
% 184.52/184.74 % Status : Unsatisfiable
% 184.52/184.74 % Rating : 0.00 v9.3.0, 0.17 v9.1.0, 0.08 v9.0.0, 0.12 v8.2.0, 0.08 v8.1.0, 0.11 v7.5.0, 0.10 v7.4.0, 0.22 v7.2.0, 0.25 v7.1.0, 0.29 v6.3.0, 0.17 v6.2.0, 0.00 v6.0.0, 0.33 v5.5.0, 0.19 v5.4.0, 0.20 v5.3.0, 0.17 v5.2.0, 0.38 v5.1.0, 0.29 v5.0.0, 0.14 v4.1.0, 0.22 v4.0.1, 0.00 v4.0.0, 0.17 v3.5.0, 0.00 v3.4.0, 0.17 v3.3.0, 0.29 v3.2.0, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.3.0
% 184.52/184.74 % Syntax : Number of clauses : 9 ( 7 unt; 0 nHn; 3 RR)
% 184.52/184.74 % Number of literals : 12 ( 1 equ; 4 neg)
% 184.52/184.74 % Maximal clause size : 3 ( 1 avg)
% 184.52/184.74 % Maximal term depth : 4 ( 2 avg)
% 184.52/184.74 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 184.52/184.74 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 184.52/184.74 % Number of variables : 16 ( 1 sgn)
% 184.52/184.74 % SPC : CNF_UNS_RFO_SEQ_HRN
% 184.52/184.74
% 184.52/184.74 % Comments :
% 184.52/184.74 %--------------------------------------------------------------------------
% 184.52/184.74 %----Include axioms of propositional logic
% 184.52/184.74 include('Axioms/LCL004-0.ax').
% 184.52/184.74 %--------------------------------------------------------------------------
% 184.52/184.75 cnf(prove_this,negated_conjecture,
% 184.52/184.75 ~ theorem(implies(or(q,or(p,q)),or(p,q))) ).
% 184.52/184.75
% 184.52/184.75 %--------------------------------------------------------------------------
% 184.52/184.75 %-------------------------------------------
% 184.52/184.75 % Proof found
% 184.52/184.75 % SZS status Theorem for theBenchmark
% 184.52/184.75 % SZS output start Proof
% 184.52/184.75 %ClaNum:8(EqnAxiom:0)
% 184.52/184.75 %VarNum:28(SingletonVarNum:14)
% 184.52/184.75 %MaxLitNum:3
% 184.52/184.75 %MaxfuncDepth:3
% 184.52/184.75 %SharedTerms:7
% 184.52/184.75 %goalClause: 6
% 184.52/184.75 %singleGoalClaCount:1
% 184.52/184.75 [6]~P2(f2(f1(f2(a3,f2(a4,a3))),f2(a4,a3)))
% 184.52/184.75 [2]P1(f2(f1(f2(x21,x21)),x21))
% 184.52/184.75 [1]P1(f2(f1(x11),f2(x12,x11)))
% 184.52/184.75 [3]P1(f2(f1(f2(x31,x32)),f2(x32,x31)))
% 184.52/184.75 [4]P1(f2(f1(f2(x41,f2(x42,x43))),f2(x42,f2(x41,x43))))
% 184.52/184.75 [5]P1(f2(f1(f2(f1(x51),x52)),f2(f1(f2(x53,x51)),f2(x53,x52))))
% 184.52/184.75 [7]~P1(x71)+P2(x71)
% 184.52/184.75 [8]P2(x81)+~P2(x82)+~P2(f2(f1(x82),x81))
% 184.52/184.75 %EqnAxiom
% 184.52/184.75
% 184.52/184.75 %-------------------------------------------
% 184.86/185.04 cnf(274205,plain,
% 184.86/185.04 (P2(f2(f1(x2742051),f2(x2742052,x2742051)))),
% 184.86/185.04 inference(scs_inference,[],[1,7])).
% 184.86/185.04 cnf(274209,plain,
% 184.86/185.04 (P2(f2(f1(f2(x2742091,x2742092)),f2(x2742092,x2742091)))),
% 184.86/185.04 inference(scs_inference,[],[3,7])).
% 184.86/185.04 cnf(274211,plain,
% 184.86/185.04 (~P2(f2(f1(f2(f1(f2(x2742111,x2742112)),f2(x2742112,x2742111))),f2(f1(f2(a3,f2(a4,a3))),f2(a4,a3))))),
% 184.86/185.04 inference(scs_inference,[],[6,3,7,8])).
% 184.86/185.04 cnf(274213,plain,
% 184.86/185.04 (P2(f2(f1(f2(x2742131,x2742131)),x2742131))),
% 184.86/185.04 inference(scs_inference,[],[2,7])).
% 184.86/185.04 cnf(274217,plain,
% 184.86/185.04 (P2(f2(f1(f2(x2742171,f2(x2742172,x2742173))),f2(x2742172,f2(x2742171,x2742173))))),
% 184.86/185.04 inference(scs_inference,[],[4,7])).
% 184.86/185.04 cnf(274219,plain,
% 184.86/185.04 (P2(f2(f1(f2(f1(x2742191),x2742192)),f2(f1(f2(x2742193,x2742191)),f2(x2742193,x2742192))))),
% 184.86/185.04 inference(scs_inference,[],[5,7])).
% 184.86/185.04 cnf(275196,plain,
% 184.86/185.04 (P2(f2(x2751961,f2(f1(f2(f1(x2751962),x2751963)),f2(f1(f2(x2751964,x2751962)),f2(x2751964,x2751963)))))),
% 184.86/185.04 inference(scs_inference,[],[274219,274205,8])).
% 184.86/185.04 cnf(275209,plain,
% 184.86/185.04 (~P2(f2(f1(f2(f2(a4,a3),a3)),f2(a4,a3)))),
% 184.86/185.04 inference(scs_inference,[],[274219,274211,8])).
% 184.86/185.04 cnf(275214,plain,
% 184.86/185.04 (~P2(f2(f1(f2(f1(f2(x2752141,x2752141)),x2752141)),f2(f1(f2(f2(a4,a3),a3)),f2(a4,a3))))),
% 184.86/185.04 inference(scs_inference,[],[275209,274213,8])).
% 184.86/185.04 cnf(275223,plain,
% 184.86/185.04 (P2(f2(f1(f2(f1(x2752231),x2752232)),f2(x2752233,f2(f1(f2(x2752234,x2752231)),f2(x2752234,x2752232)))))),
% 184.86/185.04 inference(scs_inference,[],[275196,274217,8])).
% 184.86/185.04 cnf(275234,plain,
% 184.86/185.04 (P2(f2(f2(f1(f2(f1(x2752341),x2752342)),f2(f1(f2(x2752343,x2752341)),f2(x2752343,x2752342))),x2752344))),
% 184.86/185.04 inference(scs_inference,[],[275196,274209,8])).
% 184.86/185.04 cnf(275243,plain,
% 184.86/185.04 (~P2(f2(f1(f2(f1(x2752431),f2(x2752432,x2752431))),f2(f1(f2(f2(a4,a3),a3)),f2(a4,a3))))),
% 184.86/185.04 inference(scs_inference,[],[275209,274205,8])).
% 184.86/185.04 cnf(275252,plain,
% 184.86/185.04 (P2(f2(x2752521,f2(f1(f2(x2752522,x2752523)),f2(x2752522,f2(x2752524,x2752523)))))),
% 184.86/185.04 inference(scs_inference,[],[275223,274205,8])).
% 184.86/185.04 cnf(275259,plain,
% 184.86/185.04 (P2(f2(f1(f2(x2752591,x2752592)),f2(x2752591,f2(x2752593,x2752592))))),
% 184.86/185.04 inference(scs_inference,[],[275252,275234,8])).
% 184.86/185.04 cnf(275299,plain,
% 184.86/185.04 (P2(f2(f1(f2(x2752991,x2752992)),f2(x2752993,f2(x2752991,f2(x2752994,x2752992)))))),
% 184.86/185.04 inference(scs_inference,[],[275252,274217,8])).
% 184.86/185.04 cnf(275311,plain,
% 184.86/185.04 (P2(f2(f2(f1(f2(x2753111,x2753112)),f2(x2753111,f2(x2753113,x2753112))),x2753114))),
% 184.86/185.04 inference(scs_inference,[],[275252,274209,8])).
% 184.86/185.04 cnf(275319,plain,
% 184.86/185.04 (~P2(f2(f1(f2(f1(x2753191),f2(x2753192,x2753191))),f2(a4,a3)))),
% 184.86/185.05 inference(scs_inference,[],[275259,275243,8])).
% 184.86/185.05 cnf(275323,plain,
% 184.86/185.05 (P2(f2(x2753231,f2(f1(f2(x2753232,f2(x2753233,x2753234))),f2(x2753232,f2(x2753233,f2(x2753235,x2753234))))))),
% 184.86/185.05 inference(scs_inference,[],[275259,275223,8])).
% 184.86/185.05 cnf(275332,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2753321,f2(x2753322,x2753323))),f2(x2753321,f2(x2753322,f2(x2753324,x2753323)))))),
% 184.86/185.05 inference(scs_inference,[],[275259,275323,8])).
% 184.86/185.05 cnf(275413,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2754131,f2(x2754132,x2754133))),f2(x2754131,f2(x2754134,f2(x2754132,f2(x2754135,x2754133))))))),
% 184.86/185.05 inference(scs_inference,[],[275299,274219,8])).
% 184.86/185.05 cnf(275420,plain,
% 184.86/185.05 (P2(f2(x2754201,f2(f2(f1(f2(f1(x2754202),x2754203)),f2(f1(f2(x2754204,x2754202)),f2(x2754204,x2754203))),f2(x2754205,x2754206))))),
% 184.86/185.05 inference(scs_inference,[],[275299,275234,8])).
% 184.86/185.05 cnf(275429,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2754291,x2754292)),f2(x2754293,f2(x2754291,f2(x2754294,f2(x2754295,x2754292))))))),
% 184.86/185.05 inference(scs_inference,[],[275413,275259,8])).
% 184.86/185.05 cnf(275442,plain,
% 184.86/185.05 (P2(f2(x2754421,f2(f1(f2(x2754422,x2754423)),f2(x2754424,f2(x2754425,f2(x2754423,x2754422))))))),
% 184.86/185.05 inference(scs_inference,[],[275429,274209,8])).
% 184.86/185.05 cnf(275448,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2754481,x2754482)),f2(x2754483,f2(x2754484,f2(x2754482,x2754481)))))),
% 184.86/185.05 inference(scs_inference,[],[275311,275442,8])).
% 184.86/185.05 cnf(275456,plain,
% 184.86/185.05 (P2(f2(x2754561,f2(x2754562,f2(f2(f1(f2(f1(x2754563),x2754564)),f2(f1(f2(x2754565,x2754563)),f2(x2754565,x2754564))),f2(x2754566,x2754567)))))),
% 184.86/185.05 inference(scs_inference,[],[275420,275259,8])).
% 184.86/185.05 cnf(275463,plain,
% 184.86/185.05 (~P2(f2(f1(f2(f1(f2(x2754631,x2754632)),f2(x2754631,f2(x2754633,x2754632)))),f2(f1(f2(f1(x2754634),f2(x2754635,x2754634))),f2(a4,a3))))),
% 184.86/185.05 inference(scs_inference,[],[275319,275259,7,8])).
% 184.86/185.05 cnf(275470,plain,
% 184.86/185.05 (P2(f2(f2(x2754701,f2(f2(f1(f2(f1(x2754702),x2754703)),f2(f1(f2(x2754704,x2754702)),f2(x2754704,x2754703))),f2(x2754705,x2754706))),x2754707))),
% 184.86/185.05 inference(scs_inference,[],[275456,274209,8])).
% 184.86/185.05 cnf(275481,plain,
% 184.86/185.05 (P2(f2(x2754811,f2(f2(x2754812,f2(f2(f1(f2(f1(x2754813),x2754814)),f2(f1(f2(x2754815,x2754813)),f2(x2754815,x2754814))),f2(x2754816,x2754817))),f2(x2754818,x2754819))))),
% 184.86/185.05 inference(scs_inference,[],[275470,275299,8])).
% 184.86/185.05 cnf(275485,plain,
% 184.86/185.05 (~P2(f2(f1(f2(f1(x2754851),f2(x2754852,x2754851))),f2(f1(f2(f1(x2754853),f2(x2754854,x2754853))),f2(a4,a3))))),
% 184.86/185.05 inference(scs_inference,[],[275319,274205,8])).
% 184.86/185.05 cnf(275490,plain,
% 184.86/185.05 (~P2(f2(a3,a4))),
% 184.86/185.05 inference(scs_inference,[],[275485,275448,8])).
% 184.86/185.05 cnf(275494,plain,
% 184.86/185.05 (P2(f2(f2(f2(x2754941,f2(f2(f1(f2(f1(x2754942),x2754943)),f2(f1(f2(x2754944,x2754942)),f2(x2754944,x2754943))),f2(x2754945,x2754946))),f2(x2754947,x2754948)),x2754949))),
% 184.86/185.05 inference(scs_inference,[],[275481,274209,8])).
% 184.86/185.05 cnf(275505,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2755051,f2(x2755052,x2755053))),f2(x2755054,f2(x2755051,f2(x2755052,f2(x2755055,x2755053))))))),
% 184.86/185.05 inference(scs_inference,[],[275323,274217,8])).
% 184.86/185.05 cnf(275521,plain,
% 184.86/185.05 (P2(f2(x2755211,f2(f1(f2(x2755211,f2(x2755212,x2755213))),f2(x2755212,f2(x2755214,x2755213)))))),
% 184.86/185.05 inference(scs_inference,[],[275332,274217,8])).
% 184.86/185.05 cnf(275535,plain,
% 184.86/185.05 (P2(f2(x2755351,f2(f1(f2(x2755351,f2(x2755352,x2755353))),f2(x2755354,f2(x2755352,f2(x2755355,x2755353))))))),
% 184.86/185.05 inference(scs_inference,[],[275332,275521,8])).
% 184.86/185.05 cnf(275546,plain,
% 184.86/185.05 (P2(f2(f2(x2755461,f2(x2755462,f2(x2755463,x2755464))),f1(f2(x2755461,f2(x2755462,x2755464)))))),
% 184.86/185.05 inference(scs_inference,[],[275332,274209,8])).
% 184.86/185.05 cnf(275554,plain,
% 184.86/185.05 (P2(f2(x2755541,f2(f1(f2(x2755542,x2755543)),f2(x2755542,f2(x2755544,f2(x2755545,x2755543))))))),
% 184.86/185.05 inference(scs_inference,[],[275505,275259,8])).
% 184.86/185.05 cnf(275559,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2755591,x2755592)),f2(x2755591,f2(x2755593,f2(x2755594,x2755592)))))),
% 184.86/185.05 inference(scs_inference,[],[275535,275554,8])).
% 184.86/185.05 cnf(275566,plain,
% 184.86/185.05 (P2(f2(x2755661,f2(f1(f2(x2755662,x2755662)),f2(x2755663,f2(x2755664,x2755662)))))),
% 184.86/185.05 inference(scs_inference,[],[275429,274213,8])).
% 184.86/185.05 cnf(275573,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2755731,x2755731)),f2(x2755732,f2(x2755733,x2755731))))),
% 184.86/185.05 inference(scs_inference,[],[275566,275546,8])).
% 184.86/185.05 cnf(275644,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2756441,f2(x2756442,x2756443))),f2(x2756444,f2(x2756442,f2(x2756445,f2(x2756441,x2756443))))))),
% 184.86/185.05 inference(scs_inference,[],[275413,274217,8])).
% 184.86/185.05 cnf(275658,plain,
% 184.86/185.05 (P2(f2(x2756581,f2(f1(x2756582),f2(x2756583,f2(x2756584,f2(x2756585,x2756582))))))),
% 184.86/185.05 inference(scs_inference,[],[275429,274205,8])).
% 184.86/185.05 cnf(275662,plain,
% 184.86/185.05 (P2(f2(f1(x2756621),f2(x2756622,f2(x2756623,f2(x2756624,x2756621)))))),
% 184.86/185.05 inference(scs_inference,[],[275429,275658,8])).
% 184.86/185.05 cnf(275684,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2756841,x2756842)),f2(x2756843,f2(x2756844,f2(x2756845,f2(x2756842,x2756841))))))),
% 184.86/185.05 inference(scs_inference,[],[275442,274217,8])).
% 184.86/185.05 cnf(275692,plain,
% 184.86/185.05 (P2(f2(x2756921,f2(x2756922,f2(f2(x2756923,f2(x2756924,f2(x2756925,x2756926))),f1(x2756926)))))),
% 184.86/185.05 inference(scs_inference,[],[275448,275662,8])).
% 184.86/185.05 cnf(275696,plain,
% 184.86/185.05 (P2(f2(x2756961,f2(f2(x2756962,f2(x2756963,f2(x2756964,x2756965))),f1(x2756965))))),
% 184.86/185.05 inference(scs_inference,[],[275448,275692,8])).
% 184.86/185.05 cnf(275700,plain,
% 184.86/185.05 (~P2(f2(f1(f2(f1(f2(x2757001,x2757002)),f2(x2757003,f2(x2757004,f2(x2757002,x2757001))))),f2(a3,a4)))),
% 184.86/185.05 inference(scs_inference,[],[275448,275490,8])).
% 184.86/185.05 cnf(275716,plain,
% 184.86/185.05 (P2(f2(x2757161,f2(x2757162,f2(f2(f2(x2757163,f2(x2757164,f2(x2757165,x2757166))),f1(x2757166)),x2757167))))),
% 184.86/185.05 inference(scs_inference,[],[275448,275696,8])).
% 184.86/185.05 cnf(275721,plain,
% 184.86/185.05 (P2(f2(x2757211,f2(f2(f2(x2757212,f2(x2757213,f2(x2757214,x2757215))),f1(x2757215)),x2757216)))),
% 184.86/185.05 inference(scs_inference,[],[275448,275716,8])).
% 184.86/185.05 cnf(275734,plain,
% 184.86/185.05 (P2(f2(f2(f2(x2757341,f2(x2757342,f2(x2757343,x2757344))),f1(x2757344)),x2757345))),
% 184.86/185.05 inference(scs_inference,[],[275684,275721,8])).
% 184.86/185.05 cnf(275745,plain,
% 184.86/185.05 (P2(f2(x2757451,f2(x2757452,f2(x2757453,f2(f2(x2757454,f2(x2757455,f2(x2757456,x2757457))),f1(x2757457))))))),
% 184.86/185.05 inference(scs_inference,[],[275463,275734,275448,7,8])).
% 184.86/185.05 cnf(275802,plain,
% 184.86/185.05 (P2(f2(x2758021,f2(x2758022,f2(f2(x2758023,f2(x2758024,f2(x2758025,x2758026))),f2(x2758027,f1(x2758026))))))),
% 184.86/185.05 inference(scs_inference,[],[275505,275696,8])).
% 184.86/185.05 cnf(275807,plain,
% 184.86/185.05 (P2(f2(x2758071,f2(f2(x2758072,f2(x2758073,f2(x2758074,x2758075))),f2(x2758076,f1(x2758075)))))),
% 184.86/185.05 inference(scs_inference,[],[275802,275535,8])).
% 184.86/185.05 cnf(275816,plain,
% 184.86/185.05 (P2(f2(f2(x2758161,f2(x2758162,f2(x2758163,x2758164))),f2(x2758165,f1(x2758164))))),
% 184.86/185.05 inference(scs_inference,[],[275807,275734,8])).
% 184.86/185.05 cnf(275820,plain,
% 184.86/185.05 (P2(f2(x2758201,f2(f2(x2758202,f2(x2758203,f2(x2758204,x2758205))),f2(x2758206,f2(x2758207,f1(x2758205))))))),
% 184.86/185.05 inference(scs_inference,[],[275816,275505,8])).
% 184.86/185.05 cnf(275829,plain,
% 184.86/185.05 (P2(f2(x2758291,f2(x2758292,f2(x2758293,f2(f1(f2(x2758294,x2758294)),f2(x2758295,x2758294))))))),
% 184.86/185.05 inference(scs_inference,[],[275644,275573,8])).
% 184.86/185.05 cnf(275834,plain,
% 184.86/185.05 (P2(f2(x2758341,f2(x2758342,f2(f1(f2(x2758343,x2758343)),f2(x2758344,x2758343)))))),
% 184.86/185.05 inference(scs_inference,[],[275494,275829,8])).
% 184.86/185.05 cnf(275856,plain,
% 184.86/185.05 (P2(f2(x2758561,f2(f1(f2(x2758562,x2758562)),f2(x2758563,x2758562))))),
% 184.86/185.05 inference(scs_inference,[],[275716,275834,8])).
% 184.86/185.05 cnf(275869,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2758691,x2758691)),f2(x2758692,x2758691)))),
% 184.86/185.05 inference(scs_inference,[],[275745,275856,8])).
% 184.86/185.05 cnf(275942,plain,
% 184.86/185.05 (P2(f2(x2759421,f2(x2759422,f2(f1(f2(x2759421,f2(x2759423,x2759424))),f2(x2759423,f2(x2759425,x2759424))))))),
% 184.86/185.05 inference(scs_inference,[],[275521,275259,8])).
% 184.86/185.05 cnf(276009,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2760091,f2(x2760092,x2760093))),f2(x2760094,f2(x2760095,f2(x2760092,f2(x2760091,x2760093))))))),
% 184.86/185.05 inference(scs_inference,[],[275559,274217,8])).
% 184.86/185.05 cnf(276122,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2761221,x2761222)),f2(x2761221,f2(x2761223,f2(x2761224,f2(x2761225,x2761222))))))),
% 184.86/185.05 inference(scs_inference,[],[275662,274219,8])).
% 184.86/185.05 cnf(276158,plain,
% 184.86/185.05 (P2(f2(x2761581,f2(f1(f2(x2761581,x2761582)),f2(x2761583,f2(x2761584,f2(x2761585,x2761582))))))),
% 184.86/185.05 inference(scs_inference,[],[275700,276122,274217,7,8])).
% 184.86/185.05 cnf(276168,plain,
% 184.86/185.05 (P2(f2(f2(f1(f2(x2761681,x2761682)),f2(x2761683,f2(x2761684,f2(x2761685,x2761682)))),x2761681))),
% 184.86/185.05 inference(scs_inference,[],[276158,274209,8])).
% 184.86/185.05 cnf(276303,plain,
% 184.86/185.05 (P2(f2(f2(f2(x2763031,f2(x2763032,f2(x2763033,x2763034))),f2(x2763035,f2(x2763036,f1(x2763034)))),x2763037))),
% 184.86/185.05 inference(scs_inference,[],[275820,274209,8])).
% 184.86/185.05 cnf(276374,plain,
% 184.86/185.05 (P2(f2(x2763741,f2(f1(f2(f1(f2(f1(f2(x2763742,x2763742)),f2(x2763743,x2763742))),f2(x2763744,x2763745))),f2(x2763744,f2(x2763746,x2763745)))))),
% 184.86/185.05 inference(scs_inference,[],[275869,275942,8])).
% 184.86/185.05 cnf(276381,plain,
% 184.86/185.05 (P2(f2(f1(f2(f1(f2(f1(f2(x2763811,x2763811)),f2(x2763812,x2763811))),f2(x2763813,x2763814))),f2(x2763813,f2(x2763815,x2763814))))),
% 184.86/185.05 inference(scs_inference,[],[275869,276374,8])).
% 184.86/185.05 cnf(276385,plain,
% 184.86/185.05 (P2(f2(f1(f2(f1(f2(f1(f2(x2763851,x2763851)),f2(x2763852,x2763851))),f2(x2763853,x2763854))),f2(x2763855,f2(x2763853,f2(x2763856,x2763854)))))),
% 184.86/185.05 inference(scs_inference,[],[275869,275535,8])).
% 184.86/185.05 cnf(276394,plain,
% 184.86/185.05 (P2(f2(x2763941,f2(x2763942,f2(f1(f2(x2763943,f2(x2763944,x2763944))),f2(x2763943,f2(x2763945,x2763944))))))),
% 184.86/185.05 inference(scs_inference,[],[276381,275223,8])).
% 184.86/185.05 cnf(276399,plain,
% 184.86/185.05 (P2(f2(x2763991,f2(f1(f2(x2763992,f2(x2763993,x2763993))),f2(x2763992,f2(x2763994,x2763993)))))),
% 184.86/185.05 inference(scs_inference,[],[275869,276394,8])).
% 184.86/185.05 cnf(276406,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2764061,f2(x2764062,x2764062))),f2(x2764061,f2(x2764063,x2764062))))),
% 184.86/185.05 inference(scs_inference,[],[275869,276399,8])).
% 184.86/185.05 cnf(276419,plain,
% 184.86/185.05 (P2(f2(x2764191,f2(f1(f2(x2764192,f2(x2764193,x2764193))),f2(x2764194,f2(x2764192,f2(x2764195,x2764193))))))),
% 184.86/185.05 inference(scs_inference,[],[276385,276399,8])).
% 184.86/185.05 cnf(276424,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2764241,f2(x2764242,x2764242))),f2(x2764243,f2(x2764241,f2(x2764244,x2764242)))))),
% 184.86/185.05 inference(scs_inference,[],[276419,276406,8])).
% 184.86/185.05 cnf(276482,plain,
% 184.86/185.05 (P2(f2(x2764821,f2(f2(f2(x2764822,f2(x2764823,f2(x2764824,x2764825))),f2(x2764826,f2(x2764827,f1(x2764825)))),f2(x2764828,x2764829))))),
% 184.86/185.05 inference(scs_inference,[],[276303,276424,8])).
% 184.86/185.05 cnf(276803,plain,
% 184.86/185.05 (P2(f2(x2768031,f2(x2768032,f2(f1(f2(x2768032,f2(x2768033,x2768034))),f2(x2768033,f2(x2768035,x2768034))))))),
% 184.86/185.05 inference(scs_inference,[],[275942,274217,8])).
% 184.86/185.05 cnf(276819,plain,
% 184.86/185.05 (P2(f2(f2(f1(f2(x2768191,x2768192)),f2(x2768193,f2(x2768194,f2(x2768195,x2768192)))),f2(x2768196,f2(x2768197,f2(x2768198,x2768191)))))),
% 184.86/185.05 inference(scs_inference,[],[276168,276122,8])).
% 184.86/185.05 cnf(276855,plain,
% 184.86/185.05 (P2(f2(f2(f2(f2(x2768551,f2(x2768552,f2(x2768553,x2768554))),f2(x2768555,f2(x2768556,f1(x2768554)))),f2(x2768557,x2768558)),x2768559))),
% 184.86/185.05 inference(scs_inference,[],[276482,274209,8])).
% 184.86/185.05 cnf(276893,plain,
% 184.86/185.05 (P2(f2(x2768931,f2(f1(f2(x2768932,f2(x2768933,x2768934))),f2(x2768935,f2(x2768933,f2(x2768932,x2768934))))))),
% 184.86/185.05 inference(scs_inference,[],[276009,274217,8])).
% 184.86/185.05 cnf(276898,plain,
% 184.86/185.05 (P2(f2(f1(f2(x2768981,f2(x2768982,x2768983))),f2(x2768984,f2(x2768982,f2(x2768981,x2768983)))))),
% 184.86/185.05 inference(scs_inference,[],[276893,276855,8])).
% 184.86/185.05 cnf(277010,plain,
% 184.86/185.05 (P2(f2(x2770101,f2(f1(f2(f2(x2770102,x2770103),x2770103)),f2(x2770104,f2(x2770105,f2(x2770102,x2770103))))))),
% 184.86/185.05 inference(scs_inference,[],[276819,275869,8])).
% 184.86/185.05 cnf(277026,plain,
% 184.86/185.05 (P2(f2(f1(f2(f2(x2770261,x2770262),x2770262)),f2(x2770263,f2(x2770264,f2(x2770261,x2770262)))))),
% 184.86/185.05 inference(scs_inference,[],[276394,277010,8])).
% 184.86/185.05 cnf(277039,plain,
% 184.86/185.05 (P2(f2(x2770391,f2(x2770392,f2(f1(f2(f2(x2770393,x2770394),x2770394)),f2(x2770395,f2(x2770393,x2770394))))))),
% 184.86/185.05 inference(scs_inference,[],[277026,276898,8])).
% 184.86/185.05 cnf(277050,plain,
% 184.86/185.05 (P2(f2(x2770501,f2(f1(f2(f2(x2770502,x2770503),x2770503)),f2(x2770504,f2(x2770502,x2770503)))))),
% 184.86/185.05 inference(scs_inference,[],[276419,277039,8])).
% 184.86/185.05 cnf(277061,plain,
% 184.86/185.05 (P2(f2(f1(f2(f2(x2770611,x2770612),x2770612)),f2(x2770613,f2(x2770611,x2770612))))),
% 184.86/185.05 inference(scs_inference,[],[277050,276803,8])).
% 184.86/185.05 cnf(279449,plain,
% 184.86/185.05 ($false),
% 184.86/185.05 inference(scs_inference,[],[274217,275214,277061,8]),
% 184.86/185.05 ['proof']).
% 184.98/185.14 % SZS output end Proof
% 184.98/185.14 % Total time :184.167350s
%------------------------------------------------------------------------------