%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYO648-1 : TPTP v8.2.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 20:27:38 EDT 2024
% Result : Unsatisfiable 58.40s 58.55s
% Output : CNFRefutation 58.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.09 % Problem : SYO648-1 : TPTP v8.2.0. Released v7.3.0.
% 0.03/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Sun Jun 23 08:43:23 EDT 2024
% 0.09/0.28 % CPUTime :
% 0.14/0.47 start to proof:theBenchmark
% 58.40/58.54 %-------------------------------------------
% 58.40/58.54 % File :CSE---1.7
% 58.40/58.54 % Problem :theBenchmark
% 58.40/58.54 % Transform :cnf
% 58.40/58.54 % Format :tptp:raw
% 58.40/58.54 % Command :java -jar mcs_scs.jar %d %s
% 58.40/58.54
% 58.40/58.54 % Result :Theorem 58.000000s
% 58.40/58.54 % Output :CNFRefutation 58.000000s
% 58.40/58.54 %-------------------------------------------
% 58.40/58.54 %------------------------------------------------------------------------------
% 58.40/58.54 % File : SYO648-1 : TPTP v8.2.0. Released v7.3.0.
% 58.40/58.54 % Domain : Syntactic
% 58.40/58.54 % Problem : GSM_1_1_4
% 58.40/58.54 % Version : Especial.
% 58.40/58.54 % English :
% 58.40/58.54
% 58.40/58.54 % Refs : [EH+16] Ebner et al. (2016), System Description: GAPT 2.0
% 58.40/58.54 % : [Cer18] Cerna (2018), Email to Geoff Sutcliffe
% 58.40/58.54 % Source : [Cer18]
% 58.40/58.54 % Names : GSM_1_1_4 [Cer18]
% 58.40/58.54
% 58.40/58.54 % Status : Unsatisfiable
% 58.40/58.54 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.3.0
% 58.40/58.54 % Syntax : Number of clauses : 27 ( 2 unt; 17 nHn; 26 RR)
% 58.40/58.54 % Number of literals : 244 ( 0 equ; 202 neg)
% 58.40/58.54 % Maximal clause size : 17 ( 9 avg)
% 58.40/58.54 % Maximal term depth : 6 ( 2 avg)
% 58.40/58.54 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty)
% 58.40/58.54 % Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% 58.40/58.54 % Number of variables : 42 ( 1 sgn)
% 58.40/58.54 % SPC : CNF_UNS_RFO_NEQ_NHN
% 58.40/58.54
% 58.40/58.54 % Comments : Created using the GAPT system - https://github.com/gapt/gapt/blob/
% 58.40/58.54 % master/examples/schema/GradedStrictMonotoneSequenceSchema.scala
% 58.40/58.54 %------------------------------------------------------------------------------
% 58.40/58.54 cnf(clause_113,axiom,
% 58.40/58.54 ( ~ 'E'('0',f(suc(A_1)))
% 58.40/58.54 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.54 | ~ 'E'('0',f(A_1))
% 58.40/58.54 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.54 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.54 | ~ 'E'('0',f(B_2))
% 58.40/58.54 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.54 | 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.54 | 'E'(f(B_2),f(suc(B_2))) ) ).
% 58.40/58.54
% 58.40/58.54 cnf(clause_260,axiom,
% 58.40/58.54 ( ~ 'LE'(f(suc(suc(suc(B_1)))),s('0'))
% 58.40/58.54 | 'E'('0',f(suc(suc(suc(B_1)))))
% 58.40/58.54 | 'LE'(f(B_1),'0') ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_48,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_79,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | 'E'(f(B_2),f(suc(suc(B_2)))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_90,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.40/58.55 | 'E'(f(B_2),f(suc(suc(suc(B_2))))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_326,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.40/58.55 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_203,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.40/58.55 | 'E'(f(B_2),f(suc(suc(suc(B_2))))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_299,axiom,
% 58.40/58.55 'LE'(f(A),s('0')) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_157,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.40/58.55 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_328,axiom,
% 58.40/58.55 ( ~ 'LE'(f(suc(B_1)),s('0'))
% 58.40/58.55 | 'E'('0',f(suc(B_1)))
% 58.40/58.55 | 'LE'(f(B_1),'0') ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_217,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | 'E'(f(B_2),f(suc(suc(suc(B_2))))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_44,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.40/58.55 | 'E'(f(B_2),f(suc(B_2))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_72,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.40/58.55 | 'E'(f(B_2),f(suc(B_2))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_168,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | 'E'(f(B_2),f(suc(B_2))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_231,axiom,
% 58.40/58.55 ( ~ 'LE'(f(suc(suc(suc(suc(B_1))))),s('0'))
% 58.40/58.55 | 'E'('0',f(suc(suc(suc(suc(B_1))))))
% 58.40/58.55 | 'LE'(f(B_1),'0') ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_46,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | 'E'(f(A_1),f(suc(A_1))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_278,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | 'E'(f(A_1),f(suc(suc(A_1)))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_254,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | iLEQ(suc(A_1),suc(A_1)) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_114,axiom,
% 58.40/58.55 ( ~ 'LE'(f(suc(suc(B_1))),s('0'))
% 58.40/58.55 | 'E'('0',f(suc(suc(B_1))))
% 58.40/58.55 | 'LE'(f(B_1),'0') ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_223,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | 'E'(f(B_2),f(suc(suc(suc(B_2))))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_160,axiom,
% 58.40/58.55 ~ 'LE'(f(z),'0') ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_277,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))
% 58.40/58.55 | 'E'(f(B_2),f(suc(suc(B_2)))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_29,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | 'E'(f(B_2),f(suc(suc(B_2)))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_145,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(suc(A_1)))))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_221,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | 'E'(f(A_1),f(suc(suc(suc(A_1)))))
% 58.40/58.55 | 'E'(f(B_2),f(suc(suc(B_2)))) ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_62,axiom,
% 58.40/58.55 ( ~ 'LE'(f(B_1),s('0'))
% 58.40/58.55 | 'E'('0',f(B_1))
% 58.40/58.55 | 'LE'(f(B_1),'0') ) ).
% 58.40/58.55
% 58.40/58.55 cnf(clause_237,axiom,
% 58.40/58.55 ( ~ 'E'('0',f(suc(suc(suc(A_1)))))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(B_2))))
% 58.40/58.55 | ~ 'E'('0',f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'('0',f(A_1))
% 58.40/58.55 | ~ 'E'('0',f(suc(B_2)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(suc(suc(B_2))))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(B_2)))
% 58.40/58.55 | ~ iLEQ(suc(A_1),suc(B_2))
% 58.40/58.55 | ~ 'E'('0',f(B_2))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(suc(A_1))))
% 58.40/58.55 | ~ 'E'(f(B_2),f(suc(suc(suc(B_2)))))
% 58.40/58.55 | ~ 'E'(f(A_1),f(suc(A_1)))
% 58.40/58.55 | ~ 'E'('0',f(suc(suc(B_2))))
% 58.40/58.55 | 'E'(f(A_1),f(suc(suc(suc(A_1))))) ) ).
% 58.40/58.55
% 58.40/58.55 %------------------------------------------------------------------------------
% 58.40/58.55 %-------------------------------------------
% 58.40/58.55 % Proof found
% 58.40/58.55 % SZS status Theorem for theBenchmark
% 58.40/58.55 % SZS output start Proof
% 58.40/58.55 %ClaNum:27(EqnAxiom:0)
% 58.40/58.55 %VarNum:344(SingletonVarNum:42)
% 58.40/58.55 %MaxLitNum:17
% 58.40/58.55 %MaxfuncDepth:5
% 58.40/58.55 %SharedTerms:5
% 58.40/58.55 [2]~P1(f1(a4),a2)
% 58.40/58.55 [1]P1(f1(x11),f3(a2))
% 58.40/58.55 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2)
% 58.40/58.55 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41)))
% 58.40/58.55 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61))))
% 58.40/58.55 [8]P1(f1(x81),a2)+~P1(f1(f5(f5(f5(x81)))),f3(a2))+P2(a2,f1(f5(f5(f5(x81)))))
% 58.40/58.55 [12]P1(f1(x121),a2)+~P1(f1(f5(f5(f5(f5(x121))))),f3(a2))+P2(a2,f1(f5(f5(f5(f5(x121))))))
% 58.40/58.55 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51)))
% 58.40/58.55 [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.40/58.55 [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.40/58.55 [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.40/58.55 [19]P3(f5(x191),f5(x191))+~P2(a2,f1(x191))+~P2(f1(x191),f1(f5(x191)))+~P2(f1(x191),f1(f5(f5(x191))))+~P2(a2,f1(f5(x191)))+~P2(f1(x191),f1(f5(f5(f5(x191)))))+~P2(a2,f1(f5(f5(x191))))+~P2(a2,f1(f5(f5(f5(x191)))))+~P2(a2,f1(f5(f5(f5(f5(x191))))))
% 58.40/58.55 [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.40/58.55 [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.40/58.55 [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.40/58.55 [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.40/58.55 [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.40/58.55 [20]~P3(f5(x201),f5(x202))+P2(f1(x201),f1(f5(x201)))+~P2(a2,f1(x201))+~P2(f1(x202),f1(f5(x202)))+~P2(a2,f1(x202))+~P2(a2,f1(f5(x201)))+~P2(a2,f1(f5(x202)))+~P2(f1(x202),f1(f5(f5(x202))))+~P2(a2,f1(f5(f5(x202))))+~P2(f1(x202),f1(f5(f5(f5(x202)))))+~P2(a2,f1(f5(f5(f5(x202)))))+~P2(a2,f1(f5(f5(f5(f5(x202))))))
% 58.40/58.55 [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(x212),f1(f5(f5(x212))))+~P2(a2,f1(f5(f5(x212))))+~P2(f1(x212),f1(f5(f5(f5(x212)))))+~P2(a2,f1(f5(f5(f5(x212)))))+~P2(a2,f1(f5(f5(f5(f5(x212))))))
% 58.40/58.55 [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.40/58.55 [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.40/58.55 [23]~P3(f5(x231),f5(x232))+~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(x231),f1(f5(f5(x231))))+~P2(f1(x232),f1(f5(f5(x232))))+~P2(a2,f1(f5(f5(x231))))+~P2(a2,f1(f5(f5(x232))))+~P2(f1(x232),f1(f5(f5(f5(x232)))))+~P2(a2,f1(f5(f5(f5(x232)))))+~P2(a2,f1(f5(f5(f5(f5(x232))))))
% 58.40/58.55 [24]~P3(f5(x242),f5(x241))+~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(a2,f1(f5(f5(f5(f5(x242))))))
% 58.40/58.55 [22]~P3(f5(x222),f5(x221))+~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(x221),f1(f5(f5(x221))))+~P2(f1(x222),f1(f5(f5(x222))))+~P2(a2,f1(f5(f5(x221))))+~P2(a2,f1(f5(f5(x222))))+P2(f1(x221),f1(f5(f5(f5(x221)))))+P2(f1(x222),f1(f5(f5(f5(x222)))))+~P2(a2,f1(f5(f5(f5(x221)))))+~P2(a2,f1(f5(f5(f5(x222)))))
% 58.40/58.56 [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(x251),f1(f5(f5(f5(x251)))))+~P2(f1(x252),f1(f5(f5(f5(x252)))))+~P2(a2,f1(f5(f5(f5(x251)))))+~P2(a2,f1(f5(f5(f5(x252)))))+~P2(a2,f1(f5(f5(f5(f5(x252))))))
% 58.40/58.56 [26]~P3(f5(x261),f5(x262))+~P2(f1(x261),f1(f5(x261)))+~P2(a2,f1(x261))+~P2(f1(x262),f1(f5(x262)))+~P2(a2,f1(x262))+~P2(a2,f1(f5(x262)))+~P2(a2,f1(f5(x261)))+~P2(f1(x261),f1(f5(f5(x261))))+~P2(f1(x262),f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(x261))))+P2(f1(x261),f1(f5(f5(f5(x261)))))+~P2(f1(x262),f1(f5(f5(f5(x262)))))+~P2(a2,f1(f5(f5(f5(x262)))))+~P2(a2,f1(f5(f5(f5(x261)))))+~P2(a2,f1(f5(f5(f5(f5(x262))))))
% 58.40/58.56 [27]~P3(f5(x272),f5(x271))+~P2(f1(x271),f1(f5(x271)))+~P2(f1(x272),f1(f5(x272)))+~P2(a2,f1(x271))+~P2(a2,f1(x272))+~P2(a2,f1(f5(x271)))+~P2(a2,f1(f5(x272)))+~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(x271)))))+~P2(a2,f1(f5(f5(f5(x272)))))+~P2(a2,f1(f5(f5(f5(f5(x271))))))+~P2(a2,f1(f5(f5(f5(f5(x272))))))
% 58.40/58.56 %EqnAxiom
% 58.40/58.56
% 58.40/58.56 %-------------------------------------------
% 58.40/58.56 cnf(29,plain,
% 58.40/58.56 (~P2(a2,f1(x291))+P2(f1(x291),f1(f5(x291)))+~P2(a2,f1(f5(x291)))),
% 58.40/58.56 inference(scs_inference,[],[7,5])).
% 58.40/58.56 cnf(30,plain,
% 58.40/58.56 (P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(a4))),
% 58.40/58.56 inference(scs_inference,[],[1,2,29,4])).
% 58.40/58.56 cnf(31,plain,
% 58.40/58.56 (P2(f1(a4),f1(f5(a4)))),
% 58.40/58.56 inference(scs_inference,[],[2,1,30,3])).
% 58.40/58.56 cnf(32,plain,
% 58.40/58.56 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(a2,f1(f5(f5(a4))))),
% 58.40/58.56 inference(scs_inference,[],[1,2,29,4])).
% 58.40/58.56 cnf(33,plain,
% 58.40/58.56 (P2(f1(f5(a4)),f1(f5(f5(a4))))),
% 58.40/58.56 inference(scs_inference,[],[1,2,32,6])).
% 58.40/58.56 cnf(3326,plain,
% 58.40/58.56 (P2(a2,f1(a4))),
% 58.40/58.56 inference(scs_inference,[],[1,2,3])).
% 58.40/58.56 cnf(3329,plain,
% 58.40/58.56 (P2(f1(a4),f1(f5(f5(a4))))+~P2(a2,f1(f5(a4)))+~P2(a2,f1(f5(f5(a4))))),
% 58.40/58.56 inference(scs_inference,[],[3326,31,9,13])).
% 58.40/58.56 cnf(3330,plain,
% 58.40/58.56 (~P2(a2,f1(f5(f5(a4))))+P2(f1(a4),f1(f5(f5(a4))))),
% 58.40/58.56 inference(scs_inference,[],[1,2,3329,4])).
% 58.40/58.56 cnf(3331,plain,
% 58.40/58.56 (P2(f1(a4),f1(f5(f5(a4))))),
% 58.40/58.56 inference(scs_inference,[],[1,2,3330,6])).
% 58.40/58.56 cnf(3368,plain,
% 58.40/58.56 (P2(a2,f1(f5(a4)))),
% 58.40/58.56 inference(scs_inference,[],[1,2,4])).
% 58.40/58.56 cnf(3369,plain,
% 58.40/58.56 (P1(f1(x33691),f3(a2))),
% 58.40/58.56 inference(rename_variables,[],[1])).
% 58.40/58.56 cnf(3371,plain,
% 58.40/58.56 (P2(a2,f1(f5(f5(a4))))),
% 58.40/58.56 inference(scs_inference,[],[1,3369,2,4,6])).
% 58.40/58.56 cnf(3372,plain,
% 58.40/58.56 (P1(f1(x33721),f3(a2))),
% 58.40/58.56 inference(rename_variables,[],[1])).
% 58.40/58.56 cnf(3374,plain,
% 58.40/58.56 (P2(a2,f1(f5(f5(f5(a4)))))),
% 58.40/58.56 inference(scs_inference,[],[1,3369,3372,2,4,6,8])).
% 58.40/58.56 cnf(3375,plain,
% 58.40/58.56 (P1(f1(x33751),f3(a2))),
% 58.40/58.56 inference(rename_variables,[],[1])).
% 58.40/58.56 cnf(3377,plain,
% 58.40/58.56 (P2(a2,f1(f5(f5(f5(f5(a4))))))),
% 58.40/58.56 inference(scs_inference,[],[1,3369,3372,3375,2,4,6,8,12])).
% 58.40/58.56 cnf(3384,plain,
% 58.40/58.56 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 58.40/58.56 inference(scs_inference,[],[1,3369,3372,3375,3331,33,3326,31,2,4,6,8,12,9,29,14])).
% 58.40/58.56 cnf(3386,plain,
% 58.40/58.56 (P2(f1(a4),f1(f5(f5(f5(a4)))))),
% 58.40/58.56 inference(scs_inference,[],[3371,3331,3368,3326,31,3374,3384,22])).
% 58.40/58.56 cnf(3389,plain,
% 58.40/58.56 ($false),
% 58.40/58.56 inference(scs_inference,[],[3386,3377,3368,3371,3374,3331,31,3326,19,27]),
% 58.40/58.56 ['proof']).
% 58.40/58.56 % SZS output end Proof
% 58.40/58.56 % Total time :58.000000s
%------------------------------------------------------------------------------