%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYO649-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 : n026.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:39 EDT 2024
% Result : Unsatisfiable 58.78s 58.84s
% Output : CNFRefutation 58.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYO649-1 : TPTP v8.2.0. Released v7.3.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.35 % Computer : n026.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Sun Jun 23 06:39:39 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.21/0.60 start to proof:theBenchmark
% 58.75/58.82 %-------------------------------------------
% 58.75/58.82 % File :CSE---1.7
% 58.75/58.82 % Problem :theBenchmark
% 58.75/58.82 % Transform :cnf
% 58.75/58.82 % Format :tptp:raw
% 58.75/58.82 % Command :java -jar mcs_scs.jar %d %s
% 58.75/58.82
% 58.75/58.82 % Result :Theorem 58.120000s
% 58.75/58.82 % Output :CNFRefutation 58.120000s
% 58.75/58.82 %-------------------------------------------
% 58.75/58.82 %------------------------------------------------------------------------------
% 58.75/58.82 % File : SYO649-1 : TPTP v8.2.0. Released v7.3.0.
% 58.75/58.82 % Domain : Syntactic
% 58.75/58.82 % Problem : GSM_1_1_5
% 58.75/58.82 % Version : Especial.
% 58.75/58.82 % English :
% 58.75/58.82
% 58.75/58.82 % Refs : [EH+16] Ebner et al. (2016), System Description: GAPT 2.0
% 58.75/58.82 % : [Cer18] Cerna (2018), Email to Geoff Sutcliffe
% 58.75/58.82 % Source : [Cer18]
% 58.75/58.82 % Names : GSM_1_1_5 [Cer18]
% 58.75/58.82
% 58.75/58.82 % Status : Unsatisfiable
% 58.75/58.82 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.3.0
% 58.75/58.82 % Syntax : Number of clauses : 38 ( 2 unt; 26 nHn; 37 RR)
% 58.75/58.82 % Number of literals : 424 ( 0 equ; 362 neg)
% 58.75/58.82 % Maximal clause size : 21 ( 11 avg)
% 58.75/58.82 % Maximal term depth : 7 ( 2 avg)
% 58.75/58.82 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty)
% 58.75/58.82 % Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% 58.75/58.83 % Number of variables : 62 ( 1 sgn)
% 58.75/58.83 % SPC : CNF_UNS_RFO_NEQ_NHN
% 58.75/58.83
% 58.75/58.83 % Comments : Created using the GAPT system - https://github.com/gapt/gapt/blob/
% 58.75/58.83 % master/examples/schema/GradedStrictMonotoneSequenceSchema.scala
% 58.75/58.83 %------------------------------------------------------------------------------
% 58.75/58.83 cnf(clause_252,axiom,
% 58.75/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.75/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'('0',f(A_1))
% 58.75/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(suc(suc(suc(B_2))))))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.75/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.75/58.83 | ~ 'E'('0',f(B_2))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(suc(B_2)))))))
% 58.75/58.83 | 'E'(f(A_1),f(suc(suc(suc(suc(A_1)))))) ) ).
% 58.75/58.83
% 58.75/58.83 cnf(clause_375,axiom,
% 58.75/58.83 ( ~ 'E'('0',f(suc(A_1)))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'('0',f(A_1))
% 58.75/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.75/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.75/58.83 | ~ 'E'('0',f(B_2))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.75/58.83 | 'E'(f(A_1),f(suc(suc(A_1))))
% 58.75/58.83 | 'E'(f(B_2),f(suc(suc(B_2)))) ) ).
% 58.75/58.83
% 58.75/58.83 cnf(clause_1480,axiom,
% 58.75/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.75/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'('0',f(A_1))
% 58.75/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.75/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.75/58.83 | ~ 'E'('0',f(B_2))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.75/58.83 | 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.75/58.83 | 'E'(f(B_2),f(suc(suc(B_2)))) ) ).
% 58.75/58.83
% 58.75/58.83 cnf(clause_703,axiom,
% 58.75/58.83 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.75/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.75/58.83 | ~ 'E'('0',f(A_1))
% 58.75/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.75/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.75/58.83 | ~ 'E'('0',f(B_2))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.75/58.83 | 'E'(f(A_1),f(suc(A_1)))
% 58.75/58.83 | 'E'(f(B_2),f(suc(suc(suc(suc(B_2)))))) ) ).
% 58.75/58.83
% 58.75/58.83 cnf(clause_1507,axiom,
% 58.75/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.75/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'('0',f(A_1))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(suc(A_1)))))))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.75/58.83 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.75/58.83
% 58.75/58.83 cnf(clause_62,axiom,
% 58.75/58.83 ( ~ 'LE'(f(suc(suc(suc(suc(suc(B_1)))))),s('0'))
% 58.75/58.83 | 'E'('0',f(suc(suc(suc(suc(suc(B_1)))))))
% 58.75/58.83 | 'LE'(f(B_1),'0') ) ).
% 58.75/58.83
% 58.75/58.83 cnf(clause_716,axiom,
% 58.75/58.83 ~ 'LE'(f(z),'0') ).
% 58.75/58.83
% 58.75/58.83 cnf(clause_999,axiom,
% 58.75/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.75/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'('0',f(A_1))
% 58.75/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.75/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.75/58.83 | ~ 'E'('0',f(B_2))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.75/58.83 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.75/58.83 | 'E'(f(B_2),f(suc(suc(B_2)))) ) ).
% 58.75/58.83
% 58.75/58.83 cnf(clause_512,axiom,
% 58.75/58.83 ( ~ 'E'('0',f(suc(A_1)))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.75/58.83 | ~ 'E'('0',f(A_1))
% 58.75/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.75/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.75/58.83 | ~ 'E'('0',f(B_2))
% 58.75/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.75/58.83 | 'E'(f(A_1),f(suc(suc(A_1))))
% 58.75/58.83 | 'E'(f(B_2),f(suc(B_2))) ) ).
% 58.75/58.83
% 58.75/58.83 cnf(clause_774,axiom,
% 58.75/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.75/58.83 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.75/58.83 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.75/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(A_1))
% 58.78/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.83 | ~ 'E'('0',f(B_2))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | 'E'(f(B_2),f(suc(suc(suc(B_2))))) ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_771,axiom,
% 58.78/58.83 ( ~ 'E'('0',f(suc(A_1)))
% 58.78/58.83 | ~ 'E'('0',f(A_1))
% 58.78/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.83 | ~ 'E'('0',f(B_2))
% 58.78/58.83 | 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.83 | 'E'(f(B_2),f(suc(B_2))) ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_962,axiom,
% 58.78/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(A_1))
% 58.78/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.83 | ~ 'E'('0',f(B_2))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(suc(A_1)))))))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | 'E'(f(B_2),f(suc(suc(suc(B_2))))) ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_1282,axiom,
% 58.78/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(A_1))
% 58.78/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.83 | ~ 'E'('0',f(B_2))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(suc(A_1)))))))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | 'E'(f(B_2),f(suc(suc(B_2)))) ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_1501,axiom,
% 58.78/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(A_1))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_1012,axiom,
% 58.78/58.83 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(A_1))
% 58.78/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.83 | ~ 'E'('0',f(B_2))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.83 | 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.83 | 'E'(f(B_2),f(suc(suc(suc(B_2))))) ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_1214,axiom,
% 58.78/58.83 ( ~ 'LE'(f(suc(suc(suc(B_1)))),s('0'))
% 58.78/58.83 | 'E'('0',f(suc(suc(suc(B_1)))))
% 58.78/58.83 | 'LE'(f(B_1),'0') ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_365,axiom,
% 58.78/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(A_1))
% 58.78/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.83 | ~ 'E'('0',f(B_2))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(suc(A_1)))))))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.78/58.83 | 'E'(f(B_2),f(suc(B_2))) ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_1033,axiom,
% 58.78/58.83 ( ~ 'LE'(f(suc(suc(suc(suc(B_1))))),s('0'))
% 58.78/58.83 | 'E'('0',f(suc(suc(suc(suc(B_1))))))
% 58.78/58.83 | 'LE'(f(B_1),'0') ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_1136,axiom,
% 58.78/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(A_1))
% 58.78/58.83 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(suc(suc(suc(B_2))))))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.83 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.83 | ~ 'E'('0',f(B_2))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(suc(suc(B_2)))))))
% 58.78/58.83 | 'E'(f(A_1),f(suc(suc(suc(A_1))))) ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_1172,axiom,
% 58.78/58.83 ( ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.83 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.83 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.83 | ~ 'E'('0',f(A_1))
% 58.78/58.83 | 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.83 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.78/58.83
% 58.78/58.83 cnf(clause_1046,axiom,
% 58.78/58.83 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.83 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(suc(A_1)))))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(suc(B_2))))))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_258,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_162,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | 'E'(f(B_2),f(suc(suc(B_2)))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_909,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.78/58.84 | 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.78/58.84 | 'E'(f(B_2),f(suc(B_2))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_985,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | 'E'(f(B_2),f(suc(suc(suc(B_2))))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_519,axiom,
% 58.78/58.84 ( ~ 'LE'(f(suc(suc(B_1))),s('0'))
% 58.78/58.84 | 'E'('0',f(suc(suc(B_1))))
% 58.78/58.84 | 'LE'(f(B_1),'0') ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_1121,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(suc(B_2)))))))
% 58.78/58.84 | 'E'(f(A_1),f(suc(suc(A_1)))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_1522,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.84 | 'E'(f(B_2),f(suc(suc(suc(suc(B_2)))))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_349,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.84 | 'E'(f(B_2),f(suc(B_2))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_369,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(suc(B_2)))))))
% 58.78/58.84 | 'E'(f(A_1),f(suc(A_1))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_412,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.84 | 'E'(f(B_2),f(suc(suc(suc(B_2))))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_649,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(suc(A_1)))))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.78/58.84 | 'E'(f(B_2),f(suc(suc(suc(suc(B_2)))))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_314,axiom,
% 58.78/58.84 ( ~ 'LE'(f(B_1),s('0'))
% 58.78/58.84 | 'E'('0',f(B_1))
% 58.78/58.84 | 'LE'(f(B_1),'0') ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_102,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.78/58.84 | 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
% 58.78/58.84 | 'E'(f(B_2),f(suc(suc(suc(suc(B_2)))))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_1514,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.78/58.84 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_1370,axiom,
% 58.78/58.84 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.78/58.84 | ~ 'E'('0',f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.78/58.84 | ~ 'E'('0',f(A_1))
% 58.78/58.84 | ~ 'E'('0',f(suc(B_2)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.78/58.84 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.78/58.84 | ~ 'E'('0',f(B_2))
% 58.78/58.84 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.78/58.84 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.78/58.84 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.78/58.84 | 'E'(f(A_1),f(suc(suc(A_1))))
% 58.78/58.84 | 'E'(f(B_2),f(suc(suc(suc(suc(B_2)))))) ) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_1382,axiom,
% 58.78/58.84 'LE'(f(A),s('0')) ).
% 58.78/58.84
% 58.78/58.84 cnf(clause_1518,axiom,
% 58.78/58.84 ( ~ 'LE'(f(suc(B_1)),s('0'))
% 58.78/58.84 | 'E'('0',f(suc(B_1)))
% 58.78/58.84 | 'LE'(f(B_1),'0') ) ).
% 58.78/58.84
% 58.78/58.84 %------------------------------------------------------------------------------
% 58.78/58.84 %-------------------------------------------
% 58.78/58.84 % Proof found
% 58.78/58.84 % SZS status Theorem for theBenchmark
% 58.78/58.84 % SZS output start Proof
% 58.78/58.84 %ClaNum:38(EqnAxiom:0)
% 58.78/58.84 %VarNum:607(SingletonVarNum:62)
% 58.78/58.84 %MaxLitNum:21
% 58.78/58.84 %MaxfuncDepth:6
% 58.78/58.84 %SharedTerms:5
% 58.78/58.84 [2]~P1(f1(a4),a2)
% 58.78/58.84 [1]P1(f1(x11),f3(a2))
% 58.78/58.84 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2)
% 58.78/58.84 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41)))
% 58.78/58.84 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61))))
% 58.78/58.84 [8]P1(f1(x81),a2)+~P1(f1(f5(f5(f5(x81)))),f3(a2))+P2(a2,f1(f5(f5(f5(x81)))))
% 58.78/58.84 [12]P1(f1(x121),a2)+~P1(f1(f5(f5(f5(f5(x121))))),f3(a2))+P2(a2,f1(f5(f5(f5(f5(x121))))))
% 58.78/58.84 [19]P1(f1(x191),a2)+~P1(f1(f5(f5(f5(f5(f5(x191)))))),f3(a2))+P2(a2,f1(f5(f5(f5(f5(f5(x191)))))))
% 58.78/58.84 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51)))
% 58.78/58.84 [9]P3(f5(x91),f5(x91))+~P2(a2,f1(x91))+~P2(f1(x91),f1(f5(x91)))+P2(f1(x91),f1(f5(f5(x91))))+~P2(a2,f1(f5(x91)))+~P2(a2,f1(f5(f5(x91))))
% 58.78/58.84 [7]~P3(f5(x72),f5(x71))+P2(f1(x71),f1(f5(x71)))+P2(f1(x72),f1(f5(x72)))+~P2(a2,f1(x71))+~P2(a2,f1(x72))+~P2(a2,f1(f5(x71)))+~P2(a2,f1(f5(x72)))
% 58.78/58.84 [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)))))
% 58.78/58.84 [10]~P3(f5(x102),f5(x101))+P2(f1(x101),f1(f5(x101)))+~P2(a2,f1(x101))+~P2(f1(x102),f1(f5(x102)))+~P2(a2,f1(x102))+~P2(a2,f1(f5(x101)))+~P2(a2,f1(f5(x102)))+P2(f1(x102),f1(f5(f5(x102))))+~P2(a2,f1(f5(f5(x102))))
% 58.78/58.84 [11]~P3(f5(x111),f5(x112))+P2(f1(x111),f1(f5(x111)))+~P2(a2,f1(x111))+~P2(f1(x112),f1(f5(x112)))+~P2(a2,f1(x112))+~P2(a2,f1(f5(x112)))+~P2(a2,f1(f5(x111)))+P2(f1(x112),f1(f5(f5(x112))))+~P2(a2,f1(f5(f5(x112))))
% 58.78/58.84 [20]P3(f5(x201),f5(x201))+~P2(a2,f1(x201))+~P2(f1(x201),f1(f5(x201)))+~P2(f1(x201),f1(f5(f5(x201))))+~P2(a2,f1(f5(x201)))+~P2(f1(x201),f1(f5(f5(f5(x201)))))+~P2(a2,f1(f5(f5(x201))))+P2(f1(x201),f1(f5(f5(f5(f5(x201))))))+~P2(a2,f1(f5(f5(f5(x201)))))+~P2(a2,f1(f5(f5(f5(f5(x201))))))
% 58.78/58.84 [28]P3(f5(x281),f5(x281))+~P2(a2,f1(x281))+~P2(f1(x281),f1(f5(x281)))+~P2(f1(x281),f1(f5(f5(x281))))+~P2(a2,f1(f5(x281)))+~P2(f1(x281),f1(f5(f5(f5(x281)))))+~P2(a2,f1(f5(f5(x281))))+~P2(f1(x281),f1(f5(f5(f5(f5(x281))))))+~P2(a2,f1(f5(f5(f5(x281)))))+~P2(a2,f1(f5(f5(f5(f5(x281))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x281)))))))
% 58.78/58.84 [13]~P3(f5(x132),f5(x131))+~P2(f1(x131),f1(f5(x131)))+~P2(a2,f1(x131))+~P2(f1(x132),f1(f5(x132)))+~P2(a2,f1(x132))+~P2(a2,f1(f5(x131)))+~P2(a2,f1(f5(x132)))+P2(f1(x131),f1(f5(f5(x131))))+P2(f1(x132),f1(f5(f5(x132))))+~P2(a2,f1(f5(f5(x131))))+~P2(a2,f1(f5(f5(x132))))
% 58.78/58.84 [15]~P3(f5(x151),f5(x152))+P2(f1(x151),f1(f5(x151)))+~P2(a2,f1(x151))+~P2(f1(x152),f1(f5(x152)))+~P2(a2,f1(x152))+~P2(a2,f1(f5(x151)))+~P2(a2,f1(f5(x152)))+~P2(f1(x152),f1(f5(f5(x152))))+~P2(a2,f1(f5(f5(x152))))+P2(f1(x152),f1(f5(f5(f5(x152)))))+~P2(a2,f1(f5(f5(f5(x152)))))
% 58.78/58.84 [16]~P3(f5(x162),f5(x161))+P2(f1(x161),f1(f5(x161)))+~P2(a2,f1(x161))+~P2(f1(x162),f1(f5(x162)))+~P2(a2,f1(x162))+~P2(a2,f1(f5(x161)))+~P2(a2,f1(f5(x162)))+~P2(f1(x162),f1(f5(f5(x162))))+~P2(a2,f1(f5(f5(x162))))+P2(f1(x162),f1(f5(f5(f5(x162)))))+~P2(a2,f1(f5(f5(f5(x162)))))
% 58.78/58.84 [17]~P3(f5(x171),f5(x172))+~P2(f1(x171),f1(f5(x171)))+~P2(a2,f1(x171))+~P2(f1(x172),f1(f5(x172)))+~P2(a2,f1(x172))+~P2(a2,f1(f5(x171)))+~P2(a2,f1(f5(x172)))+P2(f1(x171),f1(f5(f5(x171))))+~P2(f1(x172),f1(f5(f5(x172))))+~P2(a2,f1(f5(f5(x171))))+~P2(a2,f1(f5(f5(x172))))+P2(f1(x172),f1(f5(f5(f5(x172)))))+~P2(a2,f1(f5(f5(f5(x172)))))
% 58.78/58.84 [18]~P3(f5(x182),f5(x181))+~P2(f1(x181),f1(f5(x181)))+~P2(a2,f1(x181))+~P2(f1(x182),f1(f5(x182)))+~P2(a2,f1(x182))+~P2(a2,f1(f5(x181)))+~P2(a2,f1(f5(x182)))+P2(f1(x181),f1(f5(f5(x181))))+~P2(f1(x182),f1(f5(f5(x182))))+~P2(a2,f1(f5(f5(x181))))+~P2(a2,f1(f5(f5(x182))))+P2(f1(x182),f1(f5(f5(f5(x182)))))+~P2(a2,f1(f5(f5(f5(x182)))))
% 58.82/58.84 [22]~P3(f5(x221),f5(x222))+P2(f1(x221),f1(f5(x221)))+~P2(a2,f1(x221))+~P2(f1(x222),f1(f5(x222)))+~P2(a2,f1(x222))+~P2(a2,f1(f5(x221)))+~P2(a2,f1(f5(x222)))+~P2(f1(x222),f1(f5(f5(x222))))+~P2(a2,f1(f5(f5(x222))))+~P2(f1(x222),f1(f5(f5(f5(x222)))))+~P2(a2,f1(f5(f5(f5(x222)))))+P2(f1(x222),f1(f5(f5(f5(f5(x222))))))+~P2(a2,f1(f5(f5(f5(f5(x222))))))
% 58.82/58.84 [23]~P3(f5(x232),f5(x231))+P2(f1(x231),f1(f5(x231)))+~P2(a2,f1(x231))+~P2(f1(x232),f1(f5(x232)))+~P2(a2,f1(x232))+~P2(a2,f1(f5(x231)))+~P2(a2,f1(f5(x232)))+~P2(f1(x232),f1(f5(f5(x232))))+~P2(a2,f1(f5(f5(x232))))+~P2(f1(x232),f1(f5(f5(f5(x232)))))+~P2(a2,f1(f5(f5(f5(x232)))))+P2(f1(x232),f1(f5(f5(f5(f5(x232))))))+~P2(a2,f1(f5(f5(f5(f5(x232))))))
% 58.82/58.84 [29]~P3(f5(x291),f5(x292))+P2(f1(x291),f1(f5(x291)))+~P2(a2,f1(x291))+~P2(f1(x292),f1(f5(x292)))+~P2(a2,f1(x292))+~P2(a2,f1(f5(x291)))+~P2(a2,f1(f5(x292)))+~P2(f1(x292),f1(f5(f5(x292))))+~P2(a2,f1(f5(f5(x292))))+~P2(f1(x292),f1(f5(f5(f5(x292)))))+~P2(a2,f1(f5(f5(f5(x292)))))+~P2(f1(x292),f1(f5(f5(f5(f5(x292))))))+~P2(a2,f1(f5(f5(f5(f5(x292))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x292)))))))
% 58.82/58.84 [30]~P3(f5(x302),f5(x301))+P2(f1(x301),f1(f5(x301)))+~P2(a2,f1(x301))+~P2(f1(x302),f1(f5(x302)))+~P2(a2,f1(x302))+~P2(a2,f1(f5(x301)))+~P2(a2,f1(f5(x302)))+~P2(f1(x302),f1(f5(f5(x302))))+~P2(a2,f1(f5(f5(x302))))+~P2(f1(x302),f1(f5(f5(f5(x302)))))+~P2(a2,f1(f5(f5(f5(x302)))))+~P2(f1(x302),f1(f5(f5(f5(f5(x302))))))+~P2(a2,f1(f5(f5(f5(f5(x302))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x302)))))))
% 58.82/58.84 [21]~P3(f5(x212),f5(x211))+~P2(f1(x211),f1(f5(x211)))+~P2(a2,f1(x211))+~P2(f1(x212),f1(f5(x212)))+~P2(a2,f1(x212))+~P2(a2,f1(f5(x211)))+~P2(a2,f1(f5(x212)))+~P2(f1(x211),f1(f5(f5(x211))))+~P2(f1(x212),f1(f5(f5(x212))))+~P2(a2,f1(f5(f5(x211))))+~P2(a2,f1(f5(f5(x212))))+P2(f1(x211),f1(f5(f5(f5(x211)))))+P2(f1(x212),f1(f5(f5(f5(x212)))))+~P2(a2,f1(f5(f5(f5(x211)))))+~P2(a2,f1(f5(f5(f5(x212)))))
% 58.82/58.84 [24]~P3(f5(x241),f5(x242))+~P2(f1(x241),f1(f5(x241)))+~P2(a2,f1(x241))+~P2(f1(x242),f1(f5(x242)))+~P2(a2,f1(x242))+~P2(a2,f1(f5(x241)))+~P2(a2,f1(f5(x242)))+P2(f1(x241),f1(f5(f5(x241))))+~P2(f1(x242),f1(f5(f5(x242))))+~P2(a2,f1(f5(f5(x241))))+~P2(a2,f1(f5(f5(x242))))+~P2(f1(x242),f1(f5(f5(f5(x242)))))+~P2(a2,f1(f5(f5(f5(x242)))))+P2(f1(x242),f1(f5(f5(f5(f5(x242))))))+~P2(a2,f1(f5(f5(f5(f5(x242))))))
% 58.82/58.84 [25]~P3(f5(x252),f5(x251))+~P2(f1(x251),f1(f5(x251)))+~P2(a2,f1(x251))+~P2(f1(x252),f1(f5(x252)))+~P2(a2,f1(x252))+~P2(a2,f1(f5(x251)))+~P2(a2,f1(f5(x252)))+P2(f1(x251),f1(f5(f5(x251))))+~P2(f1(x252),f1(f5(f5(x252))))+~P2(a2,f1(f5(f5(x251))))+~P2(a2,f1(f5(f5(x252))))+~P2(f1(x252),f1(f5(f5(f5(x252)))))+~P2(a2,f1(f5(f5(f5(x252)))))+P2(f1(x252),f1(f5(f5(f5(f5(x252))))))+~P2(a2,f1(f5(f5(f5(f5(x252))))))
% 58.82/58.84 [31]~P3(f5(x311),f5(x312))+~P2(f1(x311),f1(f5(x311)))+~P2(a2,f1(x311))+~P2(f1(x312),f1(f5(x312)))+~P2(a2,f1(x312))+~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(a2,f1(f5(f5(x311))))+~P2(a2,f1(f5(f5(x312))))+~P2(f1(x312),f1(f5(f5(f5(x312)))))+~P2(a2,f1(f5(f5(f5(x312)))))+~P2(f1(x312),f1(f5(f5(f5(f5(x312))))))+~P2(a2,f1(f5(f5(f5(f5(x312))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x312)))))))
% 58.82/58.84 [32]~P3(f5(x322),f5(x321))+~P2(f1(x321),f1(f5(x321)))+~P2(a2,f1(x321))+~P2(f1(x322),f1(f5(x322)))+~P2(a2,f1(x322))+~P2(a2,f1(f5(x321)))+~P2(a2,f1(f5(x322)))+P2(f1(x321),f1(f5(f5(x321))))+~P2(f1(x322),f1(f5(f5(x322))))+~P2(a2,f1(f5(f5(x321))))+~P2(a2,f1(f5(f5(x322))))+~P2(f1(x322),f1(f5(f5(f5(x322)))))+~P2(a2,f1(f5(f5(f5(x322)))))+~P2(f1(x322),f1(f5(f5(f5(f5(x322))))))+~P2(a2,f1(f5(f5(f5(f5(x322))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x322)))))))
% 58.82/58.84 [26]~P3(f5(x262),f5(x261))+~P2(f1(x261),f1(f5(x261)))+~P2(a2,f1(x261))+~P2(f1(x262),f1(f5(x262)))+~P2(a2,f1(x262))+~P2(a2,f1(f5(x261)))+~P2(a2,f1(f5(x262)))+~P2(f1(x261),f1(f5(f5(x261))))+~P2(f1(x262),f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(x261))))+~P2(a2,f1(f5(f5(x262))))+P2(f1(x261),f1(f5(f5(f5(x261)))))+~P2(f1(x262),f1(f5(f5(f5(x262)))))+~P2(a2,f1(f5(f5(f5(x261)))))+~P2(a2,f1(f5(f5(f5(x262)))))+P2(f1(x262),f1(f5(f5(f5(f5(x262))))))+~P2(a2,f1(f5(f5(f5(f5(x262))))))
% 58.82/58.84 [27]~P3(f5(x271),f5(x272))+~P2(f1(x271),f1(f5(x271)))+~P2(a2,f1(x271))+~P2(f1(x272),f1(f5(x272)))+~P2(a2,f1(x272))+~P2(a2,f1(f5(x272)))+~P2(a2,f1(f5(x271)))+~P2(f1(x271),f1(f5(f5(x271))))+~P2(f1(x272),f1(f5(f5(x272))))+~P2(a2,f1(f5(f5(x272))))+~P2(a2,f1(f5(f5(x271))))+P2(f1(x271),f1(f5(f5(f5(x271)))))+~P2(f1(x272),f1(f5(f5(f5(x272)))))+~P2(a2,f1(f5(f5(f5(x272)))))+~P2(a2,f1(f5(f5(f5(x271)))))+P2(f1(x272),f1(f5(f5(f5(f5(x272))))))+~P2(a2,f1(f5(f5(f5(f5(x272))))))
% 58.82/58.84 [34]~P3(f5(x342),f5(x341))+~P2(f1(x341),f1(f5(x341)))+~P2(a2,f1(x341))+~P2(f1(x342),f1(f5(x342)))+~P2(a2,f1(x342))+~P2(a2,f1(f5(x341)))+~P2(a2,f1(f5(x342)))+~P2(f1(x341),f1(f5(f5(x341))))+~P2(f1(x342),f1(f5(f5(x342))))+~P2(a2,f1(f5(f5(x342))))+~P2(a2,f1(f5(f5(x341))))+P2(f1(x341),f1(f5(f5(f5(x341)))))+~P2(f1(x342),f1(f5(f5(f5(x342)))))+~P2(a2,f1(f5(f5(f5(x341)))))+~P2(a2,f1(f5(f5(f5(x342)))))+~P2(f1(x342),f1(f5(f5(f5(f5(x342))))))+~P2(a2,f1(f5(f5(f5(f5(x342))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x342)))))))
% 58.82/58.84 [35]~P3(f5(x351),f5(x352))+~P2(f1(x351),f1(f5(x351)))+~P2(a2,f1(x351))+~P2(f1(x352),f1(f5(x352)))+~P2(a2,f1(x352))+~P2(a2,f1(f5(x352)))+~P2(a2,f1(f5(x351)))+~P2(f1(x351),f1(f5(f5(x351))))+~P2(f1(x352),f1(f5(f5(x352))))+~P2(a2,f1(f5(f5(x351))))+~P2(a2,f1(f5(f5(x352))))+P2(f1(x351),f1(f5(f5(f5(x351)))))+~P2(f1(x352),f1(f5(f5(f5(x352)))))+~P2(a2,f1(f5(f5(f5(x352)))))+~P2(a2,f1(f5(f5(f5(x351)))))+~P2(f1(x352),f1(f5(f5(f5(f5(x352))))))+~P2(a2,f1(f5(f5(f5(f5(x352))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x352)))))))
% 58.82/58.84 [33]~P3(f5(x332),f5(x331))+~P2(f1(x331),f1(f5(x331)))+~P2(a2,f1(x331))+~P2(f1(x332),f1(f5(x332)))+~P2(a2,f1(x332))+~P2(a2,f1(f5(x331)))+~P2(a2,f1(f5(x332)))+~P2(f1(x331),f1(f5(f5(x331))))+~P2(f1(x332),f1(f5(f5(x332))))+~P2(a2,f1(f5(f5(x331))))+~P2(a2,f1(f5(f5(x332))))+~P2(f1(x331),f1(f5(f5(f5(x331)))))+~P2(f1(x332),f1(f5(f5(f5(x332)))))+~P2(a2,f1(f5(f5(f5(x331)))))+~P2(a2,f1(f5(f5(f5(x332)))))+P2(f1(x331),f1(f5(f5(f5(f5(x331))))))+P2(f1(x332),f1(f5(f5(f5(f5(x332))))))+~P2(a2,f1(f5(f5(f5(f5(x331))))))+~P2(a2,f1(f5(f5(f5(f5(x332))))))
% 58.82/58.84 [36]~P3(f5(x362),f5(x361))+~P2(f1(x361),f1(f5(x361)))+~P2(a2,f1(x361))+~P2(f1(x362),f1(f5(x362)))+~P2(a2,f1(x362))+~P2(a2,f1(f5(x361)))+~P2(a2,f1(f5(x362)))+~P2(f1(x361),f1(f5(f5(x361))))+~P2(f1(x362),f1(f5(f5(x362))))+~P2(a2,f1(f5(f5(x361))))+~P2(a2,f1(f5(f5(x362))))+~P2(f1(x361),f1(f5(f5(f5(x361)))))+~P2(f1(x362),f1(f5(f5(f5(x362)))))+~P2(a2,f1(f5(f5(f5(x361)))))+~P2(a2,f1(f5(f5(f5(x362)))))+P2(f1(x361),f1(f5(f5(f5(f5(x361))))))+~P2(f1(x362),f1(f5(f5(f5(f5(x362))))))+~P2(a2,f1(f5(f5(f5(f5(x361))))))+~P2(a2,f1(f5(f5(f5(f5(x362))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x362)))))))
% 58.82/58.84 [37]~P3(f5(x371),f5(x372))+~P2(f1(x371),f1(f5(x371)))+~P2(a2,f1(x371))+~P2(f1(x372),f1(f5(x372)))+~P2(a2,f1(x372))+~P2(a2,f1(f5(x372)))+~P2(a2,f1(f5(x371)))+~P2(f1(x371),f1(f5(f5(x371))))+~P2(f1(x372),f1(f5(f5(x372))))+~P2(a2,f1(f5(f5(x371))))+~P2(a2,f1(f5(f5(x372))))+~P2(f1(x371),f1(f5(f5(f5(x371)))))+~P2(f1(x372),f1(f5(f5(f5(x372)))))+~P2(a2,f1(f5(f5(f5(x372)))))+~P2(a2,f1(f5(f5(f5(x371)))))+P2(f1(x371),f1(f5(f5(f5(f5(x371))))))+~P2(f1(x372),f1(f5(f5(f5(f5(x372))))))+~P2(a2,f1(f5(f5(f5(f5(x372))))))+~P2(a2,f1(f5(f5(f5(f5(x371))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x372)))))))
% 58.82/58.84 [38]~P3(f5(x382),f5(x381))+~P2(f1(x381),f1(f5(x381)))+~P2(f1(x382),f1(f5(x382)))+~P2(a2,f1(x381))+~P2(a2,f1(x382))+~P2(a2,f1(f5(x381)))+~P2(a2,f1(f5(x382)))+~P2(f1(x381),f1(f5(f5(x381))))+~P2(f1(x382),f1(f5(f5(x382))))+~P2(a2,f1(f5(f5(x382))))+~P2(a2,f1(f5(f5(x381))))+~P2(f1(x381),f1(f5(f5(f5(x381)))))+~P2(f1(x382),f1(f5(f5(f5(x382)))))+~P2(a2,f1(f5(f5(f5(x381)))))+~P2(a2,f1(f5(f5(f5(x382)))))+~P2(f1(x381),f1(f5(f5(f5(f5(x381))))))+~P2(f1(x382),f1(f5(f5(f5(f5(x382))))))+~P2(a2,f1(f5(f5(f5(f5(x381))))))+~P2(a2,f1(f5(f5(f5(f5(x382))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x381)))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x382)))))))
% 58.82/58.84 %EqnAxiom
% 58.82/58.84
% 58.82/58.84 %-------------------------------------------
% 58.82/58.84 cnf(40,plain,
% 58.82/58.84 (~P2(a2,f1(x401))+P2(f1(x401),f1(f5(x401)))+~P2(a2,f1(f5(x401)))),
% 58.82/58.84 inference(scs_inference,[],[7,5])).
% 58.82/58.84 cnf(41,plain,
% 58.82/58.84 (P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(a4))),
% 58.82/58.84 inference(scs_inference,[],[1,2,40,4])).
% 58.82/58.84 cnf(42,plain,
% 58.82/58.84 (P2(f1(a4),f1(f5(a4)))),
% 58.82/58.84 inference(scs_inference,[],[2,1,41,3])).
% 58.82/58.84 cnf(43,plain,
% 58.82/58.84 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(a2,f1(f5(f5(a4))))),
% 58.82/58.84 inference(scs_inference,[],[1,2,40,4])).
% 58.82/58.84 cnf(44,plain,
% 58.82/58.84 (P2(f1(f5(a4)),f1(f5(f5(a4))))),
% 58.82/58.84 inference(scs_inference,[],[1,2,43,6])).
% 58.82/58.84 cnf(2892,plain,
% 58.82/58.84 (P2(a2,f1(a4))),
% 58.82/58.84 inference(scs_inference,[],[2,1,3])).
% 58.82/58.84 cnf(2893,plain,
% 58.82/58.84 (P1(f1(x28931),f3(a2))),
% 58.82/58.84 inference(rename_variables,[],[1])).
% 58.82/58.84 cnf(2895,plain,
% 58.82/58.84 (P2(a2,f1(f5(a4)))),
% 58.82/58.84 inference(scs_inference,[],[2,1,2893,3,4])).
% 58.82/58.84 cnf(2896,plain,
% 58.82/58.84 (P1(f1(x28961),f3(a2))),
% 58.82/58.84 inference(rename_variables,[],[1])).
% 58.82/58.84 cnf(2898,plain,
% 58.82/58.84 (P2(a2,f1(f5(f5(a4))))),
% 58.82/58.84 inference(scs_inference,[],[2,1,2893,2896,3,4,6])).
% 58.82/58.84 cnf(2899,plain,
% 58.82/58.84 (P1(f1(x28991),f3(a2))),
% 58.82/58.84 inference(rename_variables,[],[1])).
% 58.82/58.84 cnf(2901,plain,
% 58.82/58.84 (P2(a2,f1(f5(f5(f5(a4)))))),
% 58.82/58.84 inference(scs_inference,[],[2,1,2893,2896,2899,3,4,6,8])).
% 58.82/58.84 cnf(2902,plain,
% 58.82/58.84 (P1(f1(x29021),f3(a2))),
% 58.82/58.84 inference(rename_variables,[],[1])).
% 58.82/58.84 cnf(2904,plain,
% 58.82/58.84 (P2(a2,f1(f5(f5(f5(f5(a4))))))),
% 58.82/58.84 inference(scs_inference,[],[2,1,2893,2896,2899,2902,3,4,6,8,12])).
% 58.82/58.84 cnf(2905,plain,
% 58.82/58.84 (P1(f1(x29051),f3(a2))),
% 58.82/58.84 inference(rename_variables,[],[1])).
% 58.82/58.84 cnf(2907,plain,
% 58.82/58.84 (P2(a2,f1(f5(f5(f5(f5(f5(a4)))))))),
% 58.82/58.84 inference(scs_inference,[],[2,1,2893,2896,2899,2902,2905,3,4,6,8,12,19])).
% 58.82/58.84 cnf(2914,plain,
% 58.82/58.84 (P2(f1(a4),f1(f5(f5(a4))))),
% 58.82/58.84 inference(scs_inference,[],[2,42,1,2893,2896,2899,2902,2905,3,4,6,8,12,19,9,40,13])).
% 58.82/58.84 cnf(2917,plain,
% 58.82/58.84 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 58.82/58.84 inference(scs_inference,[],[2892,2895,2914,2898,2901,42,14])).
% 58.82/58.84 cnf(2920,plain,
% 58.82/58.84 (P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 58.82/58.84 inference(scs_inference,[],[2914,2895,2892,42,2898,2901,2917,21])).
% 58.82/58.84 cnf(2923,plain,
% 58.82/58.84 (P2(f1(f5(a4)),f1(f5(f5(f5(a4)))))),
% 58.82/58.84 inference(scs_inference,[],[44,2895,2898,2901,9,13])).
% 58.82/58.84 cnf(2929,plain,
% 58.82/58.84 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(f5(f5(a4))))))),
% 58.82/58.84 inference(scs_inference,[],[2923,2920,2914,44,2904,2892,42,2895,2898,2901,14,20])).
% 58.82/58.84 cnf(2937,plain,
% 58.82/58.84 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(f5(f5(f5(a4))))))),
% 58.82/58.84 inference(scs_inference,[],[2920,2914,2907,2892,42,2904,2895,2901,2898,28])).
% 58.82/58.84 cnf(2944,plain,
% 58.82/58.84 (P2(f1(a4),f1(f5(f5(f5(f5(a4))))))),
% 58.82/58.84 inference(scs_inference,[],[2920,2914,2892,42,2904,2895,2901,2898,33,2929])).
% 58.82/58.84 cnf(2947,plain,
% 58.82/58.84 (P3(f5(a4),f5(a4))),
% 58.82/58.84 inference(scs_inference,[],[2944,2937])).
% 58.82/58.84 cnf(2950,plain,
% 58.82/58.84 (~P3(f5(a4),f5(a4))),
% 58.82/58.84 inference(scs_inference,[],[2944,2923,2907,2920,44,2914,2892,42,2904,2895,2901,2898,34,38])).
% 58.82/58.84 cnf(2953,plain,
% 58.82/58.84 ($false),
% 58.82/58.84 inference(scs_inference,[],[2947,2950]),
% 58.82/58.84 ['proof']).
% 58.82/58.84 % SZS output end Proof
% 58.82/58.84 % Total time :58.120000s
%------------------------------------------------------------------------------