%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYO630-1 : TPTP v8.2.0. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n032.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 20:27:32 EDT 2024
% Result : Unsatisfiable 0.90s 1.06s
% Output : CNFRefutation 0.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : SYO630-1 : TPTP v8.2.0. Released v7.1.0.
% 0.00/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.27 % Computer : n032.cluster.edu
% 0.09/0.27 % Model : x86_64 x86_64
% 0.09/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.27 % Memory : 8042.1875MB
% 0.09/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.27 % CPULimit : 300
% 0.09/0.27 % WCLimit : 300
% 0.09/0.27 % DateTime : Sun Jun 23 07:40:38 EDT 2024
% 0.09/0.27 % CPUTime :
% 0.13/0.46 start to proof:theBenchmark
% 0.90/1.05 %-------------------------------------------
% 0.90/1.05 % File :CSE---1.7
% 0.90/1.05 % Problem :theBenchmark
% 0.90/1.05 % Transform :cnf
% 0.90/1.05 % Format :tptp:raw
% 0.90/1.05 % Command :java -jar mcs_scs.jar %d %s
% 0.90/1.05
% 0.90/1.05 % Result :Theorem 0.570000s
% 0.90/1.06 % Output :CNFRefutation 0.570000s
% 0.90/1.06 %-------------------------------------------
% 0.90/1.06 %------------------------------------------------------------------------------
% 0.90/1.06 % File : SYO630-1 : TPTP v8.2.0. Released v7.1.0.
% 0.90/1.06 % Domain : Syntactic
% 0.90/1.06 % Problem : ECSClauseSet5
% 0.90/1.06 % Version : Especial.
% 0.90/1.06 % English :
% 0.90/1.06
% 0.90/1.06 % Refs : [Cer15] Cerna (2015), Advances in Schematic Cut Elimination
% 0.90/1.06 % : [CL16] Cerna & Leitsch (2016), Schematic Cut Elimination and
% 0.90/1.06 % : [EH+16] Ebner et al. (2016), System Description: GAPT 2.0
% 0.90/1.06 % : [Cer17] Cerna (2017), Email to Geoff Sutcliffe
% 0.90/1.06 % Source : [Cer17]
% 0.90/1.06 % Names : ECSClauseSet5 [Cer17]
% 0.90/1.06
% 0.90/1.06 % Status : Unsatisfiable
% 0.90/1.06 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.1.0
% 0.90/1.06 % Syntax : Number of clauses : 32 ( 20 unt; 6 nHn; 19 RR)
% 0.90/1.06 % Number of literals : 60 ( 0 equ; 30 neg)
% 0.90/1.06 % Maximal clause size : 4 ( 1 avg)
% 0.90/1.06 % Maximal term depth : 6 ( 2 avg)
% 0.90/1.06 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty)
% 0.90/1.06 % Number of functors : 4 ( 4 usr; 1 con; 0-1 aty)
% 0.90/1.06 % Number of variables : 37 ( 2 sgn)
% 0.90/1.06 % SPC : CNF_UNS_RFO_NEQ_NHN
% 0.90/1.06
% 0.90/1.06 % Comments :
% 0.90/1.06 %------------------------------------------------------------------------------
% 0.90/1.06 cnf(clause_8_01,axiom,
% 0.90/1.06 ( 'E'(s(s(s(s(s('0'))))),f(A))
% 0.90/1.06 | 'LE'(f(A),s(s(s(s(s('0')))))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_13_02,axiom,
% 0.90/1.06 iLEQ(A_2,g(A_2)) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_14_03,axiom,
% 0.90/1.06 iLEQ(A_11,g(A_11)) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_18_04,axiom,
% 0.90/1.06 iLEQ(A_14,A_14) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_31_05,axiom,
% 0.90/1.06 ~ 'E'(f(A_8),f(g(A_8))) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_1_06,axiom,
% 0.90/1.06 ( ~ 'LE'(f(A_13),s('0'))
% 0.90/1.06 | ~ iLEQ(A_13,B_8)
% 0.90/1.06 | 'E'('0',f(B_8))
% 0.90/1.06 | 'LE'(f(B_8),'0') ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_6_07,axiom,
% 0.90/1.06 ~ 'LE'(f(A_15),'0') ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_20_08,axiom,
% 0.90/1.06 iLEQ(A_8,A_8) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_19_09,axiom,
% 0.90/1.06 ~ 'E'(f(A_15),f(g(A_15))) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_3_10,axiom,
% 0.90/1.06 ( ~ 'E'(s(s(s(s(s('0'))))),f(A_2))
% 0.90/1.06 | ~ 'E'(s(s(s(s(s('0'))))),f(g(A_2)))
% 0.90/1.06 | 'E'(f(A_2),f(g(A_2))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_21_11,axiom,
% 0.90/1.06 ( ~ 'E'(s(s(s('0'))),f(A_8))
% 0.90/1.06 | ~ 'E'(s(s(s('0'))),f(g(A_8)))
% 0.90/1.06 | 'E'(f(A_8),f(g(A_8))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_27_12,axiom,
% 0.90/1.06 ( ~ 'E'(s(s('0')),f(A_11))
% 0.90/1.06 | ~ 'E'(s(s('0')),f(g(A_11)))
% 0.90/1.06 | 'E'(f(A_11),f(g(A_11))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_30_13,axiom,
% 0.90/1.06 ( ~ 'E'(s('0'),f(A_14))
% 0.90/1.06 | ~ 'E'(s('0'),f(g(A_14)))
% 0.90/1.06 | 'E'(f(A_14),f(g(A_14))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_23_14,axiom,
% 0.90/1.06 ~ 'LE'(f(g(A_15)),'0') ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_16_15,axiom,
% 0.90/1.06 ( ~ 'LE'(f(A_7),s(s(s('0'))))
% 0.90/1.06 | ~ iLEQ(A_7,B_4)
% 0.90/1.06 | 'E'(s(s('0')),f(B_4))
% 0.90/1.06 | 'LE'(f(B_4),s(s('0'))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_7_16,axiom,
% 0.90/1.06 ( ~ 'LE'(f(A_1),s(s(s(s(s('0'))))))
% 0.90/1.06 | ~ iLEQ(A_1,B_0)
% 0.90/1.06 | 'E'(s(s(s(s('0')))),f(B_0))
% 0.90/1.06 | 'LE'(f(B_0),s(s(s(s('0'))))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_26_17,axiom,
% 0.90/1.06 ( ~ 'LE'(f(A_4),s(s(s(s('0')))))
% 0.90/1.06 | ~ iLEQ(A_4,B_2)
% 0.90/1.06 | 'E'(s(s(s('0'))),f(B_2))
% 0.90/1.06 | 'LE'(f(B_2),s(s(s('0')))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_10_18,axiom,
% 0.90/1.06 iLEQ(A_15,g(A_15)) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_4_19,axiom,
% 0.90/1.06 iLEQ(A_5,g(A_5)) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_25_20,axiom,
% 0.90/1.06 iLEQ(A_2,A_2) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_5_21,axiom,
% 0.90/1.06 ~ 'E'(f(A_5),f(g(A_5))) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_0_22,axiom,
% 0.90/1.06 iLEQ(A_14,g(A_14)) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_9_23,axiom,
% 0.90/1.06 iLEQ(A_5,A_5) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_29_24,axiom,
% 0.90/1.06 ( ~ 'E'('0',f(A_15))
% 0.90/1.06 | ~ 'E'('0',f(g(A_15)))
% 0.90/1.06 | 'E'(f(A_15),f(g(A_15))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_22_25,axiom,
% 0.90/1.06 iLEQ(A_8,g(A_8)) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_11_26,axiom,
% 0.90/1.06 ~ 'E'(f(A_2),f(g(A_2))) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_15_27,axiom,
% 0.90/1.06 iLEQ(A_15,A_15) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_28_28,axiom,
% 0.90/1.06 ~ 'E'(f(A_11),f(g(A_11))) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_2_29,axiom,
% 0.90/1.06 iLEQ(A_11,A_11) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_12_30,axiom,
% 0.90/1.06 ( ~ 'E'(s(s(s(s('0')))),f(A_5))
% 0.90/1.06 | ~ 'E'(s(s(s(s('0')))),f(g(A_5)))
% 0.90/1.06 | 'E'(f(A_5),f(g(A_5))) ) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_24_31,axiom,
% 0.90/1.06 ~ 'E'(f(A_14),f(g(A_14))) ).
% 0.90/1.06
% 0.90/1.06 cnf(clause_17_32,axiom,
% 0.90/1.06 ( ~ 'LE'(f(A_10),s(s('0')))
% 0.90/1.06 | ~ iLEQ(A_10,B_6)
% 0.90/1.06 | 'E'(s('0'),f(B_6))
% 0.90/1.06 | 'LE'(f(B_6),s('0')) ) ).
% 0.90/1.06
% 0.90/1.06 %------------------------------------------------------------------------------
% 0.90/1.06 %-------------------------------------------
% 0.90/1.06 % Proof found
% 0.90/1.06 % SZS status Theorem for theBenchmark
% 0.90/1.06 % SZS output start Proof
% 0.90/1.06 %ClaNum:32(EqnAxiom:0)
% 0.90/1.06 %VarNum:58(SingletonVarNum:21)
% 0.90/1.06 %MaxLitNum:4
% 0.90/1.06 %MaxfuncDepth:5
% 0.90/1.06 %SharedTerms:6
% 0.90/1.06 [6]P1(x61,x61)
% 0.90/1.06 [12]P1(x121,f1(x121))
% 0.90/1.06 [13]~P2(f2(x131),a3)
% 0.90/1.06 [20]~P3(f2(x201),f2(f1(x201)))
% 0.90/1.06 [29]P2(f2(x291),f4(f4(f4(f4(f4(a3))))))+P3(f4(f4(f4(f4(f4(a3))))),f2(x291))
% 0.90/1.06 [22]P3(f2(x221),f2(f1(x221)))+~P3(a3,f2(x221))+~P3(a3,f2(f1(x221)))
% 0.90/1.06 [24]~P3(f4(a3),f2(x241))+P3(f2(x241),f2(f1(x241)))+~P3(f4(a3),f2(f1(x241)))
% 0.90/1.06 [25]P3(f2(x251),f2(f1(x251)))+~P3(f4(f4(a3)),f2(f1(x251)))+~P3(f4(f4(a3)),f2(x251))
% 0.90/1.06 [27]P3(f2(x271),f2(f1(x271)))+~P3(f4(f4(f4(a3))),f2(f1(x271)))+~P3(f4(f4(f4(a3))),f2(x271))
% 0.90/1.06 [30]P3(f2(x301),f2(f1(x301)))+~P3(f4(f4(f4(f4(a3)))),f2(f1(x301)))+~P3(f4(f4(f4(f4(a3)))),f2(x301))
% 0.90/1.06 [32]P3(f2(x321),f2(f1(x321)))+~P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x321)))+~P3(f4(f4(f4(f4(f4(a3))))),f2(x321))
% 0.90/1.06 [21]~P1(x212,x211)+~P2(f2(x212),f4(a3))+P3(a3,f2(x211))+P2(f2(x211),a3)
% 0.90/1.06 [23]~P1(x232,x231)+P2(f2(x231),f4(a3))+P3(f4(a3),f2(x231))+~P2(f2(x232),f4(f4(a3)))
% 0.90/1.06 [26]~P1(x262,x261)+P2(f2(x261),f4(f4(a3)))+P3(f4(f4(a3)),f2(x261))+~P2(f2(x262),f4(f4(f4(a3))))
% 0.90/1.06 [28]~P1(x282,x281)+P2(f2(x281),f4(f4(f4(a3))))+P3(f4(f4(f4(a3))),f2(x281))+~P2(f2(x282),f4(f4(f4(f4(a3)))))
% 0.90/1.06 [31]~P1(x312,x311)+P2(f2(x311),f4(f4(f4(f4(a3)))))+P3(f4(f4(f4(f4(a3)))),f2(x311))+~P2(f2(x312),f4(f4(f4(f4(f4(a3))))))
% 0.90/1.06 %EqnAxiom
% 0.90/1.06
% 0.90/1.06 %-------------------------------------------
% 0.90/1.07 cnf(34,plain,
% 0.90/1.07 (~P2(f2(x341),f4(a3))+~P3(a3,f2(f1(x341)))),
% 0.90/1.07 inference(scs_inference,[],[20,13,6,22,21])).
% 0.90/1.07 cnf(37,plain,
% 0.90/1.07 (P2(f2(f1(x371)),f4(f4(a3)))+~P3(f4(f4(a3)),f2(x371))+~P2(f2(x371),f4(f4(f4(a3))))),
% 0.90/1.07 inference(scs_inference,[],[20,12,25,26])).
% 0.90/1.07 cnf(38,plain,
% 0.90/1.07 (P2(f2(f1(x381)),f4(f4(f4(a3))))+~P3(f4(f4(f4(a3))),f2(x381))+~P2(f2(x381),f4(f4(f4(f4(a3)))))),
% 0.90/1.07 inference(scs_inference,[],[20,12,27,28])).
% 0.90/1.07 cnf(45,plain,
% 0.90/1.07 (~P2(f2(x451),f4(a3))+~P2(f2(f1(x451)),f4(a3))),
% 0.90/1.07 inference(scs_inference,[],[13,6,34,21])).
% 0.90/1.07 cnf(46,plain,
% 0.90/1.07 (~P2(f2(x461),f4(a3))+P3(f4(a3),f2(f1(x461)))+~P2(f2(f1(x461)),f4(f4(a3)))),
% 0.90/1.07 inference(scs_inference,[],[6,45,23])).
% 0.90/1.07 cnf(48,plain,
% 0.90/1.07 (~P2(f2(x481),f4(a3))+P3(f4(a3),f2(f1(x481)))+~P2(f2(x481),f4(f4(a3)))),
% 0.90/1.07 inference(scs_inference,[],[12,45,23])).
% 0.90/1.07 cnf(51,plain,
% 0.90/1.07 (P2(f2(x511),f4(f4(f4(f4(a3)))))+P3(f4(f4(f4(f4(a3)))),f2(x511))+P3(f4(f4(f4(f4(f4(a3))))),f2(x511))),
% 0.90/1.07 inference(scs_inference,[],[6,29,31])).
% 0.90/1.07 cnf(53,plain,
% 0.90/1.07 (~P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x531)))+P2(f2(x531),f4(f4(f4(f4(f4(a3))))))),
% 0.90/1.07 inference(scs_inference,[],[20,29,32])).
% 0.90/1.07 cnf(58,plain,
% 0.90/1.07 (~P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x581)))+P2(f2(f1(x581)),f4(f4(f4(f4(a3)))))+P3(f4(f4(f4(f4(a3)))),f2(f1(x581)))),
% 0.90/1.07 inference(scs_inference,[],[12,53,31])).
% 0.90/1.07 cnf(59,plain,
% 0.90/1.07 (P2(f2(f1(x591)),f4(f4(f4(f4(a3)))))+P3(f4(f4(f4(f4(a3)))),f2(f1(x591)))),
% 0.90/1.07 inference(scs_inference,[],[58,51])).
% 0.90/1.07 cnf(60,plain,
% 0.90/1.07 (P3(f4(f4(f4(f4(a3)))),f2(f1(x601)))+~P3(f4(f4(f4(a3))),f2(f1(x601)))+P2(f2(f1(f1(x601))),f4(f4(f4(a3))))),
% 0.90/1.07 inference(scs_inference,[],[59,38])).
% 0.90/1.07 cnf(63,plain,
% 0.90/1.07 (P2(f2(f1(x631)),f4(f4(f4(f4(a3)))))+~P3(f4(f4(f4(f4(a3)))),f2(x631))),
% 0.99/1.07 inference(scs_inference,[],[20,59,30])).
% 0.99/1.07 cnf(66,plain,
% 0.99/1.07 (~P3(f4(f4(f4(f4(a3)))),f2(x661))+P3(f4(f4(f4(a3))),f2(f1(x661)))+P2(f2(f1(x661)),f4(f4(f4(a3))))),
% 0.99/1.07 inference(scs_inference,[],[6,63,28])).
% 0.99/1.07 cnf(67,plain,
% 0.99/1.07 (P3(f4(f4(f4(a3))),f2(f1(f1(x671))))+~P3(f4(f4(f4(a3))),f2(f1(x671)))+P2(f2(f1(f1(x671))),f4(f4(f4(a3))))),
% 0.99/1.07 inference(scs_inference,[],[66,60])).
% 0.99/1.07 cnf(68,plain,
% 0.99/1.07 (P2(f2(f1(f1(x681))),f4(f4(f4(a3))))+~P3(f4(f4(f4(a3))),f2(f1(x681)))),
% 0.99/1.07 inference(scs_inference,[],[20,67,27])).
% 0.99/1.07 cnf(81,plain,
% 0.99/1.07 (P2(f2(f1(f1(x811))),f4(f4(f4(a3))))+P2(f2(f1(x811)),f4(f4(f4(a3))))+~P2(f2(x811),f4(f4(f4(f4(a3)))))),
% 0.99/1.07 inference(scs_inference,[],[12,68,28])).
% 0.99/1.07 cnf(84,plain,
% 0.99/1.07 (P2(f2(f1(f1(x841))),f4(f4(f4(a3))))+P2(f2(f1(x841)),f4(f4(f4(a3))))+~P2(f2(f1(x841)),f4(f4(f4(f4(a3)))))),
% 0.99/1.07 inference(scs_inference,[],[6,68,28])).
% 0.99/1.07 cnf(86,plain,
% 0.99/1.07 (P3(f4(f4(f4(f4(a3)))),f2(f1(x861)))+P2(f2(f1(f1(f1(x861)))),f4(f4(f4(a3))))+P2(f2(f1(f1(x861))),f4(f4(f4(a3))))),
% 0.99/1.07 inference(scs_inference,[],[59,81])).
% 0.99/1.07 cnf(87,plain,
% 0.99/1.07 (P2(f2(f1(f1(x871))),f4(f4(f4(f4(a3)))))+P2(f2(f1(f1(f1(x871)))),f4(f4(f4(a3))))+P2(f2(f1(f1(x871))),f4(f4(f4(a3))))),
% 0.99/1.07 inference(scs_inference,[],[86,63])).
% 0.99/1.07 cnf(88,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(x881)))),f4(f4(f4(a3))))+P2(f2(f1(f1(x881))),f4(f4(f4(a3))))),
% 0.99/1.07 inference(scs_inference,[],[87,84])).
% 0.99/1.07 cnf(90,plain,
% 0.99/1.07 (P2(f2(f1(x901)),f4(f4(f4(f4(a3)))))+~P3(f4(f4(f4(f4(a3)))),f2(f1(f1(x901))))),
% 0.99/1.07 inference(scs_inference,[],[20,59,30])).
% 0.99/1.07 cnf(98,plain,
% 0.99/1.07 (P3(f4(f4(f4(f4(a3)))),f2(f1(x981)))+P3(f4(f4(f4(a3))),f2(f1(x981)))+P2(f2(f1(x981)),f4(f4(f4(a3))))),
% 0.99/1.07 inference(scs_inference,[],[6,59,28])).
% 0.99/1.07 cnf(104,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(x1041)))),f4(f4(f4(a3))))+P3(f4(f4(a3)),f2(f1(f1(f1(x1041)))))+P2(f2(f1(f1(f1(x1041)))),f4(f4(a3)))),
% 0.99/1.07 inference(scs_inference,[],[12,88,26])).
% 0.99/1.07 cnf(105,plain,
% 0.99/1.07 (P2(f2(f1(f1(x1051))),f4(f4(f4(a3))))+P3(f4(f4(a3)),f2(f1(f1(f1(x1051)))))+P2(f2(f1(f1(f1(x1051)))),f4(f4(a3)))),
% 0.99/1.07 inference(scs_inference,[],[6,88,26])).
% 0.99/1.07 cnf(106,plain,
% 0.99/1.07 (~P3(f4(f4(a3)),f2(f1(f1(x1061))))+P3(f4(f4(a3)),f2(f1(f1(f1(x1061)))))+P2(f2(f1(f1(f1(x1061)))),f4(f4(a3)))),
% 0.99/1.07 inference(scs_inference,[],[105,37])).
% 0.99/1.07 cnf(107,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(x1071)))),f4(f4(a3)))+~P3(f4(f4(a3)),f2(f1(f1(x1071))))),
% 0.99/1.07 inference(scs_inference,[],[20,106,25])).
% 0.99/1.07 cnf(119,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(x1191)))),f4(f4(a3)))+P2(f2(f1(f1(x1191))),f4(f4(a3)))+~P2(f2(f1(f1(x1191))),f4(f4(f4(a3))))),
% 0.99/1.07 inference(scs_inference,[],[6,107,26])).
% 0.99/1.07 cnf(120,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(f1(x1201))))),f4(f4(a3)))+P3(f4(f4(a3)),f2(f1(f1(f1(x1201)))))+P2(f2(f1(f1(f1(x1201)))),f4(f4(a3)))),
% 0.99/1.07 inference(scs_inference,[],[119,104])).
% 0.99/1.07 cnf(121,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(x1211)))),f4(f4(a3)))+P2(f2(f1(f1(f1(f1(x1211))))),f4(f4(a3)))),
% 0.99/1.07 inference(scs_inference,[],[120,107])).
% 0.99/1.07 cnf(127,plain,
% 0.99/1.07 (~P3(f4(f4(f4(f4(a3)))),f2(f1(f1(x1271))))+P3(f4(f4(f4(a3))),f2(f1(f1(x1271))))+P2(f2(f1(f1(x1271))),f4(f4(f4(a3))))),
% 0.99/1.07 inference(scs_inference,[],[12,90,28])).
% 0.99/1.07 cnf(128,plain,
% 0.99/1.07 (P3(f4(f4(f4(a3))),f2(f1(f1(x1281))))+P2(f2(f1(f1(x1281))),f4(f4(f4(a3))))),
% 0.99/1.07 inference(scs_inference,[],[127,98])).
% 0.99/1.07 cnf(129,plain,
% 0.99/1.07 (P2(f2(f1(f1(x1291))),f4(f4(f4(a3))))+~P3(f4(f4(f4(a3))),f2(f1(f1(f1(x1291)))))),
% 0.99/1.07 inference(scs_inference,[],[20,128,27])).
% 0.99/1.07 cnf(136,plain,
% 0.99/1.07 (P3(f4(f4(f4(a3))),f2(f1(f1(x1361))))+P3(f4(f4(a3)),f2(f1(f1(x1361))))+P2(f2(f1(f1(x1361))),f4(f4(a3)))),
% 0.99/1.07 inference(scs_inference,[],[6,128,26])).
% 0.99/1.07 cnf(141,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(x1411)))),f4(f4(a3)))+P3(f4(a3),f2(f1(f1(f1(f1(x1411))))))+~P2(f2(f1(f1(f1(x1411)))),f4(a3))),
% 0.99/1.07 inference(scs_inference,[],[121,46])).
% 0.99/1.07 cnf(142,plain,
% 0.99/1.07 (P3(f4(a3),f2(f1(f1(f1(f1(x1421))))))+~P2(f2(f1(f1(f1(x1421)))),f4(a3))),
% 0.99/1.07 inference(scs_inference,[],[141,48])).
% 0.99/1.07 cnf(165,plain,
% 0.99/1.07 (~P3(f4(f4(f4(a3))),f2(f1(f1(f1(x1651)))))+P3(f4(f4(a3)),f2(f1(f1(f1(x1651)))))+P2(f2(f1(f1(f1(x1651)))),f4(f4(a3)))),
% 0.99/1.07 inference(scs_inference,[],[12,129,26])).
% 0.99/1.07 cnf(166,plain,
% 0.99/1.07 (P3(f4(f4(a3)),f2(f1(f1(f1(x1661)))))+P2(f2(f1(f1(f1(x1661)))),f4(f4(a3)))),
% 0.99/1.07 inference(scs_inference,[],[165,136])).
% 0.99/1.07 cnf(167,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(x1671)))),f4(f4(a3)))+~P3(f4(f4(a3)),f2(f1(f1(f1(f1(x1671))))))),
% 0.99/1.07 inference(scs_inference,[],[20,166,25])).
% 0.99/1.07 cnf(177,plain,
% 0.99/1.07 (P3(f4(f4(a3)),f2(f1(f1(f1(x1771)))))+P2(f2(f1(f1(f1(x1771)))),f4(a3))+P3(f4(a3),f2(f1(f1(f1(x1771)))))),
% 0.99/1.07 inference(scs_inference,[],[6,166,23])).
% 0.99/1.07 cnf(182,plain,
% 0.99/1.07 (~P3(f4(f4(a3)),f2(f1(f1(f1(f1(x1821))))))+P2(f2(f1(f1(f1(f1(x1821))))),f4(a3))+P3(f4(a3),f2(f1(f1(f1(f1(x1821))))))),
% 0.99/1.07 inference(scs_inference,[],[12,167,23])).
% 0.99/1.07 cnf(183,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(f1(x1831))))),f4(a3))+P3(f4(a3),f2(f1(f1(f1(f1(x1831))))))),
% 0.99/1.07 inference(scs_inference,[],[182,177])).
% 0.99/1.07 cnf(187,plain,
% 0.99/1.07 (P2(f2(f1(f1(f1(f1(x1871))))),f4(a3))+~P3(f4(a3),f2(f1(f1(f1(x1871)))))),
% 0.99/1.07 inference(scs_inference,[],[20,183,24])).
% 0.99/1.07 cnf(197,plain,
% 0.99/1.07 (~P3(f4(a3),f2(f1(f1(f1(x1971)))))+P3(a3,f2(f1(f1(f1(f1(x1971))))))),
% 0.99/1.07 inference(scs_inference,[],[13,6,187,21])).
% 0.99/1.07 cnf(199,plain,
% 0.99/1.07 (~P3(f4(a3),f2(f1(f1(f1(x1991)))))+~P3(a3,f2(f1(f1(f1(x1991)))))),
% 0.99/1.07 inference(scs_inference,[],[20,197,22])).
% 0.99/1.07 cnf(202,plain,
% 0.99/1.07 (~P3(f4(a3),f2(f1(f1(f1(x2021)))))+~P2(f2(f1(f1(x2021))),f4(a3))),
% 0.99/1.07 inference(scs_inference,[],[13,12,199,21])).
% 0.99/1.07 cnf(203,plain,
% 0.99/1.07 (~P2(f2(f1(f1(f1(x2031)))),f4(a3))),
% 0.99/1.07 inference(scs_inference,[],[202,142])).
% 0.99/1.07 cnf(205,plain,
% 0.99/1.07 (~P2(f2(f1(f1(f1(x2051)))),f4(a3))),
% 0.99/1.07 inference(rename_variables,[],[203])).
% 0.99/1.07 cnf(206,plain,
% 0.99/1.07 ($false),
% 0.99/1.07 inference(scs_inference,[],[203,205,183,187]),
% 0.99/1.07 ['proof']).
% 0.99/1.07 % SZS output end Proof
% 0.99/1.07 % Total time :0.570000s
%------------------------------------------------------------------------------