%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYO674-1 : TPTP v8.2.0. Released v7.3.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 20:27:44 EDT 2024
% Result : Unsatisfiable 58.39s 58.45s
% Output : CNFRefutation 58.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO674-1 : TPTP v8.2.0. Released v7.3.0.
% 0.00/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 09:01:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.58 start to proof:theBenchmark
% 58.39/58.43 %-------------------------------------------
% 58.39/58.43 % File :CSE---1.7
% 58.39/58.43 % Problem :theBenchmark
% 58.39/58.43 % Transform :cnf
% 58.39/58.43 % Format :tptp:raw
% 58.39/58.43 % Command :java -jar mcs_scs.jar %d %s
% 58.39/58.43
% 58.39/58.43 % Result :Theorem 57.800000s
% 58.39/58.43 % Output :CNFRefutation 57.800000s
% 58.39/58.43 %-------------------------------------------
% 58.39/58.44 %------------------------------------------------------------------------------
% 58.39/58.44 % File : SYO674-1 : TPTP v8.2.0. Released v7.3.0.
% 58.39/58.44 % Domain : Syntactic
% 58.39/58.44 % Problem : GSM_3_5_1
% 58.39/58.44 % Version : Especial.
% 58.39/58.44 % English :
% 58.39/58.44
% 58.39/58.44 % Refs : [EH+16] Ebner et al. (2016), System Description: GAPT 2.0
% 58.39/58.44 % : [Cer18] Cerna (2018), Email to Geoff Sutcliffe
% 58.39/58.44 % Source : [Cer18]
% 58.39/58.44 % Names : GSM_3_5_1 [Cer18]
% 58.39/58.44
% 58.39/58.44 % Status : Unsatisfiable
% 58.39/58.44 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.33 v7.3.0
% 58.39/58.44 % Syntax : Number of clauses : 14 ( 2 unt; 6 nHn; 13 RR)
% 58.39/58.44 % Number of literals : 80 ( 0 equ; 64 neg)
% 58.39/58.44 % Maximal clause size : 17 ( 5 avg)
% 58.39/58.44 % Maximal term depth : 4 ( 2 avg)
% 58.39/58.44 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty)
% 58.39/58.44 % Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% 58.39/58.44 % Number of variables : 28 ( 1 sgn)
% 58.39/58.44 % SPC : CNF_UNS_RFO_NEQ_NHN
% 58.39/58.44
% 58.39/58.44 % Comments : Created using the GAPT system - https://github.com/gapt/gapt/blob/
% 58.39/58.44 % master/examples/schema/GradedStrictMonotoneSequenceSchema.scala
% 58.39/58.44 %------------------------------------------------------------------------------
% 58.39/58.44 cnf(clause_193,axiom,
% 58.39/58.44 ( ~ 'E'(s('0'),f(suc(B_233)))
% 58.39/58.44 | ~ 'E'(s('0'),f(suc(B_232)))
% 58.39/58.44 | ~ iLEQ(suc(B_230),suc(B_231))
% 58.39/58.44 | ~ 'E'(s('0'),f(B_229))
% 58.39/58.44 | ~ 'E'(s('0'),f(suc(A_2)))
% 58.39/58.44 | ~ 'E'(s('0'),f(suc(B_229)))
% 58.39/58.44 | ~ 'E'(s('0'),f(B_232))
% 58.39/58.44 | ~ 'E'(s('0'),f(B_233))
% 58.39/58.44 | ~ 'E'(s('0'),f(B_231))
% 58.39/58.44 | ~ iLEQ(suc(A_2),suc(B_229))
% 58.39/58.44 | ~ iLEQ(suc(B_229),suc(B_230))
% 58.39/58.44 | ~ 'E'(s('0'),f(suc(B_231)))
% 58.39/58.44 | ~ 'E'(s('0'),f(B_230))
% 58.39/58.44 | ~ 'E'(s('0'),f(suc(B_230)))
% 58.39/58.44 | ~ iLEQ(suc(B_232),suc(B_233))
% 58.39/58.44 | ~ 'E'(s('0'),f(A_2))
% 58.39/58.44 | ~ iLEQ(suc(B_231),suc(B_232)) ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_298,axiom,
% 58.39/58.44 ( ~ 'LE'(f(B_228),s(s('0')))
% 58.39/58.44 | 'E'(s('0'),f(B_228))
% 58.39/58.44 | 'LE'(f(B_228),s('0')) ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_281,axiom,
% 58.39/58.44 ( ~ 'E'('0',f(A_3))
% 58.39/58.44 | ~ 'E'('0',f(suc(A_3)))
% 58.39/58.44 | iLEQ(suc(A_3),suc(A_3)) ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_176,axiom,
% 58.39/58.44 ( ~ 'LE'(f(B_253),s('0'))
% 58.39/58.44 | 'E'('0',f(B_253))
% 58.39/58.44 | 'LE'(f(B_253),'0') ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_139,axiom,
% 58.39/58.44 ( ~ 'LE'(f(B_158),s(s(s('0'))))
% 58.39/58.44 | 'E'(s(s('0')),f(B_158))
% 58.39/58.44 | 'LE'(f(B_158),s(s('0'))) ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_126,axiom,
% 58.39/58.44 ( ~ 'E'(s(s('0')),f(A_1))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(suc(A_1)))
% 58.39/58.44 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_498,axiom,
% 58.39/58.44 'LE'(f(A),s(s(s('0')))) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_204,axiom,
% 58.39/58.44 ~ 'LE'(f(z),'0') ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_129,axiom,
% 58.39/58.44 ( ~ 'LE'(f(suc(B_158)),s(s(s('0'))))
% 58.39/58.44 | 'E'(s(s('0')),f(suc(B_158)))
% 58.39/58.44 | 'LE'(f(B_158),s(s('0'))) ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_431,axiom,
% 58.39/58.44 ( ~ 'E'(s(s('0')),f(A_1))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(suc(B_163)))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(B_159))
% 58.39/58.44 | ~ iLEQ(suc(B_160),suc(B_161))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(suc(A_1)))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(B_162))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(B_163))
% 58.39/58.44 | ~ iLEQ(suc(B_159),suc(B_160))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(suc(B_161)))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(suc(B_160)))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(suc(B_162)))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(B_160))
% 58.39/58.44 | ~ iLEQ(suc(B_161),suc(B_162))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(B_161))
% 58.39/58.44 | ~ 'E'(s(s('0')),f(suc(B_159)))
% 58.39/58.44 | ~ iLEQ(suc(B_162),suc(B_163))
% 58.39/58.44 | ~ iLEQ(suc(A_1),suc(B_159)) ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_50,axiom,
% 58.39/58.44 ( ~ 'LE'(f(suc(B_253)),s('0'))
% 58.39/58.44 | 'E'('0',f(suc(B_253)))
% 58.39/58.44 | 'LE'(f(B_253),'0') ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_84,axiom,
% 58.39/58.44 ( ~ 'LE'(f(suc(B_228)),s(s('0')))
% 58.39/58.44 | 'E'(s('0'),f(suc(B_228)))
% 58.39/58.44 | 'LE'(f(B_228),s('0')) ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_493,axiom,
% 58.39/58.44 ( ~ 'E'(s('0'),f(A_2))
% 58.39/58.44 | ~ 'E'(s('0'),f(suc(A_2)))
% 58.39/58.44 | iLEQ(suc(A_2),suc(A_2)) ) ).
% 58.39/58.44
% 58.39/58.44 cnf(clause_453,axiom,
% 58.39/58.44 ( ~ iLEQ(suc(A_3),suc(B_254))
% 58.39/58.44 | ~ 'E'('0',f(B_254))
% 58.39/58.44 | ~ 'E'('0',f(suc(B_257)))
% 58.39/58.45 | ~ iLEQ(suc(B_255),suc(B_256))
% 58.39/58.45 | ~ 'E'('0',f(B_258))
% 58.39/58.45 | ~ iLEQ(suc(B_256),suc(B_257))
% 58.39/58.45 | ~ 'E'('0',f(A_3))
% 58.39/58.45 | ~ 'E'('0',f(B_255))
% 58.39/58.45 | ~ 'E'('0',f(suc(B_254)))
% 58.39/58.45 | ~ iLEQ(suc(B_254),suc(B_255))
% 58.39/58.45 | ~ 'E'('0',f(suc(A_3)))
% 58.39/58.45 | ~ 'E'('0',f(suc(B_256)))
% 58.39/58.45 | ~ iLEQ(suc(B_257),suc(B_258))
% 58.39/58.45 | ~ 'E'('0',f(suc(B_255)))
% 58.39/58.45 | ~ 'E'('0',f(suc(B_258)))
% 58.39/58.45 | ~ 'E'('0',f(B_256))
% 58.39/58.45 | ~ 'E'('0',f(B_257)) ) ).
% 58.39/58.45
% 58.39/58.45 %------------------------------------------------------------------------------
% 58.39/58.45 %-------------------------------------------
% 58.39/58.45 % Proof found
% 58.39/58.45 % SZS status Theorem for theBenchmark
% 58.39/58.45 % SZS output start Proof
% 58.39/58.45 %ClaNum:14(EqnAxiom:0)
% 58.39/58.45 %VarNum:97(SingletonVarNum:28)
% 58.39/58.45 %MaxLitNum:17
% 58.39/58.45 %MaxfuncDepth:3
% 58.39/58.45 %SharedTerms:7
% 58.39/58.45 [2]~P1(f1(a4),a2)
% 58.39/58.45 [1]P1(f1(x11),f3(f3(f3(a2))))
% 58.39/58.45 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2)
% 58.39/58.45 [4]P1(f1(x41),f3(a2))+P2(f3(a2),f1(x41))+~P1(f1(x41),f3(f3(a2)))
% 58.39/58.45 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+~P2(a2,f1(f5(x51)))
% 58.39/58.45 [6]P1(f1(x61),a2)+~P1(f1(f5(x61)),f3(a2))+P2(a2,f1(f5(x61)))
% 58.39/58.45 [7]P3(f5(x71),f5(x71))+~P2(f3(a2),f1(x71))+~P2(f3(a2),f1(f5(x71)))
% 58.39/58.45 [8]P1(f1(x81),f3(a2))+~P1(f1(f5(x81)),f3(f3(a2)))+P2(f3(a2),f1(f5(x81)))
% 58.39/58.45 [10]P3(f5(x101),f5(x101))+~P2(f3(f3(a2)),f1(x101))+~P2(f3(f3(a2)),f1(f5(x101)))
% 58.39/58.45 [9]P1(f1(x91),f3(f3(a2)))+P2(f3(f3(a2)),f1(x91))+~P1(f1(x91),f3(f3(f3(a2))))
% 58.39/58.45 [11]P2(f3(f3(a2)),f1(f5(x111)))+P1(f1(x111),f3(f3(a2)))+~P1(f1(f5(x111)),f3(f3(f3(a2))))
% 58.39/58.45 [12]~P3(f5(x126),f5(x125))+~P3(f5(x125),f5(x123))+~P3(f5(x124),f5(x121))+~P3(f5(x123),f5(x122))+~P3(f5(x122),f5(x124))+~P2(a2,f1(x121))+~P2(a2,f1(x122))+~P2(a2,f1(x123))+~P2(a2,f1(x124))+~P2(a2,f1(x125))+~P2(a2,f1(x126))+~P2(a2,f1(f5(x121)))+~P2(a2,f1(f5(x122)))+~P2(a2,f1(f5(x123)))+~P2(a2,f1(f5(x124)))+~P2(a2,f1(f5(x125)))+~P2(a2,f1(f5(x126)))
% 58.39/58.45 [13]~P3(f5(x131),f5(x132))+~P3(f5(x132),f5(x133))+~P3(f5(x133),f5(x134))+~P3(f5(x134),f5(x135))+~P3(f5(x135),f5(x136))+~P2(f3(a2),f1(x133))+~P2(f3(a2),f1(x136))+~P2(f3(a2),f1(x135))+~P2(f3(a2),f1(x134))+~P2(f3(a2),f1(x132))+~P2(f3(a2),f1(x131))+~P2(f3(a2),f1(f5(x131)))+~P2(f3(a2),f1(f5(x132)))+~P2(f3(a2),f1(f5(x133)))+~P2(f3(a2),f1(f5(x134)))+~P2(f3(a2),f1(f5(x135)))+~P2(f3(a2),f1(f5(x136)))
% 58.39/58.45 [14]~P3(f5(x141),f5(x142))+~P3(f5(x143),f5(x141))+~P3(f5(x144),f5(x143))+~P3(f5(x145),f5(x144))+~P3(f5(x146),f5(x145))+~P2(f3(f3(a2)),f1(x145))+~P2(f3(f3(a2)),f1(x146))+~P2(f3(f3(a2)),f1(x142))+~P2(f3(f3(a2)),f1(x144))+~P2(f3(f3(a2)),f1(x143))+~P2(f3(f3(a2)),f1(x141))+~P2(f3(f3(a2)),f1(f5(x141)))+~P2(f3(f3(a2)),f1(f5(x142)))+~P2(f3(f3(a2)),f1(f5(x143)))+~P2(f3(f3(a2)),f1(f5(x144)))+~P2(f3(f3(a2)),f1(f5(x145)))+~P2(f3(f3(a2)),f1(f5(x146)))
% 58.39/58.45 %EqnAxiom
% 58.39/58.45
% 58.39/58.45 %-------------------------------------------
% 58.39/58.47 cnf(15,plain,
% 58.39/58.47 (P1(f1(x151),f3(f3(a2)))+P2(f3(f3(a2)),f1(x151))),
% 58.39/58.47 inference(scs_inference,[],[1,9])).
% 58.39/58.47 cnf(17,plain,
% 58.39/58.47 (P1(f1(x171),f3(f3(a2)))+P2(f3(f3(a2)),f1(f5(x171)))),
% 58.39/58.47 inference(scs_inference,[],[1,9,4,11])).
% 58.39/58.47 cnf(21,plain,
% 58.39/58.47 (P2(a2,f1(a4))+~P1(f1(f5(a4)),f3(f3(a2)))+P2(f3(a2),f1(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[2,3,8])).
% 58.39/58.47 cnf(26,plain,
% 58.39/58.47 (P1(f1(x261),f3(f3(a2)))+P3(f5(x261),f5(x261))+~P2(f3(f3(a2)),f1(f5(x261)))),
% 58.39/58.47 inference(scs_inference,[],[15,10])).
% 58.39/58.47 cnf(27,plain,
% 58.39/58.47 (P3(f5(x271),f5(x271))+P1(f1(x271),f3(f3(a2)))),
% 58.39/58.47 inference(scs_inference,[],[26,17])).
% 58.39/58.47 cnf(28,plain,
% 58.39/58.47 (P2(f3(f3(a2)),f1(f5(x281)))+P1(f1(x281),f3(a2))+P2(f3(a2),f1(f5(x281)))),
% 58.39/58.47 inference(scs_inference,[],[15,8])).
% 58.39/58.47 cnf(30,plain,
% 58.39/58.47 (P2(f3(f3(a2)),f1(f5(x301)))+P1(f1(x301),f3(a2))+P2(f3(a2),f1(x301))),
% 58.39/58.47 inference(scs_inference,[],[17,4])).
% 58.39/58.47 cnf(31,plain,
% 58.39/58.47 (P1(f1(x311),f3(f3(a2)))+~P3(f5(f5(x311)),f5(f5(x311)))+~P2(f3(f3(a2)),f1(f5(f5(x311))))),
% 58.39/58.47 inference(scs_inference,[],[17,14])).
% 58.39/58.47 cnf(32,plain,
% 58.39/58.47 (P1(f1(x321),f3(f3(a2)))+~P2(f3(f3(a2)),f1(f5(x321)))+~P2(f3(f3(a2)),f1(f5(f5(x321))))),
% 58.39/58.47 inference(scs_inference,[],[31,10])).
% 58.39/58.47 cnf(33,plain,
% 58.39/58.47 (~P2(f3(f3(a2)),f1(f5(f5(x331))))+P1(f1(x331),f3(f3(a2)))+P1(f1(f5(x331)),f3(f3(a2)))),
% 58.39/58.47 inference(scs_inference,[],[32,15])).
% 58.39/58.47 cnf(34,plain,
% 58.39/58.47 (P1(f1(x341),f3(f3(a2)))+P1(f1(f5(x341)),f3(f3(a2)))),
% 58.39/58.47 inference(scs_inference,[],[33,17])).
% 58.39/58.47 cnf(36,plain,
% 58.39/58.47 (P2(f3(f3(a2)),f1(f5(f5(x361))))+P1(f1(x361),f3(a2))+P2(f3(a2),f1(f5(x361)))),
% 58.39/58.47 inference(scs_inference,[],[17,8])).
% 58.39/58.47 cnf(37,plain,
% 58.39/58.47 (~P2(f3(f3(a2)),f1(f5(f5(x371))))+P1(f1(x371),f3(f3(a2)))),
% 58.39/58.47 inference(scs_inference,[],[17,32])).
% 58.39/58.47 cnf(38,plain,
% 58.39/58.47 (~P2(f3(f3(a2)),f1(f5(f5(x381))))+P1(f1(x381),f3(a2))+P2(f3(a2),f1(x381))),
% 58.39/58.47 inference(scs_inference,[],[37,4])).
% 58.39/58.47 cnf(40,plain,
% 58.39/58.47 (P2(f3(f3(a2)),f1(f5(f5(a4))))+P2(f3(a2),f1(f5(a4)))+P2(a2,f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[17,21])).
% 58.39/58.47 cnf(42,plain,
% 58.39/58.47 (P1(f1(f5(x421)),f3(f3(a2)))+P1(f1(x421),f3(a2))+P2(f3(a2),f1(x421))),
% 58.39/58.47 inference(scs_inference,[],[34,4])).
% 58.39/58.47 cnf(44,plain,
% 58.39/58.47 (P1(f1(f5(f5(x441))),f3(f3(a2)))+P1(f1(x441),f3(a2))+P2(f3(a2),f1(f5(x441)))),
% 58.39/58.47 inference(scs_inference,[],[34,8])).
% 58.39/58.47 cnf(48,plain,
% 58.39/58.47 (P1(f1(x481),f3(f3(a2)))+P1(f1(f5(f5(x481))),f3(f3(a2)))),
% 58.39/58.47 inference(scs_inference,[],[37,15])).
% 58.39/58.47 cnf(51,plain,
% 58.39/58.47 (P1(f1(x511),f3(f3(a2)))+P1(f1(f5(x511)),f3(a2))+P2(f3(a2),f1(f5(f5(x511))))),
% 58.39/58.47 inference(scs_inference,[],[37,28])).
% 58.39/58.47 cnf(54,plain,
% 58.39/58.47 (P1(f1(f5(f5(x541))),f3(f3(a2)))+P1(f1(x541),f3(a2))+P2(f3(a2),f1(x541))),
% 58.39/58.47 inference(scs_inference,[],[48,4])).
% 58.39/58.47 cnf(58,plain,
% 58.39/58.47 (~P3(f5(a4),f5(a4))+~P2(a2,f1(a4))+~P1(f1(f5(a4)),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[2,6,12])).
% 58.39/58.47 cnf(59,plain,
% 58.39/58.47 (P2(f3(a2),f1(a4))+P2(a2,f1(a4))+~P1(f1(a4),f3(f3(a2)))),
% 58.39/58.47 inference(scs_inference,[],[2,4,3])).
% 58.39/58.47 cnf(62,plain,
% 58.39/58.47 (~P2(f3(f3(a2)),f1(f5(f5(a4))))+P2(f3(a2),f1(a4))+P2(a2,f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[2,38,3])).
% 58.39/58.47 cnf(64,plain,
% 58.39/58.47 (~P1(f1(f5(a4)),f3(a2))+~P2(a2,f1(a4))+~P2(a2,f1(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[5,58])).
% 58.39/58.47 cnf(65,plain,
% 58.39/58.47 (~P2(a2,f1(a4))+~P1(f1(f5(a4)),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[2,64,6])).
% 58.39/58.47 cnf(72,plain,
% 58.39/58.47 (~P1(f1(f5(a4)),f3(a2))+~P1(f1(a4),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[2,65,3])).
% 58.39/58.47 cnf(73,plain,
% 58.39/58.47 (~P1(f1(a4),f3(a2))+P2(f3(a2),f1(f5(a4)))+~P1(f1(f5(a4)),f3(f3(a2)))),
% 58.39/58.47 inference(scs_inference,[],[72,4])).
% 58.39/58.47 cnf(74,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+P2(f3(f3(a2)),f1(f5(a4)))+~P1(f1(a4),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[73,15])).
% 58.39/58.47 cnf(75,plain,
% 58.39/58.47 (P2(f3(f3(a2)),f1(f5(a4)))+P2(f3(a2),f1(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[74,28])).
% 58.39/58.47 cnf(76,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+~P3(f5(f5(a4)),f5(f5(a4)))+~P2(f3(f3(a2)),f1(f5(f5(a4))))),
% 58.39/58.47 inference(scs_inference,[],[75,14])).
% 58.39/58.47 cnf(77,plain,
% 58.39/58.47 (~P2(a2,f1(a4))+~P1(f1(f5(f5(a4))),f3(f3(a2)))+P2(f3(a2),f1(f5(f5(a4))))),
% 58.39/58.47 inference(scs_inference,[],[65,8])).
% 58.39/58.47 cnf(80,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+~P1(f1(f5(a4)),f3(f3(a2)))+~P1(f1(f5(a4)),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[65,21])).
% 58.39/58.47 cnf(81,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+~P1(f1(f5(a4)),f3(f3(a2)))),
% 58.39/58.47 inference(scs_inference,[],[80,4])).
% 58.39/58.47 cnf(84,plain,
% 58.39/58.47 (P2(f3(f3(a2)),f1(f5(f5(a4))))+P2(f3(a2),f1(f5(a4)))+~P2(a2,f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[65,30])).
% 58.39/58.47 cnf(85,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+P2(f3(f3(a2)),f1(f5(f5(a4))))),
% 58.39/58.47 inference(scs_inference,[],[84,40])).
% 58.39/58.47 cnf(96,plain,
% 58.39/58.47 (P2(f3(a2),f1(a4))+~P1(f1(f5(a4)),f3(a2))+~P1(f1(a4),f3(f3(a2)))),
% 58.39/58.47 inference(scs_inference,[],[65,59])).
% 58.39/58.47 cnf(101,plain,
% 58.39/58.47 (P1(f1(f5(f5(a4))),f3(f3(a2)))+P2(f3(a2),f1(f5(a4)))+~P2(a2,f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[65,42])).
% 58.39/58.47 cnf(102,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+P1(f1(f5(f5(a4))),f3(f3(a2)))+~P1(f1(a4),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[2,101,3])).
% 58.39/58.47 cnf(103,plain,
% 58.39/58.47 (P1(f1(f5(f5(a4))),f3(f3(a2)))+P2(f3(a2),f1(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[102,44])).
% 58.39/58.47 cnf(104,plain,
% 58.39/58.47 (P1(f1(f5(f5(a4))),f3(f3(a2)))+~P3(f5(a4),f5(a4))+~P2(f3(a2),f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[103,13])).
% 58.39/58.47 cnf(105,plain,
% 58.39/58.47 (P1(f1(f5(f5(a4))),f3(f3(a2)))+~P2(f3(a2),f1(a4))+~P2(f3(a2),f1(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[104,7])).
% 58.39/58.47 cnf(106,plain,
% 58.39/58.47 (P1(f1(f5(f5(a4))),f3(f3(a2)))+P1(f1(a4),f3(a2))+~P2(f3(a2),f1(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[105,54])).
% 58.39/58.47 cnf(107,plain,
% 58.39/58.47 (P1(f1(f5(f5(a4))),f3(f3(a2)))+P1(f1(a4),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[106,103])).
% 58.39/58.47 cnf(127,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+P3(f5(f5(a4)),f5(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[81,27])).
% 58.39/58.47 cnf(128,plain,
% 58.39/58.47 (P3(f5(f5(a4)),f5(f5(a4)))+~P3(f5(a4),f5(a4))+~P2(f3(a2),f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[127,13])).
% 58.39/58.47 cnf(129,plain,
% 58.39/58.47 (P3(f5(f5(a4)),f5(f5(a4)))+~P2(f3(a2),f1(a4))+~P2(f3(a2),f1(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[128,7])).
% 58.39/58.47 cnf(130,plain,
% 58.39/58.47 (~P2(f3(a2),f1(a4))+P3(f5(f5(a4)),f5(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[129,127])).
% 58.39/58.47 cnf(133,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+~P2(f3(a2),f1(a4))+~P2(f3(f3(a2)),f1(f5(f5(a4))))),
% 58.39/58.47 inference(scs_inference,[],[130,76])).
% 58.39/58.47 cnf(134,plain,
% 58.39/58.47 (~P2(f3(f3(a2)),f1(f5(f5(a4))))+P3(f5(a4),f5(a4))+~P2(f3(a2),f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[133,7])).
% 58.39/58.47 cnf(150,plain,
% 58.39/58.47 (P1(f1(f5(f5(a4))),f3(f3(a2)))+P2(a2,f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[2,107,3])).
% 58.39/58.47 cnf(153,plain,
% 58.39/58.47 (P2(a2,f1(a4))+P1(f1(f5(a4)),f3(a2))+P2(f3(a2),f1(f5(f5(a4))))),
% 58.39/58.47 inference(scs_inference,[],[150,8])).
% 58.39/58.47 cnf(160,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+~P2(f3(f3(a2)),f1(f5(f5(a4))))),
% 58.39/58.47 inference(scs_inference,[],[127,76])).
% 58.39/58.47 cnf(161,plain,
% 58.39/58.47 (~P2(f3(f3(a2)),f1(f5(f5(a4))))+~P3(f5(a4),f5(a4))+~P2(f3(a2),f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[160,13])).
% 58.39/58.47 cnf(162,plain,
% 58.39/58.47 (~P3(f5(a4),f5(a4))+~P2(f3(f3(a2)),f1(f5(f5(a4))))+P1(f1(a4),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[161,38])).
% 58.39/58.47 cnf(163,plain,
% 58.39/58.47 (~P2(f3(a2),f1(a4))+~P2(f3(f3(a2)),f1(f5(f5(a4))))+P1(f1(a4),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[162,134])).
% 58.39/58.47 cnf(164,plain,
% 58.39/58.47 (~P2(f3(f3(a2)),f1(f5(f5(a4))))+P1(f1(a4),f3(a2))+P2(a2,f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[163,62])).
% 58.39/58.47 cnf(165,plain,
% 58.39/58.47 (P2(a2,f1(a4))+P1(f1(a4),f3(a2))+P2(f3(a2),f1(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[164,36])).
% 58.39/58.47 cnf(166,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))+P2(a2,f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[2,165,3])).
% 58.39/58.47 cnf(167,plain,
% 58.39/58.47 (P2(a2,f1(a4))+~P3(f5(a4),f5(a4))+~P2(f3(a2),f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[166,13])).
% 58.39/58.47 cnf(168,plain,
% 58.39/58.47 (~P3(f5(a4),f5(a4))+~P1(f1(a4),f3(f3(a2)))+P2(a2,f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[167,59])).
% 58.39/58.47 cnf(188,plain,
% 58.39/58.47 (P2(f3(a2),f1(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[85,160])).
% 58.39/58.47 cnf(191,plain,
% 58.39/58.47 (P3(f5(a4),f5(a4))+~P2(f3(a2),f1(a4))),
% 58.39/58.47 inference(scs_inference,[],[188,7])).
% 58.39/58.47 cnf(195,plain,
% 58.39/58.47 (P3(f5(a4),f5(a4))+~P1(f1(a4),f3(f3(a2)))+~P1(f1(f5(a4)),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[191,96])).
% 58.39/58.47 cnf(203,plain,
% 58.39/58.47 (P1(f1(f5(a4)),f3(a2))+P2(a2,f1(a4))+P3(f5(f5(a4)),f5(f5(a4)))),
% 58.39/58.47 inference(scs_inference,[],[188,153,7])).
% 58.39/58.47 cnf(230,plain,
% 58.39/58.47 (~P3(f5(a4),f5(a4))+~P1(f1(a4),f3(f3(a2)))+~P1(f1(f5(a4)),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[65,168])).
% 58.39/58.47 cnf(231,plain,
% 58.39/58.47 (~P1(f1(a4),f3(f3(a2)))+~P1(f1(f5(a4)),f3(a2))),
% 58.39/58.47 inference(scs_inference,[],[230,195])).
% 58.39/58.47 cnf(236,plain,
% 58.39/58.47 (~P2(f3(a2),f1(a4))),
% 58.39/58.48 inference(scs_inference,[],[188,191,13])).
% 58.39/58.48 cnf(237,plain,
% 58.39/58.48 (~P1(f1(a4),f3(f3(a2)))+P2(a2,f1(a4))),
% 58.39/58.48 inference(scs_inference,[],[236,59])).
% 58.39/58.48 cnf(239,plain,
% 58.39/58.48 (P2(a2,f1(a4))+P2(f3(f3(a2)),f1(a4))),
% 58.39/58.48 inference(scs_inference,[],[237,15])).
% 58.39/58.48 cnf(252,plain,
% 58.39/58.48 (P2(f3(a2),f1(f5(f5(a4))))+~P1(f1(f5(f5(a4))),f3(f3(a2)))+~P1(f1(a4),f3(f3(a2)))),
% 58.39/58.48 inference(scs_inference,[],[237,77])).
% 58.39/58.48 cnf(253,plain,
% 58.39/58.48 (~P1(f1(f5(f5(a4))),f3(f3(a2)))+~P1(f1(a4),f3(f3(a2)))+P3(f5(f5(a4)),f5(f5(a4)))),
% 58.39/58.48 inference(scs_inference,[],[188,252,7])).
% 58.39/58.48 cnf(273,plain,
% 58.39/58.48 (P2(a2,f1(a4))+~P3(f5(a4),f5(a4))+~P2(f3(f3(a2)),f1(f5(a4)))),
% 58.39/58.48 inference(scs_inference,[],[239,14])).
% 58.39/58.48 cnf(274,plain,
% 58.39/58.48 (P2(a2,f1(a4))+~P2(f3(f3(a2)),f1(a4))+~P2(f3(f3(a2)),f1(f5(a4)))),
% 58.39/58.48 inference(scs_inference,[],[273,10])).
% 58.39/58.48 cnf(275,plain,
% 58.39/58.48 (~P2(f3(f3(a2)),f1(f5(a4)))+~P2(f3(f3(a2)),f1(a4))+~P1(f1(f5(a4)),f3(a2))),
% 58.39/58.48 inference(scs_inference,[],[274,65])).
% 58.39/58.48 cnf(276,plain,
% 58.39/58.48 (~P2(f3(f3(a2)),f1(a4))+~P1(f1(f5(a4)),f3(a2))+P1(f1(a4),f3(a2))),
% 58.39/58.48 inference(scs_inference,[],[236,275,30])).
% 58.39/58.48 cnf(277,plain,
% 58.39/58.48 (~P2(f3(f3(a2)),f1(a4))+~P1(f1(f5(a4)),f3(a2))),
% 58.39/58.48 inference(scs_inference,[],[276,72])).
% 58.39/58.48 cnf(278,plain,
% 58.39/58.48 (~P1(f1(f5(a4)),f3(a2))+P1(f1(a4),f3(f3(a2)))),
% 58.39/58.48 inference(scs_inference,[],[277,15])).
% 58.39/58.48 cnf(279,plain,
% 58.39/58.48 (~P1(f1(f5(a4)),f3(a2))),
% 58.39/58.48 inference(scs_inference,[],[278,231])).
% 58.39/58.48 cnf(280,plain,
% 58.39/58.48 (P2(f3(a2),f1(f5(f5(a4))))+P2(a2,f1(a4))),
% 58.39/58.48 inference(scs_inference,[],[279,153])).
% 58.39/58.48 cnf(282,plain,
% 58.39/58.48 (P3(f5(f5(a4)),f5(f5(a4)))+P2(a2,f1(a4))),
% 58.39/58.48 inference(scs_inference,[],[279,203])).
% 58.39/58.48 cnf(289,plain,
% 58.39/58.48 (P2(a2,f1(a4))+~P3(f5(f5(a4)),f5(f5(a4)))),
% 58.39/58.48 inference(scs_inference,[],[188,280,13])).
% 58.39/58.48 cnf(290,plain,
% 58.39/58.48 (P1(f1(a4),f3(f3(a2)))+P2(f3(a2),f1(f5(f5(a4))))),
% 58.39/58.48 inference(scs_inference,[],[279,51])).
% 58.39/58.48 cnf(292,plain,
% 58.39/58.48 (P1(f1(a4),f3(f3(a2)))+P3(f5(f5(a4)),f5(f5(a4)))),
% 58.39/58.48 inference(scs_inference,[],[188,279,51,7])).
% 58.39/58.48 cnf(295,plain,
% 58.39/58.48 (P2(a2,f1(a4))),
% 58.39/58.48 inference(scs_inference,[],[282,289])).
% 58.39/58.48 cnf(296,plain,
% 58.39/58.48 (P2(f3(a2),f1(f5(f5(a4))))+~P1(f1(f5(f5(a4))),f3(f3(a2)))),
% 58.39/58.48 inference(scs_inference,[],[295,77])).
% 58.39/58.48 cnf(308,plain,
% 58.39/58.48 (P1(f1(a4),f3(f3(a2)))+~P3(f5(f5(a4)),f5(f5(a4)))),
% 58.39/58.48 inference(scs_inference,[],[188,290,13])).
% 58.39/58.48 cnf(309,plain,
% 58.39/58.48 (P1(f1(a4),f3(f3(a2)))),
% 58.39/58.48 inference(scs_inference,[],[292,308])).
% 58.39/58.48 cnf(311,plain,
% 58.39/58.48 (P3(f5(f5(a4)),f5(f5(a4)))+~P1(f1(f5(f5(a4))),f3(f3(a2)))),
% 58.39/58.48 inference(scs_inference,[],[309,253])).
% 58.39/58.48 cnf(314,plain,
% 58.39/58.48 (~P1(f1(f5(f5(a4))),f3(f3(a2)))+~P3(f5(f5(a4)),f5(f5(a4)))),
% 58.39/58.48 inference(scs_inference,[],[188,296,13])).
% 58.39/58.48 cnf(318,plain,
% 58.39/58.48 (~P1(f1(f5(f5(a4))),f3(f3(a2)))),
% 58.39/58.48 inference(scs_inference,[],[311,314])).
% 58.39/58.48 cnf(319,plain,
% 58.39/58.48 (P2(f3(f3(a2)),f1(f5(f5(a4))))),
% 58.39/58.48 inference(scs_inference,[],[318,15])).
% 58.39/58.48 cnf(321,plain,
% 58.39/58.48 (~P2(f3(f3(a2)),f1(f5(f5(f5(a4)))))),
% 58.39/58.48 inference(scs_inference,[],[318,319,27,14])).
% 58.39/58.48 cnf(14717,plain,
% 58.39/58.48 ($false),
% 58.39/58.48 inference(scs_inference,[],[318,321,17]),
% 58.39/58.48 ['proof']).
% 58.52/58.50 % SZS output end Proof
% 58.52/58.50 % Total time :57.800000s
%------------------------------------------------------------------------------