%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYO650-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 : n021.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:40 EDT 2024
% Result : Unsatisfiable 61.33s 61.82s
% Output : CNFRefutation 61.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SYO650-1 : TPTP v8.2.0. Released v7.3.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sun Jun 23 08:15:39 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.53/0.59 start to proof:theBenchmark
% 61.33/61.80 %-------------------------------------------
% 61.33/61.80 % File :CSE---1.7
% 61.33/61.80 % Problem :theBenchmark
% 61.33/61.80 % Transform :cnf
% 61.33/61.80 % Format :tptp:raw
% 61.33/61.80 % Command :java -jar mcs_scs.jar %d %s
% 61.33/61.80
% 61.33/61.80 % Result :Theorem 60.680000s
% 61.33/61.80 % Output :CNFRefutation 60.680000s
% 61.33/61.80 %-------------------------------------------
% 61.33/61.81 %------------------------------------------------------------------------------
% 61.33/61.81 % File : SYO650-1 : TPTP v8.2.0. Released v7.3.0.
% 61.33/61.81 % Domain : Syntactic
% 61.33/61.81 % Problem : GSM_1_2_3
% 61.33/61.81 % Version : Especial.
% 61.33/61.81 % English :
% 61.33/61.81
% 61.33/61.81 % Refs : [EH+16] Ebner et al. (2016), System Description: GAPT 2.0
% 61.33/61.81 % : [Cer18] Cerna (2018), Email to Geoff Sutcliffe
% 61.33/61.81 % Source : [Cer18]
% 61.33/61.81 % Names : GSM_1_2_3 [Cer18]
% 61.33/61.81
% 61.33/61.81 % Status : Unsatisfiable
% 61.33/61.81 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.3.0
% 61.33/61.81 % Syntax : Number of clauses : 36 ( 2 unt; 26 nHn; 35 RR)
% 61.33/61.81 % Number of literals : 463 ( 0 equ; 395 neg)
% 61.33/61.81 % Maximal clause size : 20 ( 12 avg)
% 61.33/61.81 % Maximal term depth : 5 ( 2 avg)
% 61.33/61.81 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty)
% 61.33/61.81 % Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% 61.33/61.81 % Number of variables : 89 ( 1 sgn)
% 61.33/61.81 % SPC : CNF_UNS_RFO_NEQ_NHN
% 61.33/61.81
% 61.33/61.81 % Comments : Created using the GAPT system - https://github.com/gapt/gapt/blob/
% 61.33/61.81 % master/examples/schema/GradedStrictMonotoneSequenceSchema.scala
% 61.33/61.81 %------------------------------------------------------------------------------
% 61.33/61.81 cnf(clause_338,axiom,
% 61.33/61.81 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.81 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.81 | ~ 'E'('0',f(A_1))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 61.33/61.81 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.81 | ~ 'E'('0',f(B_6))
% 61.33/61.81 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.81 | ~ 'E'('0',f(B_7))
% 61.33/61.81 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.81 | 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.81 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_150,axiom,
% 61.33/61.81 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.81 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.81 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(A_1))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.81 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.81 | ~ 'E'('0',f(B_6))
% 61.33/61.81 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 61.33/61.81 | ~ 'E'('0',f(B_7))
% 61.33/61.81 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.81 | 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.81 | 'E'(f(B_6),f(suc(suc(B_6)))) ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_437,axiom,
% 61.33/61.81 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.81 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.81 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.81 | ~ 'E'('0',f(A_1))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.81 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.81 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.81 | ~ 'E'('0',f(B_6))
% 61.33/61.81 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 61.33/61.81 | ~ 'E'('0',f(B_7))
% 61.33/61.81 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.81 | 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.81 | 'E'(f(B_6),f(suc(suc(B_6)))) ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_211,axiom,
% 61.33/61.81 ( ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.81 | ~ 'E'('0',f(A_1))
% 61.33/61.81 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.81 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.81 | ~ 'E'('0',f(B_6))
% 61.33/61.81 | ~ 'E'('0',f(B_7))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.81 | 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.81 | 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.81 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_436,axiom,
% 61.33/61.81 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.81 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.81 | ~ 'E'('0',f(A_1))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 61.33/61.81 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.81 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.81 | ~ 'E'('0',f(B_6))
% 61.33/61.81 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.81 | ~ 'E'('0',f(B_7))
% 61.33/61.81 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.81 | 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.81 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_419,axiom,
% 61.33/61.81 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.81 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.81 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(A_1))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.81 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.81 | ~ 'E'('0',f(B_6))
% 61.33/61.81 | ~ 'E'('0',f(B_7))
% 61.33/61.81 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.81 | 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.81 | 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.81 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_278,axiom,
% 61.33/61.81 ( ~ 'LE'(f(B_5),s('0'))
% 61.33/61.81 | 'E'('0',f(B_5))
% 61.33/61.81 | 'LE'(f(B_5),'0') ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_217,axiom,
% 61.33/61.81 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.81 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.81 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.81 | ~ 'E'('0',f(A_1))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.81 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.81 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.81 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.81 | ~ 'E'('0',f(B_6))
% 61.33/61.81 | ~ 'E'('0',f(B_7))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.81 | 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.81 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_129,axiom,
% 61.33/61.81 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.81 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.81 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.81 | ~ 'E'('0',f(A_1))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.81 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.81 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.81 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.81 | ~ 'E'('0',f(B_6))
% 61.33/61.81 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 61.33/61.81 | ~ 'E'('0',f(B_7))
% 61.33/61.81 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.81 | 'E'(f(B_6),f(suc(suc(B_6)))) ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_406,axiom,
% 61.33/61.81 'LE'(f(A),s('0')) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_359,axiom,
% 61.33/61.81 ( ~ 'LE'(f(suc(suc(B_5))),s('0'))
% 61.33/61.81 | 'E'('0',f(suc(suc(B_5))))
% 61.33/61.81 | 'LE'(f(B_5),'0') ) ).
% 61.33/61.81
% 61.33/61.81 cnf(clause_109,axiom,
% 61.33/61.81 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.81 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.81 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.81 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.81 | ~ 'E'('0',f(A_1))
% 61.33/61.81 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 61.33/61.81 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.81 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.81 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_110,axiom,
% 61.33/61.82 ( ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | 'E'(f(B_6),f(suc(B_6))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_189,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_309,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_145,axiom,
% 61.33/61.82 ( ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_447,axiom,
% 61.33/61.82 ( ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | 'E'(f(B_6),f(suc(B_6))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_24,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_313,axiom,
% 61.33/61.82 ( ~ 'LE'(f(suc(B_5)),s('0'))
% 61.33/61.82 | 'E'('0',f(suc(B_5)))
% 61.33/61.82 | 'LE'(f(B_5),'0') ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_2,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_333,axiom,
% 61.33/61.82 ( ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_376,axiom,
% 61.33/61.82 ( ~ 'LE'(f(suc(suc(suc(B_5)))),s('0'))
% 61.33/61.82 | 'E'('0',f(suc(suc(suc(B_5)))))
% 61.33/61.82 | 'LE'(f(B_5),'0') ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_308,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_135,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_319,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(A_1))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_345,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_282,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_206,axiom,
% 61.33/61.82 ~ 'LE'(f(z),'0') ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_253,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(suc(A_1)))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_88,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_6),f(suc(B_6))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_167,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_441,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_416,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_64,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_451,axiom,
% 61.33/61.82 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_6))))
% 61.33/61.82 | ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(A_1))))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_6),f(suc(suc(B_6))))
% 61.33/61.82 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 61.33/61.82
% 61.33/61.82 cnf(clause_371,axiom,
% 61.33/61.82 ( ~ iLEQ(suc(A_1),suc(B_6))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(suc(A_1)))
% 61.33/61.82 | ~ 'E'(f(B_7),f(suc(B_7)))
% 61.33/61.82 | ~ 'E'('0',f(A_1))
% 61.33/61.82 | ~ 'E'('0',f(suc(suc(B_7))))
% 61.33/61.82 | ~ iLEQ(suc(B_6),suc(B_7))
% 61.33/61.82 | ~ 'E'('0',f(B_6))
% 61.33/61.82 | ~ 'E'('0',f(B_7))
% 61.33/61.82 | ~ 'E'('0',f(suc(B_6)))
% 61.33/61.82 | 'E'(f(A_1),f(suc(A_1)))
% 61.33/61.82 | 'E'(f(B_6),f(suc(B_6)))
% 61.33/61.82 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 61.33/61.82
% 61.33/61.82 %------------------------------------------------------------------------------
% 61.33/61.82 %-------------------------------------------
% 61.33/61.82 % Proof found
% 61.33/61.82 % SZS status Theorem for theBenchmark
% 61.33/61.82 % SZS output start Proof
% 61.33/61.82 %ClaNum:36(EqnAxiom:0)
% 61.33/61.82 %VarNum:659(SingletonVarNum:89)
% 61.33/61.82 %MaxLitNum:20
% 61.33/61.82 %MaxfuncDepth:4
% 61.33/61.82 %SharedTerms:5
% 61.33/61.82 [2]~P1(f1(a4),a2)
% 61.33/61.82 [1]P1(f1(x11),f3(a2))
% 61.33/61.82 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2)
% 61.33/61.82 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41)))
% 61.33/61.82 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61))))
% 61.33/61.82 [7]P1(f1(x71),a2)+~P1(f1(f5(f5(f5(x71)))),f3(a2))+P2(a2,f1(f5(f5(f5(x71)))))
% 61.33/61.82 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51)))
% 61.33/61.82 [8]P3(f5(x81),f5(x81))+~P2(a2,f1(x81))+~P2(f1(x81),f1(f5(x81)))+P2(f1(x81),f1(f5(f5(x81))))+~P2(a2,f1(f5(x81)))+~P2(a2,f1(f5(f5(x81))))
% 61.33/61.82 [10]P3(f5(x101),f5(x101))+~P2(a2,f1(x101))+~P2(f1(x101),f1(f5(x101)))+~P2(f1(x101),f1(f5(f5(x101))))+~P2(a2,f1(f5(x101)))+~P2(a2,f1(f5(f5(x101))))+~P2(a2,f1(f5(f5(f5(x101)))))
% 61.33/61.82 [9]~P3(f5(x92),f5(x91))+~P3(f5(x93),f5(x92))+P2(f1(x91),f1(f5(x91)))+P2(f1(x92),f1(f5(x92)))+~P2(a2,f1(x91))+P2(f1(x93),f1(f5(x93)))+~P2(a2,f1(x92))+~P2(a2,f1(x93))+~P2(a2,f1(f5(x91)))+~P2(a2,f1(f5(x92)))+~P2(a2,f1(f5(x93)))
% 61.33/61.82 [11]~P3(f5(x112),f5(x111))+~P3(f5(x113),f5(x112))+P2(f1(x111),f1(f5(x111)))+P2(f1(x112),f1(f5(x112)))+~P2(a2,f1(x111))+~P2(f1(x113),f1(f5(x113)))+~P2(a2,f1(x112))+~P2(a2,f1(x113))+~P2(a2,f1(f5(x111)))+~P2(a2,f1(f5(x112)))+~P2(a2,f1(f5(x113)))+P2(f1(x113),f1(f5(f5(x113))))+~P2(a2,f1(f5(f5(x113))))
% 61.33/61.82 [12]~P3(f5(x122),f5(x123))+~P3(f5(x123),f5(x121))+P2(f1(x121),f1(f5(x121)))+P2(f1(x122),f1(f5(x122)))+~P2(a2,f1(x121))+~P2(f1(x123),f1(f5(x123)))+~P2(a2,f1(x122))+~P2(a2,f1(x123))+~P2(a2,f1(f5(x121)))+~P2(a2,f1(f5(x122)))+~P2(a2,f1(f5(x123)))+P2(f1(x123),f1(f5(f5(x123))))+~P2(a2,f1(f5(f5(x123))))
% 61.33/61.83 [13]~P3(f5(x131),f5(x133))+~P3(f5(x132),f5(x131))+P2(f1(x131),f1(f5(x131)))+P2(f1(x132),f1(f5(x132)))+~P2(a2,f1(x131))+~P2(f1(x133),f1(f5(x133)))+~P2(a2,f1(x132))+~P2(a2,f1(x133))+~P2(a2,f1(f5(x133)))+~P2(a2,f1(f5(x131)))+~P2(a2,f1(f5(x132)))+P2(f1(x133),f1(f5(f5(x133))))+~P2(a2,f1(f5(f5(x133))))
% 61.33/61.83 [17]~P3(f5(x172),f5(x171))+~P3(f5(x173),f5(x172))+P2(f1(x171),f1(f5(x171)))+P2(f1(x172),f1(f5(x172)))+~P2(a2,f1(x171))+~P2(f1(x173),f1(f5(x173)))+~P2(a2,f1(x172))+~P2(a2,f1(x173))+~P2(a2,f1(f5(x171)))+~P2(a2,f1(f5(x172)))+~P2(a2,f1(f5(x173)))+~P2(f1(x173),f1(f5(f5(x173))))+~P2(a2,f1(f5(f5(x173))))+~P2(a2,f1(f5(f5(f5(x173)))))
% 61.33/61.83 [18]~P3(f5(x182),f5(x183))+~P3(f5(x183),f5(x181))+P2(f1(x181),f1(f5(x181)))+P2(f1(x182),f1(f5(x182)))+~P2(a2,f1(x181))+~P2(f1(x183),f1(f5(x183)))+~P2(a2,f1(x182))+~P2(a2,f1(x183))+~P2(a2,f1(f5(x181)))+~P2(a2,f1(f5(x182)))+~P2(a2,f1(f5(x183)))+~P2(f1(x183),f1(f5(f5(x183))))+~P2(a2,f1(f5(f5(x183))))+~P2(a2,f1(f5(f5(f5(x183)))))
% 61.33/61.83 [19]~P3(f5(x191),f5(x193))+~P3(f5(x192),f5(x191))+P2(f1(x191),f1(f5(x191)))+P2(f1(x192),f1(f5(x192)))+~P2(a2,f1(x191))+~P2(f1(x193),f1(f5(x193)))+~P2(a2,f1(x192))+~P2(a2,f1(x193))+~P2(a2,f1(f5(x193)))+~P2(a2,f1(f5(x191)))+~P2(a2,f1(f5(x192)))+~P2(f1(x193),f1(f5(f5(x193))))+~P2(a2,f1(f5(f5(x193))))+~P2(a2,f1(f5(f5(f5(x193)))))
% 61.33/61.83 [14]~P3(f5(x142),f5(x143))+~P3(f5(x143),f5(x141))+P2(f1(x141),f1(f5(x141)))+~P2(a2,f1(x141))+~P2(f1(x142),f1(f5(x142)))+~P2(f1(x143),f1(f5(x143)))+~P2(a2,f1(x142))+~P2(a2,f1(x143))+~P2(a2,f1(f5(x141)))+~P2(a2,f1(f5(x142)))+~P2(a2,f1(f5(x143)))+P2(f1(x142),f1(f5(f5(x142))))+P2(f1(x143),f1(f5(f5(x143))))+~P2(a2,f1(f5(f5(x142))))+~P2(a2,f1(f5(f5(x143))))
% 61.33/61.83 [15]~P3(f5(x151),f5(x152))+~P3(f5(x153),f5(x151))+P2(f1(x151),f1(f5(x151)))+~P2(a2,f1(x151))+~P2(f1(x152),f1(f5(x152)))+~P2(f1(x153),f1(f5(x153)))+~P2(a2,f1(x152))+~P2(a2,f1(x153))+~P2(a2,f1(f5(x152)))+~P2(a2,f1(f5(x151)))+~P2(a2,f1(f5(x153)))+P2(f1(x152),f1(f5(f5(x152))))+P2(f1(x153),f1(f5(f5(x153))))+~P2(a2,f1(f5(f5(x152))))+~P2(a2,f1(f5(f5(x153))))
% 61.33/61.83 [16]~P3(f5(x161),f5(x163))+~P3(f5(x163),f5(x162))+P2(f1(x161),f1(f5(x161)))+~P2(a2,f1(x161))+~P2(f1(x162),f1(f5(x162)))+~P2(f1(x163),f1(f5(x163)))+~P2(a2,f1(x162))+~P2(a2,f1(x163))+~P2(a2,f1(f5(x162)))+~P2(a2,f1(f5(x161)))+~P2(a2,f1(f5(x163)))+P2(f1(x162),f1(f5(f5(x162))))+P2(f1(x163),f1(f5(f5(x163))))+~P2(a2,f1(f5(f5(x162))))+~P2(a2,f1(f5(f5(x163))))
% 61.33/61.83 [21]~P3(f5(x212),f5(x211))+~P3(f5(x213),f5(x212))+P2(f1(x211),f1(f5(x211)))+~P2(a2,f1(x211))+~P2(f1(x212),f1(f5(x212)))+~P2(f1(x213),f1(f5(x213)))+~P2(a2,f1(x212))+~P2(a2,f1(x213))+~P2(a2,f1(f5(x211)))+~P2(a2,f1(f5(x212)))+~P2(a2,f1(f5(x213)))+P2(f1(x212),f1(f5(f5(x212))))+~P2(f1(x213),f1(f5(f5(x213))))+~P2(a2,f1(f5(f5(x212))))+~P2(a2,f1(f5(f5(x213))))+~P2(a2,f1(f5(f5(f5(x213)))))
% 61.33/61.83 [22]~P3(f5(x222),f5(x223))+~P3(f5(x223),f5(x221))+P2(f1(x221),f1(f5(x221)))+~P2(a2,f1(x221))+~P2(f1(x222),f1(f5(x222)))+~P2(f1(x223),f1(f5(x223)))+~P2(a2,f1(x222))+~P2(a2,f1(x223))+~P2(a2,f1(f5(x221)))+~P2(a2,f1(f5(x222)))+~P2(a2,f1(f5(x223)))+P2(f1(x222),f1(f5(f5(x222))))+~P2(f1(x223),f1(f5(f5(x223))))+~P2(a2,f1(f5(f5(x222))))+~P2(a2,f1(f5(f5(x223))))+~P2(a2,f1(f5(f5(f5(x223)))))
% 61.33/61.83 [23]~P3(f5(x231),f5(x232))+~P3(f5(x233),f5(x231))+P2(f1(x231),f1(f5(x231)))+~P2(a2,f1(x231))+~P2(f1(x232),f1(f5(x232)))+~P2(f1(x233),f1(f5(x233)))+~P2(a2,f1(x232))+~P2(a2,f1(x233))+~P2(a2,f1(f5(x232)))+~P2(a2,f1(f5(x231)))+~P2(a2,f1(f5(x233)))+P2(f1(x232),f1(f5(f5(x232))))+~P2(f1(x233),f1(f5(f5(x233))))+~P2(a2,f1(f5(f5(x232))))+~P2(a2,f1(f5(f5(x233))))+~P2(a2,f1(f5(f5(f5(x233)))))
% 61.33/61.83 [24]~P3(f5(x241),f5(x243))+~P3(f5(x243),f5(x242))+P2(f1(x241),f1(f5(x241)))+~P2(a2,f1(x241))+~P2(f1(x242),f1(f5(x242)))+~P2(f1(x243),f1(f5(x243)))+~P2(a2,f1(x242))+~P2(a2,f1(x243))+~P2(a2,f1(f5(x242)))+~P2(a2,f1(f5(x241)))+~P2(a2,f1(f5(x243)))+P2(f1(x242),f1(f5(f5(x242))))+~P2(f1(x243),f1(f5(f5(x243))))+~P2(a2,f1(f5(f5(x242))))+~P2(a2,f1(f5(f5(x243))))+~P2(a2,f1(f5(f5(f5(x243)))))
% 61.33/61.83 [25]~P3(f5(x251),f5(x253))+~P3(f5(x252),f5(x251))+P2(f1(x251),f1(f5(x251)))+~P2(a2,f1(x251))+~P2(f1(x252),f1(f5(x252)))+~P2(f1(x253),f1(f5(x253)))+~P2(a2,f1(x252))+~P2(a2,f1(x253))+~P2(a2,f1(f5(x253)))+~P2(a2,f1(f5(x251)))+~P2(a2,f1(f5(x252)))+P2(f1(x252),f1(f5(f5(x252))))+~P2(f1(x253),f1(f5(f5(x253))))+~P2(a2,f1(f5(f5(x253))))+~P2(a2,f1(f5(f5(x252))))+~P2(a2,f1(f5(f5(f5(x253)))))
% 61.33/61.83 [26]~P3(f5(x261),f5(x262))+~P3(f5(x262),f5(x263))+P2(f1(x261),f1(f5(x261)))+~P2(a2,f1(x261))+~P2(f1(x262),f1(f5(x262)))+~P2(f1(x263),f1(f5(x263)))+~P2(a2,f1(x262))+~P2(a2,f1(x263))+~P2(a2,f1(f5(x263)))+~P2(a2,f1(f5(x261)))+~P2(a2,f1(f5(x262)))+P2(f1(x262),f1(f5(f5(x262))))+~P2(f1(x263),f1(f5(f5(x263))))+~P2(a2,f1(f5(f5(x263))))+~P2(a2,f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(f5(x263)))))
% 61.33/61.83 [20]~P3(f5(x202),f5(x203))+~P3(f5(x203),f5(x201))+~P2(f1(x201),f1(f5(x201)))+~P2(a2,f1(x201))+~P2(f1(x202),f1(f5(x202)))+~P2(f1(x203),f1(f5(x203)))+~P2(a2,f1(x202))+~P2(a2,f1(x203))+~P2(a2,f1(f5(x201)))+~P2(a2,f1(f5(x202)))+~P2(a2,f1(f5(x203)))+P2(f1(x201),f1(f5(f5(x201))))+P2(f1(x202),f1(f5(f5(x202))))+P2(f1(x203),f1(f5(f5(x203))))+~P2(a2,f1(f5(f5(x201))))+~P2(a2,f1(f5(f5(x202))))+~P2(a2,f1(f5(f5(x203))))
% 61.33/61.83 [30]~P3(f5(x302),f5(x301))+~P3(f5(x303),f5(x302))+P2(f1(x301),f1(f5(x301)))+~P2(a2,f1(x301))+~P2(f1(x302),f1(f5(x302)))+~P2(f1(x303),f1(f5(x303)))+~P2(a2,f1(x302))+~P2(a2,f1(x303))+~P2(a2,f1(f5(x303)))+~P2(a2,f1(f5(x302)))+~P2(a2,f1(f5(x301)))+~P2(f1(x302),f1(f5(f5(x302))))+~P2(f1(x303),f1(f5(f5(x303))))+~P2(a2,f1(f5(f5(x302))))+~P2(a2,f1(f5(f5(x303))))+~P2(a2,f1(f5(f5(f5(x302)))))+~P2(a2,f1(f5(f5(f5(x303)))))
% 61.33/61.83 [31]~P3(f5(x311),f5(x312))+~P3(f5(x313),f5(x311))+P2(f1(x311),f1(f5(x311)))+~P2(a2,f1(x311))+~P2(f1(x312),f1(f5(x312)))+~P2(f1(x313),f1(f5(x313)))+~P2(a2,f1(x312))+~P2(a2,f1(x313))+~P2(a2,f1(f5(x313)))+~P2(a2,f1(f5(x311)))+~P2(a2,f1(f5(x312)))+~P2(f1(x312),f1(f5(f5(x312))))+~P2(f1(x313),f1(f5(f5(x313))))+~P2(a2,f1(f5(f5(x312))))+~P2(a2,f1(f5(f5(x313))))+~P2(a2,f1(f5(f5(f5(x312)))))+~P2(a2,f1(f5(f5(f5(x313)))))
% 61.33/61.83 [32]~P3(f5(x321),f5(x323))+~P3(f5(x323),f5(x322))+P2(f1(x321),f1(f5(x321)))+~P2(a2,f1(x321))+~P2(f1(x322),f1(f5(x322)))+~P2(f1(x323),f1(f5(x323)))+~P2(a2,f1(x322))+~P2(a2,f1(x323))+~P2(a2,f1(f5(x323)))+~P2(a2,f1(f5(x321)))+~P2(a2,f1(f5(x322)))+~P2(f1(x322),f1(f5(f5(x322))))+~P2(f1(x323),f1(f5(f5(x323))))+~P2(a2,f1(f5(f5(x322))))+~P2(a2,f1(f5(f5(x323))))+~P2(a2,f1(f5(f5(f5(x322)))))+~P2(a2,f1(f5(f5(f5(x323)))))
% 61.33/61.83 [27]~P3(f5(x272),f5(x271))+~P3(f5(x273),f5(x272))+~P2(f1(x271),f1(f5(x271)))+~P2(a2,f1(x271))+~P2(f1(x272),f1(f5(x272)))+~P2(f1(x273),f1(f5(x273)))+~P2(a2,f1(x272))+~P2(a2,f1(x273))+~P2(a2,f1(f5(x271)))+~P2(a2,f1(f5(x272)))+~P2(a2,f1(f5(x273)))+P2(f1(x271),f1(f5(f5(x271))))+P2(f1(x272),f1(f5(f5(x272))))+~P2(f1(x273),f1(f5(f5(x273))))+~P2(a2,f1(f5(f5(x271))))+~P2(a2,f1(f5(f5(x272))))+~P2(a2,f1(f5(f5(x273))))+~P2(a2,f1(f5(f5(f5(x273)))))
% 61.33/61.83 [28]~P3(f5(x282),f5(x283))+~P3(f5(x283),f5(x281))+~P2(f1(x281),f1(f5(x281)))+~P2(a2,f1(x281))+~P2(f1(x282),f1(f5(x282)))+~P2(f1(x283),f1(f5(x283)))+~P2(a2,f1(x282))+~P2(a2,f1(x283))+~P2(a2,f1(f5(x281)))+~P2(a2,f1(f5(x282)))+~P2(a2,f1(f5(x283)))+P2(f1(x281),f1(f5(f5(x281))))+P2(f1(x282),f1(f5(f5(x282))))+~P2(f1(x283),f1(f5(f5(x283))))+~P2(a2,f1(f5(f5(x281))))+~P2(a2,f1(f5(f5(x282))))+~P2(a2,f1(f5(f5(x283))))+~P2(a2,f1(f5(f5(f5(x283)))))
% 61.33/61.83 [29]~P3(f5(x291),f5(x292))+~P3(f5(x292),f5(x293))+~P2(f1(x291),f1(f5(x291)))+~P2(a2,f1(x291))+~P2(f1(x292),f1(f5(x292)))+~P2(f1(x293),f1(f5(x293)))+~P2(a2,f1(x292))+~P2(a2,f1(x293))+~P2(a2,f1(f5(x293)))+~P2(a2,f1(f5(x291)))+~P2(a2,f1(f5(x292)))+P2(f1(x291),f1(f5(f5(x291))))+P2(f1(x292),f1(f5(f5(x292))))+~P2(f1(x293),f1(f5(f5(x293))))+~P2(a2,f1(f5(f5(x293))))+~P2(a2,f1(f5(f5(x291))))+~P2(a2,f1(f5(f5(x292))))+~P2(a2,f1(f5(f5(f5(x293)))))
% 61.33/61.83 [33]~P3(f5(x333),f5(x332))+~P3(f5(x332),f5(x331))+~P2(f1(x331),f1(f5(x331)))+~P2(a2,f1(x331))+~P2(f1(x332),f1(f5(x332)))+~P2(f1(x333),f1(f5(x333)))+~P2(a2,f1(x332))+~P2(a2,f1(x333))+~P2(a2,f1(f5(x331)))+~P2(a2,f1(f5(x332)))+~P2(a2,f1(f5(x333)))+P2(f1(x331),f1(f5(f5(x331))))+~P2(f1(x332),f1(f5(f5(x332))))+~P2(f1(x333),f1(f5(f5(x333))))+~P2(a2,f1(f5(f5(x331))))+~P2(a2,f1(f5(f5(x332))))+~P2(a2,f1(f5(f5(x333))))+~P2(a2,f1(f5(f5(f5(x332)))))+~P2(a2,f1(f5(f5(f5(x333)))))
% 61.33/61.83 [34]~P3(f5(x341),f5(x342))+~P3(f5(x343),f5(x341))+~P2(f1(x341),f1(f5(x341)))+~P2(a2,f1(x341))+~P2(f1(x342),f1(f5(x342)))+~P2(f1(x343),f1(f5(x343)))+~P2(a2,f1(x342))+~P2(a2,f1(x343))+~P2(a2,f1(f5(x341)))+~P2(a2,f1(f5(x343)))+~P2(a2,f1(f5(x342)))+P2(f1(x341),f1(f5(f5(x341))))+~P2(f1(x342),f1(f5(f5(x342))))+~P2(f1(x343),f1(f5(f5(x343))))+~P2(a2,f1(f5(f5(x342))))+~P2(a2,f1(f5(f5(x341))))+~P2(a2,f1(f5(f5(x343))))+~P2(a2,f1(f5(f5(f5(x342)))))+~P2(a2,f1(f5(f5(f5(x343)))))
% 61.33/61.83 [35]~P3(f5(x351),f5(x353))+~P3(f5(x353),f5(x352))+~P2(f1(x351),f1(f5(x351)))+~P2(a2,f1(x351))+~P2(f1(x352),f1(f5(x352)))+~P2(f1(x353),f1(f5(x353)))+~P2(a2,f1(x352))+~P2(a2,f1(x353))+~P2(a2,f1(f5(x351)))+~P2(a2,f1(f5(x353)))+~P2(a2,f1(f5(x352)))+P2(f1(x351),f1(f5(f5(x351))))+~P2(f1(x352),f1(f5(f5(x352))))+~P2(f1(x353),f1(f5(f5(x353))))+~P2(a2,f1(f5(f5(x352))))+~P2(a2,f1(f5(f5(x351))))+~P2(a2,f1(f5(f5(x353))))+~P2(a2,f1(f5(f5(f5(x352)))))+~P2(a2,f1(f5(f5(f5(x353)))))
% 61.33/61.83 [36]~P3(f5(x362),f5(x361))+~P3(f5(x363),f5(x362))+~P2(f1(x361),f1(f5(x361)))+~P2(a2,f1(x361))+~P2(f1(x362),f1(f5(x362)))+~P2(f1(x363),f1(f5(x363)))+~P2(a2,f1(x362))+~P2(a2,f1(x363))+~P2(a2,f1(f5(x363)))+~P2(a2,f1(f5(x362)))+~P2(a2,f1(f5(x361)))+~P2(f1(x361),f1(f5(f5(x361))))+~P2(f1(x362),f1(f5(f5(x362))))+~P2(f1(x363),f1(f5(f5(x363))))+~P2(a2,f1(f5(f5(x361))))+~P2(a2,f1(f5(f5(x362))))+~P2(a2,f1(f5(f5(x363))))+~P2(a2,f1(f5(f5(f5(x361)))))+~P2(a2,f1(f5(f5(f5(x362)))))+~P2(a2,f1(f5(f5(f5(x363)))))
% 61.33/61.83 %EqnAxiom
% 61.33/61.83
% 61.33/61.83 %-------------------------------------------
% 61.33/61.83 cnf(48,plain,
% 61.33/61.83 (P2(a2,f1(a4))),
% 61.33/61.83 inference(scs_inference,[],[1,2,3])).
% 61.33/61.83 cnf(49,plain,
% 61.33/61.83 (P1(f1(x491),f3(a2))),
% 61.33/61.83 inference(rename_variables,[],[1])).
% 61.33/61.83 cnf(51,plain,
% 61.33/61.83 (P2(a2,f1(f5(a4)))),
% 61.33/61.83 inference(scs_inference,[],[1,49,2,3,4])).
% 61.33/61.83 cnf(52,plain,
% 61.33/61.83 (P1(f1(x521),f3(a2))),
% 61.33/61.83 inference(rename_variables,[],[1])).
% 61.33/61.83 cnf(54,plain,
% 61.33/61.83 (P2(a2,f1(f5(f5(a4))))),
% 61.33/61.83 inference(scs_inference,[],[1,49,52,2,3,4,6])).
% 61.33/61.83 cnf(55,plain,
% 61.33/61.83 (P1(f1(x551),f3(a2))),
% 61.33/61.83 inference(rename_variables,[],[1])).
% 61.33/61.83 cnf(57,plain,
% 61.33/61.83 (P2(a2,f1(f5(f5(f5(a4)))))),
% 61.33/61.83 inference(scs_inference,[],[1,49,52,55,2,3,4,6,7])).
% 61.33/61.83 cnf(60,plain,
% 61.33/61.83 (~P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))),
% 61.33/61.83 inference(scs_inference,[],[1,49,52,55,2,3,4,6,7,9])).
% 61.33/61.83 cnf(68,plain,
% 61.33/61.83 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))),
% 61.33/61.83 inference(scs_inference,[],[48,51,57,54,10])).
% 61.33/61.83 cnf(73,plain,
% 61.33/61.83 (~P2(f1(a4),f1(f5(a4)))+P2(f1(a4),f1(f5(f5(a4))))),
% 61.33/61.83 inference(scs_inference,[],[48,51,54,8,20])).
% 61.33/61.83 cnf(79,plain,
% 61.33/61.83 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))),
% 61.33/61.83 inference(scs_inference,[],[73,68])).
% 61.33/61.83 cnf(85,plain,
% 61.33/61.83 (~P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))),
% 61.33/61.83 inference(scs_inference,[],[48,57,51,54,36])).
% 61.33/61.83 cnf(109,plain,
% 61.33/61.83 (~P2(f1(a4),f1(f5(f5(a4))))+~P3(f5(a4),f5(a4))),
% 61.33/61.83 inference(scs_inference,[],[48,51,85,9])).
% 61.33/61.83 cnf(264,plain,
% 61.33/61.83 (P2(f1(a4),f1(f5(a4)))),
% 61.33/61.83 inference(scs_inference,[],[48,51,60,5])).
% 61.33/61.83 cnf(265,plain,
% 61.33/61.83 (P2(f1(a4),f1(f5(f5(a4))))),
% 61.33/61.83 inference(scs_inference,[],[264,73])).
% 61.33/61.83 cnf(266,plain,
% 61.33/61.83 (P3(f5(a4),f5(a4))),
% 61.33/61.83 inference(scs_inference,[],[264,79])).
% 61.33/61.83 cnf(271,plain,
% 61.33/61.83 ($false),
% 61.33/61.83 inference(scs_inference,[],[266,265,109]),
% 61.33/61.83 ['proof']).
% 61.33/61.83 % SZS output end Proof
% 61.33/61.83 % Total time :60.680000s
%------------------------------------------------------------------------------