%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYO651-1 : TPTP v8.2.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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 : 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 64.59s 64.60s
% Output : CNFRefutation 64.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.15 % Problem : SYO651-1 : TPTP v8.2.0. Released v7.3.0.
% 0.04/0.15 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.16/0.37 % Computer : n027.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 300
% 0.16/0.37 % DateTime : Sun Jun 23 06:38:09 EDT 2024
% 0.16/0.37 % CPUTime :
% 0.65/0.68 start to proof:theBenchmark
% 64.59/64.56 %-------------------------------------------
% 64.59/64.56 % File :CSE---1.7
% 64.59/64.56 % Problem :theBenchmark
% 64.59/64.56 % Transform :cnf
% 64.59/64.56 % Format :tptp:raw
% 64.59/64.56 % Command :java -jar mcs_scs.jar %d %s
% 64.59/64.56
% 64.59/64.56 % Result :Theorem 63.750000s
% 64.59/64.56 % Output :CNFRefutation 63.750000s
% 64.59/64.56 %-------------------------------------------
% 64.59/64.57 %------------------------------------------------------------------------------
% 64.59/64.57 % File : SYO651-1 : TPTP v8.2.0. Released v7.3.0.
% 64.59/64.57 % Domain : Syntactic
% 64.59/64.57 % Problem : GSM_1_2_4
% 64.59/64.57 % Version : Especial.
% 64.59/64.57 % English :
% 64.59/64.57
% 64.59/64.57 % Refs : [EH+16] Ebner et al. (2016), System Description: GAPT 2.0
% 64.59/64.57 % : [Cer18] Cerna (2018), Email to Geoff Sutcliffe
% 64.59/64.57 % Source : [Cer18]
% 64.59/64.57 % Names : GSM_1_2_4 [Cer18]
% 64.59/64.57
% 64.59/64.57 % Status : Unsatisfiable
% 64.59/64.57 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.17 v7.3.0
% 64.59/64.57 % Syntax : Number of clauses : 75 ( 2 unt; 62 nHn; 74 RR)
% 64.59/64.57 % Number of literals : 1276 ( 0 equ;1114 neg)
% 64.59/64.57 % Maximal clause size : 26 ( 17 avg)
% 64.59/64.57 % Maximal term depth : 6 ( 2 avg)
% 64.59/64.57 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty)
% 64.59/64.57 % Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% 64.59/64.57 % Number of variables : 202 ( 1 sgn)
% 64.59/64.57 % SPC : CNF_UNS_RFO_NEQ_NHN
% 64.59/64.57
% 64.59/64.57 % Comments : Created using the GAPT system - https://github.com/gapt/gapt/blob/
% 64.59/64.57 % master/examples/schema/GradedStrictMonotoneSequenceSchema.scala
% 64.59/64.57 %------------------------------------------------------------------------------
% 64.59/64.57 cnf(clause_2802,axiom,
% 64.59/64.57 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.57 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.57 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.57 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.57 | ~ 'E'('0',f(A_1))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.57 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.57 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.57 | ~ 'E'('0',f(B_6))
% 64.59/64.57 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.57 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.57 | ~ 'E'('0',f(B_7))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.57 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.57 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.57 | 'E'(f(B_6),f(suc(suc(suc(B_6))))) ) ).
% 64.59/64.57
% 64.59/64.57 cnf(clause_2744,axiom,
% 64.59/64.57 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.57 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.57 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.57 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.57 | ~ 'E'('0',f(A_1))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.57 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.57 | ~ 'E'('0',f(B_6))
% 64.59/64.57 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.57 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.57 | ~ 'E'('0',f(B_7))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.57 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.57 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.57 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.57
% 64.59/64.57 cnf(clause_1772,axiom,
% 64.59/64.57 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.57 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.57 | ~ 'E'('0',f(A_1))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.57 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 64.59/64.57
% 64.59/64.57 cnf(clause_613,axiom,
% 64.59/64.57 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.57 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.57 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.57 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.57 | ~ 'E'('0',f(A_1))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.57 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.57 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.57 | ~ 'E'('0',f(B_6))
% 64.59/64.57 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.57 | ~ 'E'('0',f(B_7))
% 64.59/64.57 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.57 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.57 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.57
% 64.59/64.57 cnf(clause_1532,axiom,
% 64.59/64.57 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.57 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.57 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.57 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.57 | ~ 'E'('0',f(A_1))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.57 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.57 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.57 | ~ 'E'('0',f(B_6))
% 64.59/64.57 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.57 | ~ 'E'('0',f(B_7))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.57 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.57 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.57 | 'E'(f(B_6),f(suc(suc(B_6)))) ) ).
% 64.59/64.57
% 64.59/64.57 cnf(clause_3823,axiom,
% 64.59/64.57 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.57 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.57 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.57 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.57 | ~ 'E'('0',f(A_1))
% 64.59/64.57 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.57 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.57 | ~ 'E'('0',f(B_6))
% 64.59/64.57 | ~ 'E'('0',f(B_7))
% 64.59/64.57 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.57 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.57 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.57 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.57 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.57
% 64.59/64.57 cnf(clause_733,axiom,
% 64.59/64.57 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.58 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_1536,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.58 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.58 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_1318,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.58 | 'E'(f(B_6),f(suc(suc(suc(B_6))))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_3677,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | 'E'(f(B_6),f(suc(suc(suc(B_6))))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_2650,axiom,
% 64.59/64.58 ( ~ 'LE'(f(suc(B_5)),s('0'))
% 64.59/64.58 | 'E'('0',f(suc(B_5)))
% 64.59/64.58 | 'LE'(f(B_5),'0') ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_2891,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.58 | 'E'(f(B_6),f(suc(B_6))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_1098,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(A_1)))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_3530,axiom,
% 64.59/64.58 'LE'(f(A),s('0')) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_3578,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.58 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.58 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_187,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.58 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_492,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.58 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.58 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_2573,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_3275,axiom,
% 64.59/64.58 ( ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_3274,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.58 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.58 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_1875,axiom,
% 64.59/64.58 ( ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.58 | ~ 'E'('0',f(A_1))
% 64.59/64.58 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.58 | ~ 'E'('0',f(B_6))
% 64.59/64.58 | ~ 'E'('0',f(B_7))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.58 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.58 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.58 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.58
% 64.59/64.58 cnf(clause_627,axiom,
% 64.59/64.58 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.58 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.58 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.58 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.58 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.58 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.58 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_2277,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_3412,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_2612,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_2529,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_935,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_255,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_2887,axiom,
% 64.59/64.59 ( ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_1563,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_3718,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_3339,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_2312,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_426,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_3575,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(B_6)))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_3112,axiom,
% 64.59/64.59 ( ~ 'LE'(f(suc(suc(B_5))),s('0'))
% 64.59/64.59 | 'E'('0',f(suc(suc(B_5))))
% 64.59/64.59 | 'LE'(f(B_5),'0') ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_2518,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_1816,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_1829,axiom,
% 64.59/64.59 ~ 'LE'(f(z),'0') ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_1564,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_408,axiom,
% 64.59/64.59 ( ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(B_6))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_1901,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(suc(A_1))))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_3408,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_619,axiom,
% 64.59/64.59 ( ~ 'LE'(f(suc(suc(suc(suc(B_5))))),s('0'))
% 64.59/64.59 | 'E'('0',f(suc(suc(suc(suc(B_5))))))
% 64.59/64.59 | 'LE'(f(B_5),'0') ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_403,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.59 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_6))
% 64.59/64.59 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.59 | ~ 'E'('0',f(B_7))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.59 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.59 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.59 | 'E'(f(B_6),f(suc(suc(suc(B_6))))) ) ).
% 64.59/64.59
% 64.59/64.59 cnf(clause_3827,axiom,
% 64.59/64.59 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.59 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.59 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'('0',f(A_1))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.59 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.59 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.59 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_960,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(A_1))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_752,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_3337,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(B_6))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_55,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_1587,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_896,axiom,
% 64.59/64.60 ( ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_930,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_2899,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_3669,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_2721,axiom,
% 64.59/64.60 ( ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | 'E'(f(B_6),f(suc(B_6))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_2386,axiom,
% 64.59/64.60 ( ~ 'LE'(f(B_5),s('0'))
% 64.59/64.60 | 'E'('0',f(B_5))
% 64.59/64.60 | 'LE'(f(B_5),'0') ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_1550,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_3129,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_1229,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_3293,axiom,
% 64.59/64.60 ( ~ 'LE'(f(suc(suc(suc(B_5)))),s('0'))
% 64.59/64.60 | 'E'('0',f(suc(suc(suc(B_5)))))
% 64.59/64.60 | 'LE'(f(B_5),'0') ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_249,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_698,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_3360,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_1427,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | 'E'(f(B_7),f(suc(B_7))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_2015,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_2993,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_2195,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(suc(B_6)))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_1366,axiom,
% 64.59/64.60 ( ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_2665,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_1375,axiom,
% 64.59/64.60 ( ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_3155,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_2054,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(A_1))))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(suc(B_7))))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(B_7)))))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(suc(A_1))))
% 64.59/64.60 | 'E'(f(B_6),f(suc(suc(B_6)))) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_636,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 64.59/64.60
% 64.59/64.60 cnf(clause_3679,axiom,
% 64.59/64.60 ( ~ 'E'('0',f(suc(suc(B_6))))
% 64.59/64.60 | ~ iLEQ(suc(A_1),suc(B_6))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(suc(A_1)))
% 64.59/64.60 | ~ 'E'(f(B_7),f(suc(B_7)))
% 64.59/64.60 | ~ 'E'('0',f(A_1))
% 64.59/64.60 | ~ 'E'('0',f(suc(suc(B_7))))
% 64.59/64.60 | ~ iLEQ(suc(B_6),suc(B_7))
% 64.59/64.60 | ~ 'E'('0',f(B_6))
% 64.59/64.60 | ~ 'E'('0',f(B_7))
% 64.59/64.60 | ~ 'E'(f(B_6),f(suc(B_6)))
% 64.59/64.60 | ~ 'E'('0',f(suc(B_6)))
% 64.59/64.60 | 'E'(f(A_1),f(suc(A_1)))
% 64.59/64.60 | 'E'(f(B_6),f(suc(suc(B_6))))
% 64.59/64.60 | 'E'(f(B_7),f(suc(suc(B_7)))) ) ).
% 64.59/64.60
% 64.59/64.60 %------------------------------------------------------------------------------
% 64.59/64.60 %-------------------------------------------
% 64.59/64.60 % Proof found
% 64.59/64.60 % SZS status Theorem for theBenchmark
% 64.59/64.60 % SZS output start Proof
% 64.59/64.60 %ClaNum:75(EqnAxiom:0)
% 64.59/64.60 %VarNum:1848(SingletonVarNum:202)
% 64.59/64.60 %MaxLitNum:26
% 64.59/64.60 %MaxfuncDepth:5
% 64.59/64.60 %SharedTerms:5
% 64.59/64.60 [2]~P1(f1(a4),a2)
% 64.59/64.60 [1]P1(f1(x11),f3(a2))
% 64.59/64.60 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2)
% 64.59/64.60 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41)))
% 64.59/64.60 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61))))
% 64.59/64.60 [7]P1(f1(x71),a2)+~P1(f1(f5(f5(f5(x71)))),f3(a2))+P2(a2,f1(f5(f5(f5(x71)))))
% 64.59/64.60 [10]P1(f1(x101),a2)+~P1(f1(f5(f5(f5(f5(x101))))),f3(a2))+P2(a2,f1(f5(f5(f5(f5(x101))))))
% 64.59/64.60 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51)))
% 64.59/64.60 [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))))
% 64.59/64.60 [14]P3(f5(x141),f5(x141))+~P2(a2,f1(x141))+~P2(f1(x141),f1(f5(x141)))+~P2(f1(x141),f1(f5(f5(x141))))+~P2(a2,f1(f5(x141)))+P2(f1(x141),f1(f5(f5(f5(x141)))))+~P2(a2,f1(f5(f5(x141))))+~P2(a2,f1(f5(f5(f5(x141)))))
% 64.59/64.60 [22]P3(f5(x221),f5(x221))+~P2(a2,f1(x221))+~P2(f1(x221),f1(f5(x221)))+~P2(f1(x221),f1(f5(f5(x221))))+~P2(a2,f1(f5(x221)))+~P2(f1(x221),f1(f5(f5(f5(x221)))))+~P2(a2,f1(f5(f5(x221))))+~P2(a2,f1(f5(f5(f5(x221)))))+~P2(a2,f1(f5(f5(f5(f5(x221))))))
% 64.59/64.60 [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)))
% 64.59/64.60 [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))))
% 64.59/64.60 [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))))
% 64.59/64.60 [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))))
% 64.59/64.60 [15]~P3(f5(x152),f5(x153))+~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(x151)))+~P2(a2,f1(f5(x152)))+~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))))
% 64.59/64.60 [16]~P3(f5(x161),f5(x162))+~P3(f5(x163),f5(x161))+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))))
% 64.59/64.60 [17]~P3(f5(x171),f5(x173))+~P3(f5(x173),f5(x172))+P2(f1(x171),f1(f5(x171)))+~P2(a2,f1(x171))+~P2(f1(x172),f1(f5(x172)))+~P2(f1(x173),f1(f5(x173)))+~P2(a2,f1(x172))+~P2(a2,f1(x173))+~P2(a2,f1(f5(x172)))+~P2(a2,f1(f5(x171)))+~P2(a2,f1(f5(x173)))+P2(f1(x172),f1(f5(f5(x172))))+P2(f1(x173),f1(f5(f5(x173))))+~P2(a2,f1(f5(f5(x172))))+~P2(a2,f1(f5(f5(x173))))
% 64.59/64.60 [18]~P3(f5(x182),f5(x181))+~P3(f5(x183),f5(x182))+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(f1(x183),f1(f5(f5(f5(x183)))))+~P2(a2,f1(f5(f5(f5(x183)))))
% 64.59/64.60 [19]~P3(f5(x192),f5(x193))+~P3(f5(x193),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(x191)))+~P2(a2,f1(f5(x192)))+~P2(a2,f1(f5(x193)))+~P2(f1(x193),f1(f5(f5(x193))))+~P2(a2,f1(f5(f5(x193))))+P2(f1(x193),f1(f5(f5(f5(x193)))))+~P2(a2,f1(f5(f5(f5(x193)))))
% 64.59/64.60 [20]~P3(f5(x201),f5(x203))+~P3(f5(x202),f5(x201))+P2(f1(x201),f1(f5(x201)))+P2(f1(x202),f1(f5(x202)))+~P2(a2,f1(x201))+~P2(f1(x203),f1(f5(x203)))+~P2(a2,f1(x202))+~P2(a2,f1(x203))+~P2(a2,f1(f5(x203)))+~P2(a2,f1(f5(x201)))+~P2(a2,f1(f5(x202)))+~P2(f1(x203),f1(f5(f5(x203))))+~P2(a2,f1(f5(f5(x203))))+P2(f1(x203),f1(f5(f5(f5(x203)))))+~P2(a2,f1(f5(f5(f5(x203)))))
% 64.59/64.60 [32]~P3(f5(x322),f5(x321))+~P3(f5(x323),f5(x322))+P2(f1(x321),f1(f5(x321)))+P2(f1(x322),f1(f5(x322)))+~P2(a2,f1(x321))+~P2(f1(x323),f1(f5(x323)))+~P2(a2,f1(x322))+~P2(a2,f1(x323))+~P2(a2,f1(f5(x321)))+~P2(a2,f1(f5(x322)))+~P2(a2,f1(f5(x323)))+~P2(f1(x323),f1(f5(f5(x323))))+~P2(a2,f1(f5(f5(x323))))+~P2(f1(x323),f1(f5(f5(f5(x323)))))+~P2(a2,f1(f5(f5(f5(x323)))))+~P2(a2,f1(f5(f5(f5(f5(x323))))))
% 64.59/64.60 [33]~P3(f5(x332),f5(x333))+~P3(f5(x333),f5(x331))+P2(f1(x331),f1(f5(x331)))+P2(f1(x332),f1(f5(x332)))+~P2(a2,f1(x331))+~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(x333),f1(f5(f5(x333))))+~P2(a2,f1(f5(f5(x333))))+~P2(f1(x333),f1(f5(f5(f5(x333)))))+~P2(a2,f1(f5(f5(f5(x333)))))+~P2(a2,f1(f5(f5(f5(f5(x333))))))
% 64.59/64.60 [34]~P3(f5(x341),f5(x343))+~P3(f5(x342),f5(x341))+P2(f1(x341),f1(f5(x341)))+P2(f1(x342),f1(f5(x342)))+~P2(a2,f1(x341))+~P2(f1(x343),f1(f5(x343)))+~P2(a2,f1(x342))+~P2(a2,f1(x343))+~P2(a2,f1(f5(x343)))+~P2(a2,f1(f5(x341)))+~P2(a2,f1(f5(x342)))+~P2(f1(x343),f1(f5(f5(x343))))+~P2(a2,f1(f5(f5(x343))))+~P2(f1(x343),f1(f5(f5(f5(x343)))))+~P2(a2,f1(f5(f5(f5(x343)))))+~P2(a2,f1(f5(f5(f5(f5(x343))))))
% 64.59/64.60 [21]~P3(f5(x212),f5(x213))+~P3(f5(x213),f5(x211))+~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(x211),f1(f5(f5(x211))))+P2(f1(x212),f1(f5(f5(x212))))+P2(f1(x213),f1(f5(f5(x213))))+~P2(a2,f1(f5(f5(x211))))+~P2(a2,f1(f5(f5(x212))))+~P2(a2,f1(f5(f5(x213))))
% 64.59/64.60 [23]~P3(f5(x232),f5(x231))+~P3(f5(x233),f5(x232))+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(x231)))+~P2(a2,f1(f5(x232)))+~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(f1(x233),f1(f5(f5(f5(x233)))))+~P2(a2,f1(f5(f5(f5(x233)))))
% 64.59/64.60 [24]~P3(f5(x242),f5(x243))+~P3(f5(x243),f5(x241))+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(x241)))+~P2(a2,f1(f5(x242)))+~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(f1(x243),f1(f5(f5(f5(x243)))))+~P2(a2,f1(f5(f5(f5(x243)))))
% 64.59/64.60 [25]~P3(f5(x251),f5(x252))+~P3(f5(x253),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(x252)))+~P2(a2,f1(f5(x251)))+~P2(a2,f1(f5(x253)))+P2(f1(x252),f1(f5(f5(x252))))+~P2(f1(x253),f1(f5(f5(x253))))+~P2(a2,f1(f5(f5(x252))))+~P2(a2,f1(f5(f5(x253))))+P2(f1(x253),f1(f5(f5(f5(x253)))))+~P2(a2,f1(f5(f5(f5(x253)))))
% 64.59/64.60 [26]~P3(f5(x261),f5(x263))+~P3(f5(x263),f5(x262))+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(x262)))+~P2(a2,f1(f5(x261)))+~P2(a2,f1(f5(x263)))+P2(f1(x262),f1(f5(f5(x262))))+~P2(f1(x263),f1(f5(f5(x263))))+~P2(a2,f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(x263))))+P2(f1(x263),f1(f5(f5(f5(x263)))))+~P2(a2,f1(f5(f5(f5(x263)))))
% 64.59/64.60 [27]~P3(f5(x271),f5(x273))+~P3(f5(x272),f5(x271))+P2(f1(x271),f1(f5(x271)))+~P2(f1(x272),f1(f5(x272)))+~P2(a2,f1(x271))+~P2(f1(x273),f1(f5(x273)))+~P2(a2,f1(x272))+~P2(a2,f1(x273))+~P2(a2,f1(f5(x273)))+~P2(a2,f1(f5(x271)))+~P2(a2,f1(f5(x272)))+P2(f1(x272),f1(f5(f5(x272))))+~P2(f1(x273),f1(f5(f5(x273))))+~P2(a2,f1(f5(f5(x273))))+~P2(a2,f1(f5(f5(x272))))+P2(f1(x273),f1(f5(f5(f5(x273)))))+~P2(a2,f1(f5(f5(f5(x273)))))
% 64.59/64.60 [28]~P3(f5(x281),f5(x282))+~P3(f5(x282),f5(x283))+P2(f1(x281),f1(f5(x281)))+~P2(f1(x282),f1(f5(x282)))+~P2(a2,f1(x281))+~P2(f1(x283),f1(f5(x283)))+~P2(a2,f1(x282))+~P2(a2,f1(x283))+~P2(a2,f1(f5(x283)))+~P2(a2,f1(f5(x281)))+~P2(a2,f1(f5(x282)))+P2(f1(x282),f1(f5(f5(x282))))+~P2(f1(x283),f1(f5(f5(x283))))+~P2(a2,f1(f5(f5(x283))))+~P2(a2,f1(f5(f5(x282))))+P2(f1(x283),f1(f5(f5(f5(x283)))))+~P2(a2,f1(f5(f5(f5(x283)))))
% 64.59/64.60 [38]~P3(f5(x382),f5(x381))+~P3(f5(x383),f5(x382))+P2(f1(x381),f1(f5(x381)))+~P2(a2,f1(x381))+~P2(f1(x382),f1(f5(x382)))+~P2(f1(x383),f1(f5(x383)))+~P2(a2,f1(x382))+~P2(a2,f1(x383))+~P2(a2,f1(f5(x381)))+~P2(a2,f1(f5(x382)))+~P2(a2,f1(f5(x383)))+P2(f1(x382),f1(f5(f5(x382))))+~P2(f1(x383),f1(f5(f5(x383))))+~P2(a2,f1(f5(f5(x382))))+~P2(a2,f1(f5(f5(x383))))+~P2(f1(x383),f1(f5(f5(f5(x383)))))+~P2(a2,f1(f5(f5(f5(x383)))))+~P2(a2,f1(f5(f5(f5(f5(x383))))))
% 64.59/64.60 [39]~P3(f5(x392),f5(x393))+~P3(f5(x393),f5(x391))+P2(f1(x391),f1(f5(x391)))+~P2(a2,f1(x391))+~P2(f1(x392),f1(f5(x392)))+~P2(f1(x393),f1(f5(x393)))+~P2(a2,f1(x392))+~P2(a2,f1(x393))+~P2(a2,f1(f5(x391)))+~P2(a2,f1(f5(x392)))+~P2(a2,f1(f5(x393)))+P2(f1(x392),f1(f5(f5(x392))))+~P2(f1(x393),f1(f5(f5(x393))))+~P2(a2,f1(f5(f5(x392))))+~P2(a2,f1(f5(f5(x393))))+~P2(f1(x393),f1(f5(f5(f5(x393)))))+~P2(a2,f1(f5(f5(f5(x393)))))+~P2(a2,f1(f5(f5(f5(f5(x393))))))
% 64.59/64.60 [40]~P3(f5(x401),f5(x402))+~P3(f5(x403),f5(x401))+P2(f1(x401),f1(f5(x401)))+~P2(a2,f1(x401))+~P2(f1(x402),f1(f5(x402)))+~P2(f1(x403),f1(f5(x403)))+~P2(a2,f1(x402))+~P2(a2,f1(x403))+~P2(a2,f1(f5(x402)))+~P2(a2,f1(f5(x401)))+~P2(a2,f1(f5(x403)))+P2(f1(x402),f1(f5(f5(x402))))+~P2(f1(x403),f1(f5(f5(x403))))+~P2(a2,f1(f5(f5(x402))))+~P2(a2,f1(f5(f5(x403))))+~P2(f1(x403),f1(f5(f5(f5(x403)))))+~P2(a2,f1(f5(f5(f5(x403)))))+~P2(a2,f1(f5(f5(f5(f5(x403))))))
% 64.59/64.60 [41]~P3(f5(x411),f5(x413))+~P3(f5(x413),f5(x412))+P2(f1(x411),f1(f5(x411)))+~P2(a2,f1(x411))+~P2(f1(x412),f1(f5(x412)))+~P2(f1(x413),f1(f5(x413)))+~P2(a2,f1(x412))+~P2(a2,f1(x413))+~P2(a2,f1(f5(x412)))+~P2(a2,f1(f5(x411)))+~P2(a2,f1(f5(x413)))+P2(f1(x412),f1(f5(f5(x412))))+~P2(f1(x413),f1(f5(f5(x413))))+~P2(a2,f1(f5(f5(x412))))+~P2(a2,f1(f5(f5(x413))))+~P2(f1(x413),f1(f5(f5(f5(x413)))))+~P2(a2,f1(f5(f5(f5(x413)))))+~P2(a2,f1(f5(f5(f5(f5(x413))))))
% 64.59/64.60 [42]~P3(f5(x421),f5(x423))+~P3(f5(x422),f5(x421))+P2(f1(x421),f1(f5(x421)))+~P2(a2,f1(x421))+~P2(f1(x422),f1(f5(x422)))+~P2(f1(x423),f1(f5(x423)))+~P2(a2,f1(x422))+~P2(a2,f1(x423))+~P2(a2,f1(f5(x423)))+~P2(a2,f1(f5(x421)))+~P2(a2,f1(f5(x422)))+P2(f1(x422),f1(f5(f5(x422))))+~P2(f1(x423),f1(f5(f5(x423))))+~P2(a2,f1(f5(f5(x423))))+~P2(a2,f1(f5(f5(x422))))+~P2(f1(x423),f1(f5(f5(f5(x423)))))+~P2(a2,f1(f5(f5(f5(x423)))))+~P2(a2,f1(f5(f5(f5(f5(x423))))))
% 64.59/64.60 [43]~P3(f5(x431),f5(x432))+~P3(f5(x432),f5(x433))+P2(f1(x431),f1(f5(x431)))+~P2(a2,f1(x431))+~P2(f1(x432),f1(f5(x432)))+~P2(f1(x433),f1(f5(x433)))+~P2(a2,f1(x432))+~P2(a2,f1(x433))+~P2(a2,f1(f5(x433)))+~P2(a2,f1(f5(x431)))+~P2(a2,f1(f5(x432)))+P2(f1(x432),f1(f5(f5(x432))))+~P2(f1(x433),f1(f5(f5(x433))))+~P2(a2,f1(f5(f5(x433))))+~P2(a2,f1(f5(f5(x432))))+~P2(f1(x433),f1(f5(f5(f5(x433)))))+~P2(a2,f1(f5(f5(f5(x433)))))+~P2(a2,f1(f5(f5(f5(f5(x433))))))
% 64.59/64.60 [29]~P3(f5(x292),f5(x291))+~P3(f5(x293),f5(x292))+~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(x291)))+~P2(a2,f1(f5(x292)))+~P2(a2,f1(f5(x293)))+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(x291))))+~P2(a2,f1(f5(f5(x292))))+~P2(a2,f1(f5(f5(x293))))+P2(f1(x293),f1(f5(f5(f5(x293)))))+~P2(a2,f1(f5(f5(f5(x293)))))
% 64.59/64.60 [30]~P3(f5(x302),f5(x303))+~P3(f5(x303),f5(x301))+~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(x301)))+~P2(a2,f1(f5(x302)))+~P2(a2,f1(f5(x303)))+P2(f1(x301),f1(f5(f5(x301))))+P2(f1(x302),f1(f5(f5(x302))))+~P2(f1(x303),f1(f5(f5(x303))))+~P2(a2,f1(f5(f5(x301))))+~P2(a2,f1(f5(f5(x302))))+~P2(a2,f1(f5(f5(x303))))+P2(f1(x303),f1(f5(f5(f5(x303)))))+~P2(a2,f1(f5(f5(f5(x303)))))
% 64.59/64.60 [31]~P3(f5(x311),f5(x312))+~P3(f5(x312),f5(x313))+~P2(f1(x311),f1(f5(x311)))+~P2(f1(x312),f1(f5(x312)))+~P2(a2,f1(x311))+~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(x311),f1(f5(f5(x311))))+P2(f1(x312),f1(f5(f5(x312))))+~P2(f1(x313),f1(f5(f5(x313))))+~P2(a2,f1(f5(f5(x313))))+~P2(a2,f1(f5(f5(x311))))+~P2(a2,f1(f5(f5(x312))))+P2(f1(x313),f1(f5(f5(f5(x313)))))+~P2(a2,f1(f5(f5(f5(x313)))))
% 64.59/64.60 [35]~P3(f5(x352),f5(x351))+~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(x352)))+~P2(a2,f1(f5(x353)))+~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(x353))))+P2(f1(x352),f1(f5(f5(f5(x352)))))+P2(f1(x353),f1(f5(f5(f5(x353)))))+~P2(a2,f1(f5(f5(f5(x352)))))+~P2(a2,f1(f5(f5(f5(x353)))))
% 64.59/64.60 [36]~P3(f5(x361),f5(x362))+~P3(f5(x363),f5(x361))+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(x362)))+~P2(a2,f1(f5(x361)))+~P2(a2,f1(f5(x363)))+~P2(f1(x362),f1(f5(f5(x362))))+~P2(f1(x363),f1(f5(f5(x363))))+~P2(a2,f1(f5(f5(x362))))+~P2(a2,f1(f5(f5(x363))))+P2(f1(x362),f1(f5(f5(f5(x362)))))+P2(f1(x363),f1(f5(f5(f5(x363)))))+~P2(a2,f1(f5(f5(f5(x362)))))+~P2(a2,f1(f5(f5(f5(x363)))))
% 64.59/64.60 [37]~P3(f5(x371),f5(x373))+~P3(f5(x373),f5(x372))+P2(f1(x371),f1(f5(x371)))+~P2(a2,f1(x371))+~P2(f1(x372),f1(f5(x372)))+~P2(f1(x373),f1(f5(x373)))+~P2(a2,f1(x372))+~P2(a2,f1(x373))+~P2(a2,f1(f5(x372)))+~P2(a2,f1(f5(x371)))+~P2(a2,f1(f5(x373)))+~P2(f1(x372),f1(f5(f5(x372))))+~P2(f1(x373),f1(f5(f5(x373))))+~P2(a2,f1(f5(f5(x372))))+~P2(a2,f1(f5(f5(x373))))+P2(f1(x372),f1(f5(f5(f5(x372)))))+P2(f1(x373),f1(f5(f5(f5(x373)))))+~P2(a2,f1(f5(f5(f5(x372)))))+~P2(a2,f1(f5(f5(f5(x373)))))
% 64.59/64.60 [47]~P3(f5(x472),f5(x471))+~P3(f5(x473),f5(x472))+~P2(f1(x471),f1(f5(x471)))+~P2(a2,f1(x471))+~P2(f1(x472),f1(f5(x472)))+~P2(f1(x473),f1(f5(x473)))+~P2(a2,f1(x472))+~P2(a2,f1(x473))+~P2(a2,f1(f5(x471)))+~P2(a2,f1(f5(x472)))+~P2(a2,f1(f5(x473)))+P2(f1(x471),f1(f5(f5(x471))))+P2(f1(x472),f1(f5(f5(x472))))+~P2(f1(x473),f1(f5(f5(x473))))+~P2(a2,f1(f5(f5(x471))))+~P2(a2,f1(f5(f5(x472))))+~P2(a2,f1(f5(f5(x473))))+~P2(f1(x473),f1(f5(f5(f5(x473)))))+~P2(a2,f1(f5(f5(f5(x473)))))+~P2(a2,f1(f5(f5(f5(f5(x473))))))
% 64.59/64.60 [48]~P3(f5(x482),f5(x483))+~P3(f5(x483),f5(x481))+~P2(f1(x481),f1(f5(x481)))+~P2(a2,f1(x481))+~P2(f1(x482),f1(f5(x482)))+~P2(f1(x483),f1(f5(x483)))+~P2(a2,f1(x482))+~P2(a2,f1(x483))+~P2(a2,f1(f5(x481)))+~P2(a2,f1(f5(x482)))+~P2(a2,f1(f5(x483)))+P2(f1(x481),f1(f5(f5(x481))))+P2(f1(x482),f1(f5(f5(x482))))+~P2(f1(x483),f1(f5(f5(x483))))+~P2(a2,f1(f5(f5(x481))))+~P2(a2,f1(f5(f5(x482))))+~P2(a2,f1(f5(f5(x483))))+~P2(f1(x483),f1(f5(f5(f5(x483)))))+~P2(a2,f1(f5(f5(f5(x483)))))+~P2(a2,f1(f5(f5(f5(f5(x483))))))
% 64.59/64.60 [49]~P3(f5(x491),f5(x492))+~P3(f5(x492),f5(x493))+~P2(f1(x491),f1(f5(x491)))+~P2(a2,f1(x491))+~P2(f1(x492),f1(f5(x492)))+~P2(f1(x493),f1(f5(x493)))+~P2(a2,f1(x492))+~P2(a2,f1(x493))+~P2(a2,f1(f5(x493)))+~P2(a2,f1(f5(x491)))+~P2(a2,f1(f5(x492)))+P2(f1(x491),f1(f5(f5(x491))))+P2(f1(x492),f1(f5(f5(x492))))+~P2(f1(x493),f1(f5(f5(x493))))+~P2(a2,f1(f5(f5(x493))))+~P2(a2,f1(f5(f5(x491))))+~P2(a2,f1(f5(f5(x492))))+~P2(f1(x493),f1(f5(f5(f5(x493)))))+~P2(a2,f1(f5(f5(f5(x493)))))+~P2(a2,f1(f5(f5(f5(f5(x493))))))
% 64.59/64.60 [50]~P3(f5(x502),f5(x501))+~P3(f5(x503),f5(x502))+P2(f1(x501),f1(f5(x501)))+~P2(a2,f1(x501))+~P2(f1(x502),f1(f5(x502)))+~P2(f1(x503),f1(f5(x503)))+~P2(a2,f1(x502))+~P2(a2,f1(x503))+~P2(a2,f1(f5(x501)))+~P2(a2,f1(f5(x502)))+~P2(a2,f1(f5(x503)))+~P2(f1(x502),f1(f5(f5(x502))))+~P2(f1(x503),f1(f5(f5(x503))))+~P2(a2,f1(f5(f5(x502))))+~P2(a2,f1(f5(f5(x503))))+P2(f1(x502),f1(f5(f5(f5(x502)))))+~P2(f1(x503),f1(f5(f5(f5(x503)))))+~P2(a2,f1(f5(f5(f5(x502)))))+~P2(a2,f1(f5(f5(f5(x503)))))+~P2(a2,f1(f5(f5(f5(f5(x503))))))
% 64.59/64.60 [51]~P3(f5(x513),f5(x511))+~P3(f5(x512),f5(x513))+P2(f1(x511),f1(f5(x511)))+~P2(a2,f1(x511))+~P2(f1(x512),f1(f5(x512)))+~P2(f1(x513),f1(f5(x513)))+~P2(a2,f1(x512))+~P2(a2,f1(x513))+~P2(a2,f1(f5(x511)))+~P2(a2,f1(f5(x513)))+~P2(a2,f1(f5(x512)))+~P2(f1(x512),f1(f5(f5(x512))))+~P2(f1(x513),f1(f5(f5(x513))))+~P2(a2,f1(f5(f5(x513))))+~P2(a2,f1(f5(f5(x512))))+P2(f1(x512),f1(f5(f5(f5(x512)))))+~P2(f1(x513),f1(f5(f5(f5(x513)))))+~P2(a2,f1(f5(f5(f5(x513)))))+~P2(a2,f1(f5(f5(f5(x512)))))+~P2(a2,f1(f5(f5(f5(f5(x513))))))
% 64.59/64.60 [52]~P3(f5(x521),f5(x522))+~P3(f5(x523),f5(x521))+P2(f1(x521),f1(f5(x521)))+~P2(a2,f1(x521))+~P2(f1(x522),f1(f5(x522)))+~P2(f1(x523),f1(f5(x523)))+~P2(a2,f1(x522))+~P2(a2,f1(x523))+~P2(a2,f1(f5(x522)))+~P2(a2,f1(f5(x521)))+~P2(a2,f1(f5(x523)))+~P2(f1(x522),f1(f5(f5(x522))))+~P2(f1(x523),f1(f5(f5(x523))))+~P2(a2,f1(f5(f5(x522))))+~P2(a2,f1(f5(f5(x523))))+P2(f1(x522),f1(f5(f5(f5(x522)))))+~P2(f1(x523),f1(f5(f5(f5(x523)))))+~P2(a2,f1(f5(f5(f5(x522)))))+~P2(a2,f1(f5(f5(f5(x523)))))+~P2(a2,f1(f5(f5(f5(f5(x523))))))
% 64.59/64.60 [53]~P3(f5(x531),f5(x533))+~P3(f5(x533),f5(x532))+P2(f1(x531),f1(f5(x531)))+~P2(a2,f1(x531))+~P2(f1(x532),f1(f5(x532)))+~P2(f1(x533),f1(f5(x533)))+~P2(a2,f1(x532))+~P2(a2,f1(x533))+~P2(a2,f1(f5(x532)))+~P2(a2,f1(f5(x531)))+~P2(a2,f1(f5(x533)))+~P2(f1(x532),f1(f5(f5(x532))))+~P2(f1(x533),f1(f5(f5(x533))))+~P2(a2,f1(f5(f5(x532))))+~P2(a2,f1(f5(f5(x533))))+P2(f1(x532),f1(f5(f5(f5(x532)))))+~P2(f1(x533),f1(f5(f5(f5(x533)))))+~P2(a2,f1(f5(f5(f5(x532)))))+~P2(a2,f1(f5(f5(f5(x533)))))+~P2(a2,f1(f5(f5(f5(f5(x533))))))
% 64.59/64.60 [54]~P3(f5(x541),f5(x543))+~P3(f5(x542),f5(x541))+P2(f1(x541),f1(f5(x541)))+~P2(a2,f1(x541))+~P2(f1(x542),f1(f5(x542)))+~P2(f1(x543),f1(f5(x543)))+~P2(a2,f1(x542))+~P2(a2,f1(x543))+~P2(a2,f1(f5(x543)))+~P2(a2,f1(f5(x541)))+~P2(a2,f1(f5(x542)))+~P2(f1(x542),f1(f5(f5(x542))))+~P2(f1(x543),f1(f5(f5(x543))))+~P2(a2,f1(f5(f5(x543))))+~P2(a2,f1(f5(f5(x542))))+P2(f1(x542),f1(f5(f5(f5(x542)))))+~P2(f1(x543),f1(f5(f5(f5(x543)))))+~P2(a2,f1(f5(f5(f5(x543)))))+~P2(a2,f1(f5(f5(f5(x542)))))+~P2(a2,f1(f5(f5(f5(f5(x543))))))
% 64.59/64.60 [55]~P3(f5(x551),f5(x552))+~P3(f5(x552),f5(x553))+P2(f1(x551),f1(f5(x551)))+~P2(a2,f1(x551))+~P2(f1(x552),f1(f5(x552)))+~P2(f1(x553),f1(f5(x553)))+~P2(a2,f1(x552))+~P2(a2,f1(x553))+~P2(a2,f1(f5(x553)))+~P2(a2,f1(f5(x551)))+~P2(a2,f1(f5(x552)))+~P2(f1(x552),f1(f5(f5(x552))))+~P2(f1(x553),f1(f5(f5(x553))))+~P2(a2,f1(f5(f5(x553))))+~P2(a2,f1(f5(f5(x552))))+P2(f1(x552),f1(f5(f5(f5(x552)))))+~P2(f1(x553),f1(f5(f5(f5(x553)))))+~P2(a2,f1(f5(f5(f5(x553)))))+~P2(a2,f1(f5(f5(f5(x552)))))+~P2(a2,f1(f5(f5(f5(f5(x553))))))
% 64.59/64.60 [44]~P3(f5(x442),f5(x441))+~P3(f5(x443),f5(x442))+~P2(f1(x441),f1(f5(x441)))+~P2(f1(x442),f1(f5(x442)))+~P2(a2,f1(x441))+~P2(f1(x443),f1(f5(x443)))+~P2(a2,f1(x442))+~P2(a2,f1(x443))+~P2(a2,f1(f5(x441)))+~P2(a2,f1(f5(x442)))+~P2(a2,f1(f5(x443)))+P2(f1(x441),f1(f5(f5(x441))))+~P2(f1(x442),f1(f5(f5(x442))))+~P2(f1(x443),f1(f5(f5(x443))))+~P2(a2,f1(f5(f5(x441))))+~P2(a2,f1(f5(f5(x442))))+~P2(a2,f1(f5(f5(x443))))+P2(f1(x442),f1(f5(f5(f5(x442)))))+P2(f1(x443),f1(f5(f5(f5(x443)))))+~P2(a2,f1(f5(f5(f5(x442)))))+~P2(a2,f1(f5(f5(f5(x443)))))
% 64.59/64.60 [45]~P3(f5(x451),f5(x452))+~P3(f5(x453),f5(x451))+~P2(f1(x451),f1(f5(x451)))+~P2(a2,f1(x451))+~P2(f1(x452),f1(f5(x452)))+~P2(f1(x453),f1(f5(x453)))+~P2(a2,f1(x452))+~P2(a2,f1(x453))+~P2(a2,f1(f5(x452)))+~P2(a2,f1(f5(x451)))+~P2(a2,f1(f5(x453)))+P2(f1(x451),f1(f5(f5(x451))))+~P2(f1(x452),f1(f5(f5(x452))))+~P2(f1(x453),f1(f5(f5(x453))))+~P2(a2,f1(f5(f5(x452))))+~P2(a2,f1(f5(f5(x451))))+~P2(a2,f1(f5(f5(x453))))+P2(f1(x452),f1(f5(f5(f5(x452)))))+P2(f1(x453),f1(f5(f5(f5(x453)))))+~P2(a2,f1(f5(f5(f5(x452)))))+~P2(a2,f1(f5(f5(f5(x453)))))
% 64.59/64.60 [46]~P3(f5(x461),f5(x463))+~P3(f5(x463),f5(x462))+~P2(f1(x461),f1(f5(x461)))+~P2(a2,f1(x461))+~P2(f1(x462),f1(f5(x462)))+~P2(f1(x463),f1(f5(x463)))+~P2(a2,f1(x462))+~P2(a2,f1(x463))+~P2(a2,f1(f5(x462)))+~P2(a2,f1(f5(x461)))+~P2(a2,f1(f5(x463)))+P2(f1(x461),f1(f5(f5(x461))))+~P2(f1(x462),f1(f5(f5(x462))))+~P2(f1(x463),f1(f5(f5(x463))))+~P2(a2,f1(f5(f5(x462))))+~P2(a2,f1(f5(f5(x461))))+~P2(a2,f1(f5(f5(x463))))+P2(f1(x462),f1(f5(f5(f5(x462)))))+P2(f1(x463),f1(f5(f5(f5(x463)))))+~P2(a2,f1(f5(f5(f5(x462)))))+~P2(a2,f1(f5(f5(f5(x463)))))
% 64.59/64.60 [63]~P3(f5(x632),f5(x631))+~P3(f5(x633),f5(x632))+P2(f1(x631),f1(f5(x631)))+~P2(a2,f1(x631))+~P2(f1(x632),f1(f5(x632)))+~P2(f1(x633),f1(f5(x633)))+~P2(a2,f1(x632))+~P2(a2,f1(x633))+~P2(a2,f1(f5(x631)))+~P2(a2,f1(f5(x632)))+~P2(a2,f1(f5(x633)))+~P2(f1(x632),f1(f5(f5(x632))))+~P2(f1(x633),f1(f5(f5(x633))))+~P2(a2,f1(f5(f5(x632))))+~P2(a2,f1(f5(f5(x633))))+~P2(f1(x632),f1(f5(f5(f5(x632)))))+~P2(f1(x633),f1(f5(f5(f5(x633)))))+~P2(a2,f1(f5(f5(f5(x632)))))+~P2(a2,f1(f5(f5(f5(x633)))))+~P2(a2,f1(f5(f5(f5(f5(x632))))))+~P2(a2,f1(f5(f5(f5(f5(x633))))))
% 64.59/64.60 [64]~P3(f5(x641),f5(x642))+~P3(f5(x643),f5(x641))+P2(f1(x641),f1(f5(x641)))+~P2(a2,f1(x641))+~P2(f1(x642),f1(f5(x642)))+~P2(f1(x643),f1(f5(x643)))+~P2(a2,f1(x642))+~P2(a2,f1(x643))+~P2(a2,f1(f5(x641)))+~P2(a2,f1(f5(x643)))+~P2(a2,f1(f5(x642)))+~P2(f1(x642),f1(f5(f5(x642))))+~P2(f1(x643),f1(f5(f5(x643))))+~P2(a2,f1(f5(f5(x642))))+~P2(a2,f1(f5(f5(x643))))+~P2(f1(x642),f1(f5(f5(f5(x642)))))+~P2(f1(x643),f1(f5(f5(f5(x643)))))+~P2(a2,f1(f5(f5(f5(x642)))))+~P2(a2,f1(f5(f5(f5(x643)))))+~P2(a2,f1(f5(f5(f5(f5(x642))))))+~P2(a2,f1(f5(f5(f5(f5(x643))))))
% 64.59/64.60 [65]~P3(f5(x651),f5(x653))+~P3(f5(x653),f5(x652))+P2(f1(x651),f1(f5(x651)))+~P2(a2,f1(x651))+~P2(f1(x652),f1(f5(x652)))+~P2(f1(x653),f1(f5(x653)))+~P2(a2,f1(x652))+~P2(a2,f1(x653))+~P2(a2,f1(f5(x651)))+~P2(a2,f1(f5(x653)))+~P2(a2,f1(f5(x652)))+~P2(f1(x652),f1(f5(f5(x652))))+~P2(f1(x653),f1(f5(f5(x653))))+~P2(a2,f1(f5(f5(x652))))+~P2(a2,f1(f5(f5(x653))))+~P2(f1(x652),f1(f5(f5(f5(x652)))))+~P2(f1(x653),f1(f5(f5(f5(x653)))))+~P2(a2,f1(f5(f5(f5(x652)))))+~P2(a2,f1(f5(f5(f5(x653)))))+~P2(a2,f1(f5(f5(f5(f5(x652))))))+~P2(a2,f1(f5(f5(f5(f5(x653))))))
% 64.59/64.60 [57]~P3(f5(x572),f5(x571))+~P3(f5(x573),f5(x572))+~P2(f1(x571),f1(f5(x571)))+~P2(a2,f1(x571))+~P2(f1(x572),f1(f5(x572)))+~P2(f1(x573),f1(f5(x573)))+~P2(a2,f1(x572))+~P2(a2,f1(x573))+~P2(a2,f1(f5(x571)))+~P2(a2,f1(f5(x572)))+~P2(a2,f1(f5(x573)))+P2(f1(x571),f1(f5(f5(x571))))+~P2(f1(x572),f1(f5(f5(x572))))+~P2(f1(x573),f1(f5(f5(x573))))+~P2(a2,f1(f5(f5(x571))))+~P2(a2,f1(f5(f5(x572))))+~P2(a2,f1(f5(f5(x573))))+P2(f1(x572),f1(f5(f5(f5(x572)))))+~P2(f1(x573),f1(f5(f5(f5(x573)))))+~P2(a2,f1(f5(f5(f5(x572)))))+~P2(a2,f1(f5(f5(f5(x573)))))+~P2(a2,f1(f5(f5(f5(f5(x573))))))
% 64.59/64.60 [58]~P3(f5(x583),f5(x581))+~P3(f5(x582),f5(x583))+~P2(f1(x581),f1(f5(x581)))+~P2(f1(x582),f1(f5(x582)))+~P2(a2,f1(x581))+~P2(f1(x583),f1(f5(x583)))+~P2(a2,f1(x582))+~P2(a2,f1(x583))+~P2(a2,f1(f5(x581)))+~P2(a2,f1(f5(x583)))+~P2(a2,f1(f5(x582)))+P2(f1(x581),f1(f5(f5(x581))))+~P2(f1(x582),f1(f5(f5(x582))))+~P2(f1(x583),f1(f5(f5(x583))))+~P2(a2,f1(f5(f5(x581))))+~P2(a2,f1(f5(f5(x583))))+~P2(a2,f1(f5(f5(x582))))+P2(f1(x582),f1(f5(f5(f5(x582)))))+~P2(f1(x583),f1(f5(f5(f5(x583)))))+~P2(a2,f1(f5(f5(f5(x583)))))+~P2(a2,f1(f5(f5(f5(x582)))))+~P2(a2,f1(f5(f5(f5(f5(x583))))))
% 64.59/64.60 [59]~P3(f5(x591),f5(x592))+~P3(f5(x593),f5(x591))+~P2(f1(x591),f1(f5(x591)))+~P2(a2,f1(x591))+~P2(f1(x592),f1(f5(x592)))+~P2(f1(x593),f1(f5(x593)))+~P2(a2,f1(x592))+~P2(a2,f1(x593))+~P2(a2,f1(f5(x592)))+~P2(a2,f1(f5(x591)))+~P2(a2,f1(f5(x593)))+P2(f1(x591),f1(f5(f5(x591))))+~P2(f1(x592),f1(f5(f5(x592))))+~P2(f1(x593),f1(f5(f5(x593))))+~P2(a2,f1(f5(f5(x592))))+~P2(a2,f1(f5(f5(x591))))+~P2(a2,f1(f5(f5(x593))))+P2(f1(x592),f1(f5(f5(f5(x592)))))+~P2(f1(x593),f1(f5(f5(f5(x593)))))+~P2(a2,f1(f5(f5(f5(x592)))))+~P2(a2,f1(f5(f5(f5(x593)))))+~P2(a2,f1(f5(f5(f5(f5(x593))))))
% 64.59/64.60 [60]~P3(f5(x601),f5(x603))+~P3(f5(x603),f5(x602))+~P2(f1(x601),f1(f5(x601)))+~P2(a2,f1(x601))+~P2(f1(x602),f1(f5(x602)))+~P2(f1(x603),f1(f5(x603)))+~P2(a2,f1(x602))+~P2(a2,f1(x603))+~P2(a2,f1(f5(x602)))+~P2(a2,f1(f5(x601)))+~P2(a2,f1(f5(x603)))+P2(f1(x601),f1(f5(f5(x601))))+~P2(f1(x602),f1(f5(f5(x602))))+~P2(f1(x603),f1(f5(f5(x603))))+~P2(a2,f1(f5(f5(x602))))+~P2(a2,f1(f5(f5(x601))))+~P2(a2,f1(f5(f5(x603))))+P2(f1(x602),f1(f5(f5(f5(x602)))))+~P2(f1(x603),f1(f5(f5(f5(x603)))))+~P2(a2,f1(f5(f5(f5(x602)))))+~P2(a2,f1(f5(f5(f5(x603)))))+~P2(a2,f1(f5(f5(f5(f5(x603))))))
% 64.59/64.60 [61]~P3(f5(x611),f5(x613))+~P3(f5(x612),f5(x611))+~P2(f1(x611),f1(f5(x611)))+~P2(f1(x612),f1(f5(x612)))+~P2(a2,f1(x611))+~P2(f1(x613),f1(f5(x613)))+~P2(a2,f1(x612))+~P2(a2,f1(x613))+~P2(a2,f1(f5(x613)))+~P2(a2,f1(f5(x611)))+~P2(a2,f1(f5(x612)))+P2(f1(x611),f1(f5(f5(x611))))+~P2(f1(x612),f1(f5(f5(x612))))+~P2(f1(x613),f1(f5(f5(x613))))+~P2(a2,f1(f5(f5(x613))))+~P2(a2,f1(f5(f5(x611))))+~P2(a2,f1(f5(f5(x612))))+P2(f1(x612),f1(f5(f5(f5(x612)))))+~P2(f1(x613),f1(f5(f5(f5(x613)))))+~P2(a2,f1(f5(f5(f5(x613)))))+~P2(a2,f1(f5(f5(f5(x612)))))+~P2(a2,f1(f5(f5(f5(f5(x613))))))
% 64.59/64.60 [62]~P3(f5(x621),f5(x622))+~P3(f5(x622),f5(x623))+~P2(f1(x621),f1(f5(x621)))+~P2(f1(x622),f1(f5(x622)))+~P2(a2,f1(x621))+~P2(f1(x623),f1(f5(x623)))+~P2(a2,f1(x622))+~P2(a2,f1(x623))+~P2(a2,f1(f5(x623)))+~P2(a2,f1(f5(x621)))+~P2(a2,f1(f5(x622)))+P2(f1(x621),f1(f5(f5(x621))))+~P2(f1(x622),f1(f5(f5(x622))))+~P2(f1(x623),f1(f5(f5(x623))))+~P2(a2,f1(f5(f5(x623))))+~P2(a2,f1(f5(f5(x621))))+~P2(a2,f1(f5(f5(x622))))+P2(f1(x622),f1(f5(f5(f5(x622)))))+~P2(f1(x623),f1(f5(f5(f5(x623)))))+~P2(a2,f1(f5(f5(f5(x623)))))+~P2(a2,f1(f5(f5(f5(x622)))))+~P2(a2,f1(f5(f5(f5(f5(x623))))))
% 64.59/64.60 [56]~P3(f5(x562),f5(x561))+~P3(f5(x563),f5(x562))+~P2(f1(x561),f1(f5(x561)))+~P2(a2,f1(x561))+~P2(f1(x562),f1(f5(x562)))+~P2(f1(x563),f1(f5(x563)))+~P2(a2,f1(x562))+~P2(a2,f1(x563))+~P2(a2,f1(f5(x561)))+~P2(a2,f1(f5(x562)))+~P2(a2,f1(f5(x563)))+~P2(f1(x561),f1(f5(f5(x561))))+~P2(f1(x562),f1(f5(f5(x562))))+~P2(f1(x563),f1(f5(f5(x563))))+~P2(a2,f1(f5(f5(x561))))+~P2(a2,f1(f5(f5(x562))))+~P2(a2,f1(f5(f5(x563))))+P2(f1(x561),f1(f5(f5(f5(x561)))))+P2(f1(x562),f1(f5(f5(f5(x562)))))+P2(f1(x563),f1(f5(f5(f5(x563)))))+~P2(a2,f1(f5(f5(f5(x561)))))+~P2(a2,f1(f5(f5(f5(x562)))))+~P2(a2,f1(f5(f5(f5(x563)))))
% 64.59/64.60 [69]~P3(f5(x692),f5(x691))+~P3(f5(x693),f5(x692))+~P2(f1(x691),f1(f5(x691)))+~P2(a2,f1(x691))+~P2(f1(x692),f1(f5(x692)))+~P2(f1(x693),f1(f5(x693)))+~P2(a2,f1(x692))+~P2(a2,f1(x693))+~P2(a2,f1(f5(x692)))+~P2(a2,f1(f5(x693)))+~P2(a2,f1(f5(x691)))+P2(f1(x691),f1(f5(f5(x691))))+~P2(f1(x692),f1(f5(f5(x692))))+~P2(f1(x693),f1(f5(f5(x693))))+~P2(a2,f1(f5(f5(x693))))+~P2(a2,f1(f5(f5(x692))))+~P2(a2,f1(f5(f5(x691))))+~P2(f1(x692),f1(f5(f5(f5(x692)))))+~P2(f1(x693),f1(f5(f5(f5(x693)))))+~P2(a2,f1(f5(f5(f5(x692)))))+~P2(a2,f1(f5(f5(f5(x693)))))+~P2(a2,f1(f5(f5(f5(f5(x692))))))+~P2(a2,f1(f5(f5(f5(f5(x693))))))
% 64.59/64.60 [70]~P3(f5(x701),f5(x702))+~P3(f5(x703),f5(x701))+~P2(f1(x701),f1(f5(x701)))+~P2(a2,f1(x701))+~P2(f1(x702),f1(f5(x702)))+~P2(f1(x703),f1(f5(x703)))+~P2(a2,f1(x702))+~P2(a2,f1(x703))+~P2(a2,f1(f5(x701)))+~P2(a2,f1(f5(x703)))+~P2(a2,f1(f5(x702)))+P2(f1(x701),f1(f5(f5(x701))))+~P2(f1(x702),f1(f5(f5(x702))))+~P2(f1(x703),f1(f5(f5(x703))))+~P2(a2,f1(f5(f5(x702))))+~P2(a2,f1(f5(f5(x701))))+~P2(a2,f1(f5(f5(x703))))+~P2(f1(x702),f1(f5(f5(f5(x702)))))+~P2(f1(x703),f1(f5(f5(f5(x703)))))+~P2(a2,f1(f5(f5(f5(x702)))))+~P2(a2,f1(f5(f5(f5(x703)))))+~P2(a2,f1(f5(f5(f5(f5(x702))))))+~P2(a2,f1(f5(f5(f5(f5(x703))))))
% 64.59/64.60 [71]~P3(f5(x711),f5(x713))+~P3(f5(x713),f5(x712))+~P2(f1(x711),f1(f5(x711)))+~P2(a2,f1(x711))+~P2(f1(x712),f1(f5(x712)))+~P2(f1(x713),f1(f5(x713)))+~P2(a2,f1(x712))+~P2(a2,f1(x713))+~P2(a2,f1(f5(x711)))+~P2(a2,f1(f5(x713)))+~P2(a2,f1(f5(x712)))+P2(f1(x711),f1(f5(f5(x711))))+~P2(f1(x712),f1(f5(f5(x712))))+~P2(f1(x713),f1(f5(f5(x713))))+~P2(a2,f1(f5(f5(x712))))+~P2(a2,f1(f5(f5(x711))))+~P2(a2,f1(f5(f5(x713))))+~P2(f1(x712),f1(f5(f5(f5(x712)))))+~P2(f1(x713),f1(f5(f5(f5(x713)))))+~P2(a2,f1(f5(f5(f5(x712)))))+~P2(a2,f1(f5(f5(f5(x713)))))+~P2(a2,f1(f5(f5(f5(f5(x712))))))+~P2(a2,f1(f5(f5(f5(f5(x713))))))
% 64.59/64.60 [66]~P3(f5(x662),f5(x661))+~P3(f5(x663),f5(x662))+~P2(f1(x661),f1(f5(x661)))+~P2(a2,f1(x661))+~P2(f1(x662),f1(f5(x662)))+~P2(f1(x663),f1(f5(x663)))+~P2(a2,f1(x662))+~P2(a2,f1(x663))+~P2(a2,f1(f5(x661)))+~P2(a2,f1(f5(x662)))+~P2(a2,f1(f5(x663)))+~P2(f1(x661),f1(f5(f5(x661))))+~P2(f1(x662),f1(f5(f5(x662))))+~P2(f1(x663),f1(f5(f5(x663))))+~P2(a2,f1(f5(f5(x662))))+~P2(a2,f1(f5(f5(x663))))+~P2(a2,f1(f5(f5(x661))))+P2(f1(x661),f1(f5(f5(f5(x661)))))+P2(f1(x662),f1(f5(f5(f5(x662)))))+~P2(f1(x663),f1(f5(f5(f5(x663)))))+~P2(a2,f1(f5(f5(f5(x661)))))+~P2(a2,f1(f5(f5(f5(x662)))))+~P2(a2,f1(f5(f5(f5(x663)))))+~P2(a2,f1(f5(f5(f5(f5(x663))))))
% 64.59/64.60 [67]~P3(f5(x673),f5(x671))+~P3(f5(x672),f5(x673))+~P2(f1(x671),f1(f5(x671)))+~P2(a2,f1(x671))+~P2(f1(x672),f1(f5(x672)))+~P2(f1(x673),f1(f5(x673)))+~P2(a2,f1(x672))+~P2(a2,f1(x673))+~P2(a2,f1(f5(x671)))+~P2(a2,f1(f5(x673)))+~P2(a2,f1(f5(x672)))+~P2(f1(x671),f1(f5(f5(x671))))+~P2(f1(x672),f1(f5(f5(x672))))+~P2(f1(x673),f1(f5(f5(x673))))+~P2(a2,f1(f5(f5(x671))))+~P2(a2,f1(f5(f5(x673))))+~P2(a2,f1(f5(f5(x672))))+P2(f1(x671),f1(f5(f5(f5(x671)))))+P2(f1(x672),f1(f5(f5(f5(x672)))))+~P2(f1(x673),f1(f5(f5(f5(x673)))))+~P2(a2,f1(f5(f5(f5(x671)))))+~P2(a2,f1(f5(f5(f5(x673)))))+~P2(a2,f1(f5(f5(f5(x672)))))+~P2(a2,f1(f5(f5(f5(f5(x673))))))
% 64.59/64.60 [68]~P3(f5(x681),f5(x683))+~P3(f5(x682),f5(x681))+~P2(f1(x681),f1(f5(x681)))+~P2(a2,f1(x681))+~P2(f1(x682),f1(f5(x682)))+~P2(f1(x683),f1(f5(x683)))+~P2(a2,f1(x682))+~P2(a2,f1(x683))+~P2(a2,f1(f5(x683)))+~P2(a2,f1(f5(x681)))+~P2(a2,f1(f5(x682)))+~P2(f1(x681),f1(f5(f5(x681))))+~P2(f1(x682),f1(f5(f5(x682))))+~P2(f1(x683),f1(f5(f5(x683))))+~P2(a2,f1(f5(f5(x683))))+~P2(a2,f1(f5(f5(x681))))+~P2(a2,f1(f5(f5(x682))))+P2(f1(x681),f1(f5(f5(f5(x681)))))+P2(f1(x682),f1(f5(f5(f5(x682)))))+~P2(f1(x683),f1(f5(f5(f5(x683)))))+~P2(a2,f1(f5(f5(f5(x683)))))+~P2(a2,f1(f5(f5(f5(x681)))))+~P2(a2,f1(f5(f5(f5(x682)))))+~P2(a2,f1(f5(f5(f5(f5(x683))))))
% 64.59/64.60 [72]~P3(f5(x722),f5(x721))+~P3(f5(x723),f5(x722))+~P2(f1(x721),f1(f5(x721)))+~P2(a2,f1(x721))+~P2(f1(x722),f1(f5(x722)))+~P2(f1(x723),f1(f5(x723)))+~P2(a2,f1(x722))+~P2(a2,f1(x723))+~P2(a2,f1(f5(x721)))+~P2(a2,f1(f5(x722)))+~P2(a2,f1(f5(x723)))+~P2(f1(x721),f1(f5(f5(x721))))+~P2(f1(x722),f1(f5(f5(x722))))+~P2(f1(x723),f1(f5(f5(x723))))+~P2(a2,f1(f5(f5(x721))))+~P2(a2,f1(f5(f5(x723))))+~P2(a2,f1(f5(f5(x722))))+P2(f1(x721),f1(f5(f5(f5(x721)))))+~P2(f1(x722),f1(f5(f5(f5(x722)))))+~P2(f1(x723),f1(f5(f5(f5(x723)))))+~P2(a2,f1(f5(f5(f5(x721)))))+~P2(a2,f1(f5(f5(f5(x722)))))+~P2(a2,f1(f5(f5(f5(x723)))))+~P2(a2,f1(f5(f5(f5(f5(x722))))))+~P2(a2,f1(f5(f5(f5(f5(x723))))))
% 64.59/64.60 [73]~P3(f5(x731),f5(x732))+~P3(f5(x733),f5(x731))+~P2(f1(x731),f1(f5(x731)))+~P2(a2,f1(x731))+~P2(f1(x732),f1(f5(x732)))+~P2(f1(x733),f1(f5(x733)))+~P2(a2,f1(x732))+~P2(a2,f1(x733))+~P2(a2,f1(f5(x732)))+~P2(a2,f1(f5(x731)))+~P2(a2,f1(f5(x733)))+~P2(f1(x731),f1(f5(f5(x731))))+~P2(f1(x732),f1(f5(f5(x732))))+~P2(f1(x733),f1(f5(f5(x733))))+~P2(a2,f1(f5(f5(x732))))+~P2(a2,f1(f5(f5(x733))))+~P2(a2,f1(f5(f5(x731))))+P2(f1(x731),f1(f5(f5(f5(x731)))))+~P2(f1(x732),f1(f5(f5(f5(x732)))))+~P2(f1(x733),f1(f5(f5(f5(x733)))))+~P2(a2,f1(f5(f5(f5(x732)))))+~P2(a2,f1(f5(f5(f5(x731)))))+~P2(a2,f1(f5(f5(f5(x733)))))+~P2(a2,f1(f5(f5(f5(f5(x732))))))+~P2(a2,f1(f5(f5(f5(f5(x733))))))
% 64.59/64.60 [74]~P3(f5(x743),f5(x742))+~P3(f5(x741),f5(x743))+~P2(f1(x741),f1(f5(x741)))+~P2(a2,f1(x741))+~P2(f1(x742),f1(f5(x742)))+~P2(f1(x743),f1(f5(x743)))+~P2(a2,f1(x742))+~P2(a2,f1(x743))+~P2(a2,f1(f5(x742)))+~P2(a2,f1(f5(x743)))+~P2(a2,f1(f5(x741)))+~P2(f1(x741),f1(f5(f5(x741))))+~P2(f1(x742),f1(f5(f5(x742))))+~P2(f1(x743),f1(f5(f5(x743))))+~P2(a2,f1(f5(f5(x742))))+~P2(a2,f1(f5(f5(x741))))+~P2(a2,f1(f5(f5(x743))))+P2(f1(x741),f1(f5(f5(f5(x741)))))+~P2(f1(x742),f1(f5(f5(f5(x742)))))+~P2(f1(x743),f1(f5(f5(f5(x743)))))+~P2(a2,f1(f5(f5(f5(x742)))))+~P2(a2,f1(f5(f5(f5(x743)))))+~P2(a2,f1(f5(f5(f5(x741)))))+~P2(a2,f1(f5(f5(f5(f5(x742))))))+~P2(a2,f1(f5(f5(f5(f5(x743))))))
% 64.59/64.60 [75]~P3(f5(x752),f5(x751))+~P3(f5(x753),f5(x752))+~P2(f1(x751),f1(f5(x751)))+~P2(f1(x752),f1(f5(x752)))+~P2(a2,f1(x751))+~P2(f1(x753),f1(f5(x753)))+~P2(a2,f1(x752))+~P2(a2,f1(x753))+~P2(a2,f1(f5(x751)))+~P2(a2,f1(f5(x752)))+~P2(a2,f1(f5(x753)))+~P2(f1(x751),f1(f5(f5(x751))))+~P2(f1(x752),f1(f5(f5(x752))))+~P2(f1(x753),f1(f5(f5(x753))))+~P2(a2,f1(f5(f5(x753))))+~P2(a2,f1(f5(f5(x752))))+~P2(a2,f1(f5(f5(x751))))+~P2(f1(x751),f1(f5(f5(f5(x751)))))+~P2(f1(x752),f1(f5(f5(f5(x752)))))+~P2(f1(x753),f1(f5(f5(f5(x753)))))+~P2(a2,f1(f5(f5(f5(x751)))))+~P2(a2,f1(f5(f5(f5(x752)))))+~P2(a2,f1(f5(f5(f5(x753)))))+~P2(a2,f1(f5(f5(f5(f5(x751))))))+~P2(a2,f1(f5(f5(f5(f5(x752))))))+~P2(a2,f1(f5(f5(f5(f5(x753))))))
% 64.59/64.60 %EqnAxiom
% 64.59/64.60
% 64.59/64.60 %-------------------------------------------
% 64.59/64.60 cnf(78,plain,
% 64.59/64.60 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))),
% 64.59/64.60 inference(scs_inference,[],[2,1,5,3])).
% 64.59/64.60 cnf(79,plain,
% 64.59/64.60 (P2(f1(a4),f1(f5(a4)))+P3(f5(a4),f5(a4))),
% 64.59/64.60 inference(scs_inference,[],[1,2,78,4])).
% 64.59/64.60 cnf(86,plain,
% 64.59/64.60 (P2(a2,f1(a4))),
% 64.59/64.60 inference(scs_inference,[],[1,2,3])).
% 64.59/64.60 cnf(87,plain,
% 64.59/64.60 (P1(f1(x871),f3(a2))),
% 64.59/64.60 inference(rename_variables,[],[1])).
% 64.59/64.60 cnf(89,plain,
% 64.59/64.60 (P2(a2,f1(f5(a4)))),
% 64.59/64.60 inference(scs_inference,[],[1,87,2,3,4])).
% 64.59/64.60 cnf(90,plain,
% 64.59/64.60 (P1(f1(x901),f3(a2))),
% 64.59/64.60 inference(rename_variables,[],[1])).
% 64.59/64.60 cnf(92,plain,
% 64.59/64.60 (P2(a2,f1(f5(f5(a4))))),
% 64.59/64.60 inference(scs_inference,[],[1,87,90,2,3,4,6])).
% 64.59/64.60 cnf(93,plain,
% 64.59/64.60 (P1(f1(x931),f3(a2))),
% 64.59/64.60 inference(rename_variables,[],[1])).
% 64.59/64.60 cnf(95,plain,
% 64.59/64.60 (P2(a2,f1(f5(f5(f5(a4)))))),
% 64.59/64.60 inference(scs_inference,[],[1,87,90,93,2,3,4,6,7])).
% 64.59/64.60 cnf(96,plain,
% 64.59/64.60 (P1(f1(x961),f3(a2))),
% 64.59/64.60 inference(rename_variables,[],[1])).
% 64.59/64.60 cnf(98,plain,
% 64.59/64.60 (P2(a2,f1(f5(f5(f5(f5(a4))))))),
% 64.59/64.60 inference(scs_inference,[],[1,87,90,93,96,2,3,4,6,7,10])).
% 64.59/64.60 cnf(101,plain,
% 64.59/64.60 (~P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))),
% 64.59/64.60 inference(scs_inference,[],[1,87,90,93,96,2,3,4,6,7,10,9])).
% 64.59/64.60 cnf(107,plain,
% 64.59/64.60 (~P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(a4))))),
% 64.59/64.60 inference(scs_inference,[],[92,89,86,101,21])).
% 64.59/64.60 cnf(117,plain,
% 64.59/64.60 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))+~P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 64.59/64.60 inference(scs_inference,[],[86,98,95,89,92,22])).
% 64.59/64.60 cnf(138,plain,
% 64.59/64.60 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))+P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 64.59/64.60 inference(scs_inference,[],[89,86,92,95,14])).
% 64.59/64.60 cnf(320,plain,
% 64.59/64.60 (P2(f1(a4),f1(f5(a4)))),
% 64.59/64.60 inference(scs_inference,[],[101,79])).
% 64.59/64.60 cnf(323,plain,
% 64.59/64.60 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(f5(a4))))+~P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 64.59/64.60 inference(scs_inference,[],[320,117])).
% 64.59/64.60 cnf(324,plain,
% 64.59/64.60 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(f5(a4))))+P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 64.59/64.60 inference(scs_inference,[],[320,138])).
% 64.59/64.60 cnf(332,plain,
% 64.59/64.60 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(a4))))),
% 64.59/64.60 inference(scs_inference,[],[320,86,89,92,8])).
% 64.59/64.60 cnf(340,plain,
% 64.59/64.60 (P2(f1(a4),f1(f5(f5(a4))))),
% 64.59/64.60 inference(scs_inference,[],[332,107])).
% 64.59/64.60 cnf(343,plain,
% 64.59/64.60 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 64.59/64.60 inference(scs_inference,[],[340,323])).
% 64.59/64.60 cnf(344,plain,
% 64.59/64.60 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 64.59/64.60 inference(scs_inference,[],[340,324])).
% 64.59/64.60 cnf(346,plain,
% 64.59/64.60 (~P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 64.59/64.60 inference(scs_inference,[],[340,320,86,89,98,95,92,75])).
% 64.59/64.60 cnf(391,plain,
% 64.59/64.60 (P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 64.59/64.60 inference(scs_inference,[],[95,340,89,320,92,86,344,56])).
% 64.59/64.60 cnf(392,plain,
% 64.59/64.60 (P3(f5(a4),f5(a4))),
% 64.59/64.60 inference(scs_inference,[],[391,343])).
% 64.59/64.60 cnf(393,plain,
% 64.59/64.60 (~P3(f5(a4),f5(a4))),
% 64.59/64.60 inference(scs_inference,[],[391,346])).
% 64.59/64.60 cnf(395,plain,
% 64.59/64.60 ($false),
% 64.59/64.60 inference(scs_inference,[],[392,393]),
% 64.59/64.60 ['proof']).
% 64.59/64.60 % SZS output end Proof
% 64.59/64.60 % Total time :63.750000s
%------------------------------------------------------------------------------