%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO634-1 : TPTP v9.0.0. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n025.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 : Fri Jul 25 09:59:06 PM UTC 2025
% Result : Unsatisfiable 0.18s 0.37s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO634-1 : TPTP v9.0.0. Released v7.1.0.
% 0.03/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jul 22 20:02:49 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.35 % launching worker at depth: 10
% 0.12/0.35 % launching worker at depth: 11
% 0.18/0.37 % SZS status Theorem for theBenchmark
% 0.18/0.37 % SZS output start CNFRefutation
% 0.18/0.37 cnf(2, plain, 'E'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))), inference(cnf, [status(esa)], [clause_11_03])).
% 0.18/0.37 cnf(l0, plain, 'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))), inference(instantiation, [status(thm)], [2])).
% 0.18/0.37 cnf(11, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1),s(s(s(s(s('0')))))) | ~'E'(f(X2),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X3),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X4),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X5),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6)),s(s(s(s('0'))))), inference(cnf, [status(esa)], [clause_9_12])).
% 0.18/0.37 cnf(l1, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_15),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))), inference(instantiation, [status(thm)], [11])).
% 0.18/0.37 cnf(5, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X2),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X3),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1),s(s(s(s(s(s('0'))))))), inference(cnf, [status(esa)], [clause_1_06])).
% 0.18/0.37 cnf(l3, plain, ~'E'(f(X0_54),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.37 cnf(0, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1),s(s(s(s(s(s(s(s('0'))))))))), inference(cnf, [status(esa)], [clause_21_01])).
% 0.18/0.37 cnf(l11, plain, ~'E'(f(X0_22),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.37 cnf(l12, plain, ~'E'(f(X0_30),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.37 cnf(13, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X2),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1),s(s(s(s(s(s(s('0')))))))), inference(cnf, [status(esa)], [clause_12_14])).
% 0.18/0.37 cnf(l13, plain, ~'E'(f(X0_39),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.37 cnf(l14, plain, ~'E'(f(X0_16),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.37 cnf(8, plain, 'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))), inference(cnf, [status(esa)], [clause_17_09])).
% 0.18/0.37 cnf(l15, plain, 'E'(f(X0_15),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.37 cnf(14, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1),s(s(s(s(s('0')))))) | ~'E'(f(X2),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X3),s(s(s(s('0'))))) | ~'E'(f(X4),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X5),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X6),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7)),s(s(s('0')))), inference(cnf, [status(esa)], [clause_18_15])).
% 0.18/0.37 cnf(l6, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_65),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7_6)),s(s(s('0')))), inference(instantiation, [status(thm)], [14])).
% 0.18/0.37 cnf(l16, plain, 'E'(f(X0_16),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.37 cnf(l17, plain, ~'E'(f(X0_18),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.37 cnf(l18, plain, 'E'(f(X0_18),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.37 cnf(l19, plain, ~'E'(f(X0_29),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.37 cnf(l20, plain, ~'E'(f(X0_28),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l54, plain, 'E'(f(X0_54),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l26, plain, ~'E'(f(X0_55),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l30, plain, 'E'(f(X0_30),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(19, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X2),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X3),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X4),s(s(s(s(s(s('0'))))))) | 'E'(f(X1),s(s(s(s(s('0')))))), inference(cnf, [status(esa)], [clause_15_20])).
% 0.18/0.38 cnf(l47, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_48),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l65, plain, 'E'(f(X0_65),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l48, plain, 'E'(f(X0_48),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l4, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_70),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l29, plain, 'E'(f(X0_29),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l2, plain, ~'E'(f(X0_5),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l53, plain, ~'E'(f(X0_58),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l70, plain, 'E'(f(X0_70),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l55, plain, 'E'(f(X0_55),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l22, plain, 'E'(f(X0_22),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l42, plain, ~'E'(f(X0_64),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l39, plain, 'E'(f(X0_39),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l31, plain, ~'E'(f(X0_33),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l36, plain, ~'E'(f(X0_86),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l34, plain, ~'E'(f(X0_74),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l71, plain, ~'E'(f(X0_72),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l58, plain, 'E'(f(X0_58),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l72, plain, 'E'(f(X0_72),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(16, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1),s(s(s(s(s('0')))))) | ~'E'(f(X2),s('0')) | ~'E'(f(X3),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X4),s(s(s(s('0'))))) | ~'E'(f(X5),s(s('0'))) | ~'E'(f(X6),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X7),s(s(s('0')))) | ~'E'(f(X8),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X9),s(s(s(s(s(s('0'))))))) | ~'E'(f(X10),'0'), inference(cnf, [status(esa)], [clause_3_17])).
% 0.18/0.38 cnf(l21, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X9_73)),s('0')) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8_67)),s(s('0'))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7_6)),s(s(s('0')))) | ~'E'(f(X0_92),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X10_77)),'0'), inference(instantiation, [status(thm)], [16])).
% 0.18/0.38 cnf(18, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1),s(s(s(s(s('0')))))) | ~'E'(f(X2),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X3),s(s(s(s('0'))))) | ~'E'(f(X4),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X5),s(s(s('0')))) | ~'E'(f(X6),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X7),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8)),s(s('0'))), inference(cnf, [status(esa)], [clause_0_19])).
% 0.18/0.38 cnf(l67, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7_6)),s(s(s('0')))) | ~'E'(f(X0_75),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8_67)),s(s('0'))), inference(instantiation, [status(thm)], [18])).
% 0.18/0.38 cnf(10, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1),s(s(s(s(s('0')))))) | ~'E'(f(X2),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X3),s(s(s(s('0'))))) | ~'E'(f(X4),s(s('0'))) | ~'E'(f(X5),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X6),s(s(s('0')))) | ~'E'(f(X7),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X8),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X9)),s('0')), inference(cnf, [status(esa)], [clause_8_11])).
% 0.18/0.38 cnf(l73, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8_76)),s(s('0'))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7_6)),s(s(s('0')))) | ~'E'(f(X0_102),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X9_73)),s('0')), inference(instantiation, [status(thm)], [10])).
% 0.18/0.38 cnf(l5, plain, 'E'(f(X0_5),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l46, plain, ~'E'(f(X0_60),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l74, plain, 'E'(f(X0_74),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l75, plain, 'E'(f(X0_75),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l37, plain, ~'E'(f(X0_61),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l76, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7_6)),s(s(s('0')))) | ~'E'(f(X0_84),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8_76)),s(s('0'))), inference(instantiation, [status(thm)], [18])).
% 0.18/0.38 cnf(21, plain, ~'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1),s(s(s(s(s('0')))))) | ~'E'(f(X2),s('0')) | ~'E'(f(X3),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X4),s(s(s(s('0'))))) | ~'E'(f(X5),s(s('0'))) | ~'E'(f(X6),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X7),s(s(s('0')))) | ~'E'(f(X8),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X9),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X10)),'0'), inference(cnf, [status(esa)], [clause_10_22])).
% 0.18/0.38 cnf(l77, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X9_90)),s('0')) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8_265)),s(s('0'))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7_6)),s(s(s('0')))) | ~'E'(f(X0_83),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X10_77)),'0'), inference(instantiation, [status(thm)], [21])).
% 0.18/0.38 cnf(l78, plain, ~'E'(f(X0_134),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l79, plain, ~'E'(f(X0_186),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l80, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_101),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l81, plain, ~'E'(f(X0_141),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l82, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_111),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l83, plain, 'E'(f(X0_83),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l84, plain, 'E'(f(X0_84),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l85, plain, ~'E'(f(X0_96),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l86, plain, 'E'(f(X0_86),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l27, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_52),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l87, plain, ~'E'(f(X0_120),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l88, plain, ~'E'(f(X0_94),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l89, plain, ~'E'(f(X0_208),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l25, plain, ~'E'(f(X0_44),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l28, plain, 'E'(f(X0_28),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l90, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8_165)),s(s('0'))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7_6)),s(s(s('0')))) | ~'E'(f(X0_144),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X9_90)),s('0')), inference(instantiation, [status(thm)], [10])).
% 0.18/0.38 cnf(l91, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_128),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l92, plain, 'E'(f(X0_92),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l93, plain, ~'E'(f(X0_148),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l94, plain, 'E'(f(X0_94),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l69, plain, ~'E'(f(X0_174),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l95, plain, ~'E'(f(X0_108),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l96, plain, 'E'(f(X0_96),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l97, plain, ~'E'(f(X0_147),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l98, plain, ~'E'(f(X0_119),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l41, plain, ~'E'(f(X0_43),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l99, plain, ~'E'(f(X0_129),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l100, plain, ~'E'(f(X0_105),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l101, plain, 'E'(f(X0_101),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l102, plain, 'E'(f(X0_102),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l103, plain, ~'E'(f(X0_172),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l104, plain, ~'E'(f(X0_234),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l33, plain, 'E'(f(X0_33),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l105, plain, 'E'(f(X0_105),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l106, plain, ~'E'(f(X0_118),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l107, plain, ~'E'(f(X0_126),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l108, plain, 'E'(f(X0_108),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l109, plain, ~'E'(f(X0_125),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l110, plain, ~'E'(f(X0_127),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l111, plain, 'E'(f(X0_111),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l112, plain, ~'E'(f(X0_190),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l113, plain, ~'E'(f(X0_310),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l114, plain, ~'E'(f(X0_152),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l115, plain, ~'E'(f(X0_121),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l116, plain, ~'E'(f(X0_201),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l117, plain, ~'E'(f(X0_160),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l118, plain, 'E'(f(X0_118),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l119, plain, 'E'(f(X0_119),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l120, plain, 'E'(f(X0_120),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l121, plain, 'E'(f(X0_121),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l122, plain, ~'E'(f(X0_231),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l123, plain, ~'E'(f(X0_132),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l60, plain, 'E'(f(X0_60),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l64, plain, 'E'(f(X0_64),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l124, plain, ~'E'(f(X0_295),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l56, plain, ~'E'(f(X0_153),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l125, plain, 'E'(f(X0_125),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l126, plain, 'E'(f(X0_126),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l127, plain, 'E'(f(X0_127),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l128, plain, 'E'(f(X0_128),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l129, plain, 'E'(f(X0_129),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l130, plain, ~'E'(f(X0_155),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l131, plain, ~'E'(f(X0_142),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l61, plain, 'E'(f(X0_61),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l132, plain, 'E'(f(X0_132),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l44, plain, 'E'(f(X0_44),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l133, plain, ~'E'(f(X0_136),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l134, plain, 'E'(f(X0_134),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l135, plain, ~'E'(f(X0_306),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l136, plain, 'E'(f(X0_136),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l137, plain, ~'E'(f(X0_164),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l138, plain, ~'E'(f(X0_257),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l139, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_305),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l140, plain, ~'E'(f(X0_299),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l141, plain, 'E'(f(X0_141),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l142, plain, 'E'(f(X0_142),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l143, plain, ~'E'(f(X0_221),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l144, plain, 'E'(f(X0_144),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l57, plain, ~'E'(f(X0_66),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l66, plain, 'E'(f(X0_66),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l145, plain, ~'E'(f(X0_204),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l43, plain, 'E'(f(X0_43),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l146, plain, ~'E'(f(X0_246),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l147, plain, 'E'(f(X0_147),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l148, plain, 'E'(f(X0_148),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l32, plain, ~'E'(f(X0_40),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l149, plain, ~'E'(f(X0_184),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l150, plain, ~'E'(f(X0_154),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l151, plain, ~'E'(f(X0_238),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l152, plain, 'E'(f(X0_152),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l153, plain, 'E'(f(X0_153),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l154, plain, 'E'(f(X0_154),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l155, plain, 'E'(f(X0_155),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l156, plain, ~'E'(f(X0_183),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l157, plain, ~'E'(f(X0_232),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l158, plain, ~'E'(f(X0_214),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l159, plain, ~'E'(f(X0_173),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l160, plain, 'E'(f(X0_160),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l161, plain, ~'E'(f(X0_188),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l162, plain, ~'E'(f(X0_228),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l163, plain, ~'E'(f(X0_182),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l62, plain, ~'E'(f(X0_251),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l164, plain, 'E'(f(X0_164),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l59, plain, ~'E'(f(X0_207),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l52, plain, 'E'(f(X0_52),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l165, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7_6)),s(s(s('0')))) | ~'E'(f(X0_169),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8_165)),s(s('0'))), inference(instantiation, [status(thm)], [18])).
% 0.18/0.38 cnf(l166, plain, ~'E'(f(X0_230),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l167, plain, ~'E'(f(X0_168),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l168, plain, 'E'(f(X0_168),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l169, plain, 'E'(f(X0_169),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l170, plain, ~'E'(f(X0_223),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l171, plain, ~'E'(f(X0_197),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l172, plain, 'E'(f(X0_172),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l173, plain, 'E'(f(X0_173),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l174, plain, 'E'(f(X0_174),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l35, plain, ~'E'(f(X0_50),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l175, plain, ~'E'(f(X0_179),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l176, plain, ~'E'(f(X0_199),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l177, plain, ~'E'(f(X0_180),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l178, plain, ~'E'(f(X0_215),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l179, plain, 'E'(f(X0_179),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l180, plain, 'E'(f(X0_180),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l181, plain, ~'E'(f(X0_227),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l182, plain, 'E'(f(X0_182),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l183, plain, 'E'(f(X0_183),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l184, plain, 'E'(f(X0_184),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l185, plain, ~'E'(f(X0_219),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l186, plain, 'E'(f(X0_186),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l187, plain, ~'E'(f(X0_192),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l188, plain, 'E'(f(X0_188),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l189, plain, ~'E'(f(X0_196),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l190, plain, 'E'(f(X0_190),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l191, plain, ~'E'(f(X0_216),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l63, plain, ~'E'(f(X0_194),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l192, plain, 'E'(f(X0_192),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l193, plain, ~'E'(f(X0_233),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l194, plain, 'E'(f(X0_194),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l195, plain, ~'E'(f(X0_239),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l196, plain, 'E'(f(X0_196),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l197, plain, 'E'(f(X0_197),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l198, plain, ~'E'(f(X0_202),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l199, plain, 'E'(f(X0_199),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l200, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_203),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l201, plain, 'E'(f(X0_201),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l202, plain, 'E'(f(X0_202),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l203, plain, 'E'(f(X0_203),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l204, plain, 'E'(f(X0_204),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l205, plain, ~'E'(f(X0_206),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l206, plain, 'E'(f(X0_206),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l207, plain, 'E'(f(X0_207),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l208, plain, 'E'(f(X0_208),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l209, plain, ~'E'(f(X0_222),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l210, plain, ~'E'(f(X0_236),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l211, plain, ~'E'(f(X0_291),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 % launching worker at depth: cnf(l212, plain, ~'E'(f(X0_220),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l213, plain, ~'E'(f(X0_226),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l214, plain, 'E'(f(X0_214),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l215, plain, 'E'(f(X0_215),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l216, plain, 'E'(f(X0_216),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 12
% 0.18/0.38 cnf(l217, plain, ~'E'(f(X0_224),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l218, plain, ~'E'(f(X0_248),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l219, plain, 'E'(f(X0_219),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l220, plain, 'E'(f(X0_220),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l221, plain, 'E'(f(X0_221),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l222, plain, 'E'(f(X0_222),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l223, plain, 'E'(f(X0_223),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l224, plain, 'E'(f(X0_224),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l225, plain, ~'E'(f(X0_255),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l226, plain, 'E'(f(X0_226),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l227, plain, 'E'(f(X0_227),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l228, plain, 'E'(f(X0_228),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l229, plain, ~'E'(f(X0_245),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l230, plain, 'E'(f(X0_230),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l231, plain, 'E'(f(X0_231),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l232, plain, 'E'(f(X0_232),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l233, plain, 'E'(f(X0_233),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l68, plain, ~'E'(f(X0_271),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l50, plain, 'E'(f(X0_50),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l234, plain, 'E'(f(X0_234),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l235, plain, ~'E'(f(X0_262),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l236, plain, 'E'(f(X0_236),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l237, plain, ~'E'(f(X0_279),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l238, plain, 'E'(f(X0_238),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l239, plain, 'E'(f(X0_239),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l240, plain, ~'E'(f(X0_241),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l241, plain, 'E'(f(X0_241),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l242, plain, ~'E'(f(X0_250),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l40, plain, 'E'(f(X0_40),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l243, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_293),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l244, plain, ~'E'(f(X0_247),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l245, plain, 'E'(f(X0_245),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l246, plain, 'E'(f(X0_246),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l247, plain, 'E'(f(X0_247),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l248, plain, 'E'(f(X0_248),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l249, plain, ~'E'(f(X0_259),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l250, plain, 'E'(f(X0_250),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l251, plain, 'E'(f(X0_251),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l252, plain, ~'E'(f(X0_260),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l253, plain, ~'E'(f(X0_263),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l254, plain, ~'E'(f(X0_284),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l255, plain, 'E'(f(X0_255),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l256, plain, ~'E'(f(X0_323),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l257, plain, 'E'(f(X0_257),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l258, plain, ~'E'(f(X0_296),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l259, plain, 'E'(f(X0_259),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l260, plain, 'E'(f(X0_260),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l261, plain, ~'E'(f(X0_267),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l262, plain, 'E'(f(X0_262),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l263, plain, 'E'(f(X0_263),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l264, plain, ~'E'(f(X0_272),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l265, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s('0')))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6_1)),s(s(s(s('0'))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7_6)),s(s(s('0')))) | ~'E'(f(X0_278),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8_265)),s(s('0'))), inference(instantiation, [status(thm)], [18])).
% 0.18/0.38 cnf(l266, plain, ~'E'(f(X0_277),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l267, plain, 'E'(f(X0_267),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l268, plain, ~'E'(f(X0_286),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l269, plain, ~'E'(f(X0_294),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l270, plain, ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | ~'E'(f(X0_300),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s('0'))))))) | 'E'(f(X1_329),s(s(s(s(s('0')))))), inference(instantiation, [status(thm)], [19])).
% 0.18/0.38 cnf(l271, plain, 'E'(f(X0_271),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l272, plain, 'E'(f(X0_272),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l273, plain, ~'E'(f(X0_280),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l274, plain, ~'E'(f(X0_311),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l275, plain, ~'E'(f(X0_303),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l276, plain, ~'E'(f(X0_285),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l277, plain, 'E'(f(X0_277),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l278, plain, 'E'(f(X0_278),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l279, plain, 'E'(f(X0_279),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l280, plain, 'E'(f(X0_280),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l281, plain, ~'E'(f(X0_288),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l282, plain, ~'E'(f(X0_304),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.38 cnf(l283, plain, ~'E'(f(X0_289),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.38 cnf(l284, plain, 'E'(f(X0_284),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l285, plain, 'E'(f(X0_285),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l286, plain, 'E'(f(X0_286),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l287, plain, ~'E'(f(X0_321),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.38 cnf(l288, plain, 'E'(f(X0_288),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l289, plain, 'E'(f(X0_289),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.38 cnf(l290, plain, ~'E'(f(X0_312),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.39 cnf(l291, plain, 'E'(f(X0_291),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l292, plain, ~'E'(f(X0_325),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.39 cnf(l293, plain, 'E'(f(X0_293),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l294, plain, 'E'(f(X0_294),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l295, plain, 'E'(f(X0_295),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l296, plain, 'E'(f(X0_296),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l297, plain, ~'E'(f(X0_318),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.39 cnf(l298, plain, ~'E'(f(X0_307),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.39 cnf(l299, plain, 'E'(f(X0_299),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l300, plain, 'E'(f(X0_300),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l301, plain, ~'E'(f(X0_320),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.39 cnf(l302, plain, ~'E'(f(X0_319),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.39 cnf(l303, plain, 'E'(f(X0_303),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l304, plain, 'E'(f(X0_304),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l305, plain, 'E'(f(X0_305),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l306, plain, 'E'(f(X0_306),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l307, plain, 'E'(f(X0_307),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l308, plain, ~'E'(f(X0_315),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))) | 'E'(f(X1_329),s(s(s(s(s(s('0'))))))), inference(instantiation, [status(thm)], [5])).
% 0.18/0.39 cnf(l309, plain, ~'E'(f(X0_314),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.39 cnf(l310, plain, 'E'(f(X0_310),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l311, plain, 'E'(f(X0_311),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l312, plain, 'E'(f(X0_312),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l313, plain, ~'E'(f(X0_316),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.39 cnf(l314, plain, 'E'(f(X0_314),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l315, plain, 'E'(f(X0_315),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l316, plain, 'E'(f(X0_316),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l317, plain, ~'E'(f(X0_326),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.39 cnf(l318, plain, 'E'(f(X0_318),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l319, plain, 'E'(f(X0_319),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l320, plain, 'E'(f(X0_320),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l321, plain, 'E'(f(X0_321),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l322, plain, ~'E'(f(X0_327),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.39 cnf(l323, plain, 'E'(f(X0_323),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l324, plain, ~'E'(f(X0_328),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s('0')))))))), inference(instantiation, [status(thm)], [13])).
% 0.18/0.39 cnf(l325, plain, 'E'(f(X0_325),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l326, plain, 'E'(f(X0_326),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l327, plain, 'E'(f(X0_327),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l328, plain, 'E'(f(X0_328),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(l329, plain, ~'E'(f(X0_330),s(s(s(s(s(s(s(s(s('0')))))))))) | ~'E'(f(X1_329),s(s(s(s(s(s(s(s(s(s('0'))))))))))) | 'E'(f(X1_329),s(s(s(s(s(s(s(s('0'))))))))), inference(instantiation, [status(thm)], [0])).
% 0.18/0.39 cnf(l330, plain, 'E'(f(X0_330),s(s(s(s(s(s(s(s(s('0')))))))))), inference(instantiation, [status(thm)], [8])).
% 0.18/0.39 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l3, l11, l12, l13, l14, l15, l6, l16, l17, l18, l19, l20, l54, l26, l30, l47, l65, l48, l4, l29, l2, l53, l70, l55, l22, l42, l39, l31, l36, l34, l71, l58, l72, l21, l67, l73, l5, l46, l74, l75, l37, l76, l77, l78, l79, l80, l81, l82, l83, l84, l85, l86, l27, l87, l88, l89, l25, l28, l90, l91, l92, l93, l94, l69, l95, l96, l97, l98, l41, l99, l100, l101, l102, l103, l104, l33, l105, l106, l107, l108, l109, l110, l111, l112, l113, l114, l115, l116, l117, l118, l119, l120, l121, l122, l123, l60, l64, l124, l56, l125, l126, l127, l128, l129, l130, l131, l61, l132, l44, l133, l134, l135, l136, l137, l138, l139, l140, l141, l142, l143, l144, l57, l66, l145, l43, l146, l147, l148, l32, l149, l150, l151, l152, l153, l154, l155, l156, l157, l158, l159, l160, l161, l162, l163, l62, l164, l59, l52, l165, l166, l167, l168, l169, l170, l171, l172, l173, l174, l35, l175, l176, l177, l178, l179, l180, l181, l182, l183, l184, l185, l186, l187, l188, l189, l190, l191, l63, l192, l193, l194, l195, l196, l197, l198, l199, l200, l201, l202, l203, l204, l205, l206, l207, l208, l209, l210, l211, l212, l213, l214, l215, l216, l217, l218, l219, l220, l221, l222, l223, l224, l225, l226, l227, l228, l229, l230, l231, l232, l233, l68, l50, l234, l235, l236, l237, l238, l239, l240, l241, l242, l40, l243, l244, l245, l246, l247, l248, l249, l250, l251, l252, l253, l254, l255, l256, l257, l258, l259, l260, l261, l262, l263, l264, l265, l266, l267, l268, l269, l270, l271, l272, l273, l274, l275, l276, l277, l278, l279, l280, l281, l282, l283, l284, l285, l286, l287, l288, l289, l290, l291, l292, l293, l294, l295, l296, l297, l298, l299, l300, l301, l302, l303, l304, l305, l306, l307, l308, l309, l310, l311, l312, l313, l314, l315, l316, l317, l318, l319, l320, l321, l322, l323, l324, l325, l326, l327, l328, l329, l330])).
% 0.18/0.39 % SZS output end CNFRefutation
%------------------------------------------------------------------------------