%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL901+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:43:47 PM UTC 2026
% Result : Theorem 3.05s 3.31s
% Output : CNFRefutation 3.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL901+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.08/0.36 % Computer : n014.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Sat Sep 5 10:21:27 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 3.05/3.31 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.05/3.31
% 3.05/3.31 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.05/3.31 fof(sos_01, axiom, (! [A, B, C] : add(add(A, B), C) = add(A, add(B, C)))).
% 3.05/3.31
% 3.05/3.31 fof(sos_02, axiom, (! [A, B] : add(A, B) = add(B, A))).
% 3.05/3.31
% 3.05/3.31 fof(sos_03, axiom, (! [A] : add(A, 0) = A)).
% 3.05/3.31
% 3.05/3.31 fof(sos_04, axiom, (! [A] : greater_equal(A, A))).
% 3.05/3.31
% 3.05/3.31 fof(sos_06, axiom,
% 3.05/3.31 (! [X3, X4] :
% 3.05/3.31 ((greater_equal(X3, X4) & greater_equal(X4, X3)) => X3 = X4))).
% 3.05/3.31
% 3.05/3.31 fof(sos_07, axiom,
% 3.05/3.31 (! [X5, X6, X7] :
% 3.05/3.31 (greater_equal(add(X5, X6), X7) <=>
% 3.05/3.31 greater_equal(X6, '==>'(X5, X7))))).
% 3.05/3.31
% 3.05/3.31 fof(sos_08, axiom, (! [A] : greater_equal(A, 0))).
% 3.05/3.31
% 3.05/3.31 fof(sos_09, axiom,
% 3.05/3.31 (! [X8, X9, X10] :
% 3.05/3.31 (greater_equal(X8, X9) =>
% 3.05/3.31 greater_equal(add(X8, X10), add(X9, X10))))).
% 3.05/3.31
% 3.05/3.31 fof(sos_10, axiom,
% 3.05/3.31 (! [X11, X12, X13] :
% 3.05/3.31 (greater_equal(X11, X12) =>
% 3.05/3.31 greater_equal('==>'(X12, X13), '==>'(X11, X13))))).
% 3.05/3.31
% 3.05/3.31 fof(sos_12, axiom, (! [A] : add(A, 1) = 1)).
% 3.05/3.31
% 3.05/3.31 fof(sos_13, axiom,
% 3.05/3.31 (! [A, B] : '==>'('==>'(A, B), B) = '==>'('==>'(B, A), A))).
% 3.05/3.31
% 3.05/3.31 fof(sos_14, axiom, (! [A] : add(A, A) = A)).
% 3.05/3.31
% 3.05/3.31 fof(goals_15, conjecture,
% 3.05/3.31 (! [X17] : '==>'('==>'('==>'(X17, 1), X17), X17) = 0)).
% 3.05/3.31
% 3.05/3.31 fof(subgoal_0, plain,
% 3.05/3.31 (! [X17] : '==>'('==>'('==>'(X17, 1), X17), X17) = 0),
% 3.05/3.31 inference(strip, [], [goals_15])).
% 3.05/3.31
% 3.05/3.31 fof(negate_0_0, plain,
% 3.05/3.31 (~ ! [X17] : '==>'('==>'('==>'(X17, 1), X17), X17) = 0),
% 3.05/3.31 inference(negate, [], [subgoal_0])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_0, plain,
% 3.05/3.31 (? [X17] : '==>'('==>'('==>'(X17, 1), X17), X17) != 0),
% 3.05/3.31 inference(canonicalize, [], [negate_0_0])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_1, plain,
% 3.05/3.31 ('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.31 skolemFOFtoCNF_X17) != 0),
% 3.05/3.31 inference(skolemize, [], [normalize_0_0])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_2, plain,
% 3.05/3.31 (! [A, B] : '==>'('==>'(A, B), B) = '==>'('==>'(B, A), A)),
% 3.05/3.31 inference(canonicalize, [], [sos_13])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_3, plain,
% 3.05/3.31 (! [A, B] : '==>'('==>'(A, B), B) = '==>'('==>'(B, A), A)),
% 3.05/3.31 inference(specialize, [], [normalize_0_2])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_4, plain, (! [A] : greater_equal(A, A)),
% 3.05/3.31 inference(canonicalize, [], [sos_04])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_5, plain, (! [A] : greater_equal(A, A)),
% 3.05/3.31 inference(specialize, [], [normalize_0_4])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_6, plain,
% 3.05/3.31 (! [X5, X6, X7] :
% 3.05/3.31 (~ greater_equal(X6, '==>'(X5, X7)) <=>
% 3.05/3.31 ~ greater_equal(add(X5, X6), X7))),
% 3.05/3.31 inference(canonicalize, [], [sos_07])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_7, plain,
% 3.05/3.31 (! [X5, X6, X7] :
% 3.05/3.31 (~ greater_equal(X6, '==>'(X5, X7)) <=>
% 3.05/3.31 ~ greater_equal(add(X5, X6), X7))),
% 3.05/3.31 inference(specialize, [], [normalize_0_6])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_8, plain,
% 3.05/3.31 (! [X5, X6, X7] :
% 3.05/3.31 ((~ greater_equal(X6, '==>'(X5, X7)) |
% 3.05/3.31 greater_equal(add(X5, X6), X7)) &
% 3.05/3.31 (~ greater_equal(add(X5, X6), X7) |
% 3.05/3.31 greater_equal(X6, '==>'(X5, X7))))),
% 3.05/3.31 inference(clausify, [], [normalize_0_7])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_9, plain,
% 3.05/3.31 (! [X5, X6, X7] :
% 3.05/3.31 (~ greater_equal(X6, '==>'(X5, X7)) |
% 3.05/3.31 greater_equal(add(X5, X6), X7))),
% 3.05/3.31 inference(conjunct, [], [normalize_0_8])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_10, plain, (! [A] : add(A, 0) = A),
% 3.05/3.31 inference(canonicalize, [], [sos_03])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_11, plain, (! [A] : add(A, 0) = A),
% 3.05/3.31 inference(specialize, [], [normalize_0_10])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_12, plain, (! [A, B] : add(A, B) = add(B, A)),
% 3.05/3.31 inference(canonicalize, [], [sos_02])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_13, plain, (! [A, B] : add(A, B) = add(B, A)),
% 3.05/3.31 inference(specialize, [], [normalize_0_12])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_14, plain,
% 3.05/3.31 (! [X3, X4] :
% 3.05/3.31 (~ greater_equal(X3, X4) | ~ greater_equal(X4, X3) | X3 = X4)),
% 3.05/3.31 inference(canonicalize, [], [sos_06])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_15, plain,
% 3.05/3.31 (! [X3, X4] :
% 3.05/3.31 (~ greater_equal(X3, X4) | ~ greater_equal(X4, X3) | X3 = X4)),
% 3.05/3.31 inference(specialize, [], [normalize_0_14])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_16, plain, (! [A] : greater_equal(A, 0)),
% 3.05/3.31 inference(canonicalize, [], [sos_08])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_17, plain, (! [A] : greater_equal(A, 0)),
% 3.05/3.31 inference(specialize, [], [normalize_0_16])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_18, plain,
% 3.05/3.31 (! [X8, X9] :
% 3.05/3.31 (~ greater_equal(X8, X9) |
% 3.05/3.31 ! [X10] : greater_equal(add(X8, X10), add(X9, X10)))),
% 3.05/3.31 inference(canonicalize, [], [sos_09])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_19, plain,
% 3.05/3.31 (! [X8, X9] :
% 3.05/3.31 (~ greater_equal(X8, X9) |
% 3.05/3.31 ! [X10] : greater_equal(add(X8, X10), add(X9, X10)))),
% 3.05/3.31 inference(specialize, [], [normalize_0_18])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_20, plain,
% 3.05/3.31 (! [X10, X8, X9] :
% 3.05/3.31 (~ greater_equal(X8, X9) |
% 3.05/3.31 greater_equal(add(X8, X10), add(X9, X10)))),
% 3.05/3.31 inference(clausify, [], [normalize_0_19])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_21, plain,
% 3.05/3.31 (! [X5, X6, X7] :
% 3.05/3.31 (~ greater_equal(add(X5, X6), X7) |
% 3.05/3.31 greater_equal(X6, '==>'(X5, X7)))),
% 3.05/3.31 inference(conjunct, [], [normalize_0_8])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_22, plain,
% 3.05/3.31 (! [X11, X12] :
% 3.05/3.31 (~ greater_equal(X11, X12) |
% 3.05/3.31 ! [X13] : greater_equal('==>'(X12, X13), '==>'(X11, X13)))),
% 3.05/3.31 inference(canonicalize, [], [sos_10])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_23, plain,
% 3.05/3.31 (! [X11, X12] :
% 3.05/3.31 (~ greater_equal(X11, X12) |
% 3.05/3.31 ! [X13] : greater_equal('==>'(X12, X13), '==>'(X11, X13)))),
% 3.05/3.31 inference(specialize, [], [normalize_0_22])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_24, plain,
% 3.05/3.31 (! [X11, X12, X13] :
% 3.05/3.31 (~ greater_equal(X11, X12) |
% 3.05/3.31 greater_equal('==>'(X12, X13), '==>'(X11, X13)))),
% 3.05/3.31 inference(clausify, [], [normalize_0_23])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_25, plain,
% 3.05/3.31 (! [A, B, C] : add(add(A, B), C) = add(A, add(B, C))),
% 3.05/3.31 inference(canonicalize, [], [sos_01])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_26, plain,
% 3.05/3.31 (! [A, B, C] : add(add(A, B), C) = add(A, add(B, C))),
% 3.05/3.31 inference(specialize, [], [normalize_0_25])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_27, plain, (! [A] : add(A, A) = A),
% 3.05/3.31 inference(canonicalize, [], [sos_14])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_28, plain, (! [A] : add(A, A) = A),
% 3.05/3.31 inference(specialize, [], [normalize_0_27])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_29, plain, (! [A] : add(A, 1) = 1),
% 3.05/3.31 inference(canonicalize, [], [sos_12])).
% 3.05/3.31
% 3.05/3.31 fof(normalize_0_30, plain, (! [A] : add(A, 1) = 1),
% 3.05/3.31 inference(specialize, [], [normalize_0_29])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_0, plain,
% 3.05/3.31 ('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.31 skolemFOFtoCNF_X17) != 0),
% 3.05/3.31 inference(canonicalize, [], [normalize_0_1])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_1, plain, ('==>'('==>'(A, B), B) = '==>'('==>'(B, A), A)),
% 3.05/3.31 inference(canonicalize, [], [normalize_0_3])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_2, plain,
% 3.05/3.31 ('==>'('==>'(A, '==>'('==>'(X_19, A), A)), '==>'('==>'(X_19, A), A)) =
% 3.05/3.31 '==>'('==>'('==>'('==>'(X_19, A), A), A), A)),
% 3.05/3.31 inference(subst, [],
% 3.05/3.31 [refute_0_1 : [bind(B, $fot('==>'('==>'(X_19, A), A)))]])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_3, plain,
% 3.05/3.31 ('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)) =
% 3.05/3.31 '==>'('==>'('==>'(X_5, A), A), A)),
% 3.05/3.31 inference(subst, [], [refute_0_1 : [bind(B, $fot('==>'(X_5, A)))]])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_4, plain,
% 3.05/3.31 ('==>'('==>'(X_5, A), A) = '==>'('==>'(A, X_5), X_5)),
% 3.05/3.31 inference(subst, [],
% 3.05/3.31 [refute_0_1 : [bind(A, $fot(X_5)), bind(B, $fot(A))]])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_5, plain,
% 3.05/3.31 ('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)) !=
% 3.05/3.31 '==>'('==>'('==>'(X_5, A), A), A) |
% 3.05/3.31 '==>'('==>'(X_5, A), A) != '==>'('==>'(A, X_5), X_5) |
% 3.05/3.31 '==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)) =
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A)),
% 3.05/3.31 introduced(tautology,
% 3.05/3.31 [equality,
% 3.05/3.31 [$cnf($equal('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)),
% 3.05/3.31 '==>'('==>'('==>'(X_5, A), A), A))), [1, 0],
% 3.05/3.31 $fot('==>'('==>'(A, X_5), X_5))]])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_6, plain,
% 3.05/3.31 ('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)) !=
% 3.05/3.31 '==>'('==>'('==>'(X_5, A), A), A) |
% 3.05/3.31 '==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)) =
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A)),
% 3.05/3.31 inference(resolve,
% 3.05/3.31 [$cnf($equal('==>'('==>'(X_5, A), A),
% 3.05/3.31 '==>'('==>'(A, X_5), X_5)))],
% 3.05/3.31 [refute_0_4, refute_0_5])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_7, plain,
% 3.05/3.31 ('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)) =
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A)),
% 3.05/3.31 inference(resolve,
% 3.05/3.31 [$cnf($equal('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)),
% 3.05/3.31 '==>'('==>'('==>'(X_5, A), A), A)))],
% 3.05/3.31 [refute_0_3, refute_0_6])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_8, plain,
% 3.05/3.31 ('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)) !=
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A) |
% 3.05/3.31 '==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)) !=
% 3.05/3.31 '==>'('==>'('==>'(X_5, A), A), A) |
% 3.05/3.31 '==>'('==>'('==>'(X_5, A), A), A) =
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A)),
% 3.05/3.31 introduced(tautology,
% 3.05/3.31 [equality,
% 3.05/3.31 [$cnf($equal('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)),
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A))), [0],
% 3.05/3.31 $fot('==>'('==>'('==>'(X_5, A), A), A))]])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_9, plain,
% 3.05/3.31 ('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)) !=
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A) |
% 3.05/3.31 '==>'('==>'('==>'(X_5, A), A), A) =
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A)),
% 3.05/3.31 inference(resolve,
% 3.05/3.31 [$cnf($equal('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)),
% 3.05/3.31 '==>'('==>'('==>'(X_5, A), A), A)))],
% 3.05/3.31 [refute_0_3, refute_0_8])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_10, plain,
% 3.05/3.31 ('==>'('==>'('==>'(X_5, A), A), A) =
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A)),
% 3.05/3.31 inference(resolve,
% 3.05/3.31 [$cnf($equal('==>'('==>'(A, '==>'(X_5, A)), '==>'(X_5, A)),
% 3.05/3.31 '==>'('==>'('==>'(A, X_5), X_5), A)))],
% 3.05/3.31 [refute_0_7, refute_0_9])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_11, plain,
% 3.05/3.31 ('==>'('==>'('==>'(X_19, A), A), A) =
% 3.05/3.31 '==>'('==>'('==>'(A, X_19), X_19), A)),
% 3.05/3.31 inference(subst, [], [refute_0_10 : [bind(X_5, $fot(X_19))]])).
% 3.05/3.31
% 3.05/3.31 cnf(refute_0_12, plain,
% 3.05/3.31 ('==>'('==>'(A, '==>'('==>'(X_19, A), A)), '==>'('==>'(X_19, A), A)) !=
% 3.05/3.31 '==>'('==>'('==>'('==>'(X_19, A), A), A), A) |
% 3.05/3.32 '==>'('==>'('==>'(X_19, A), A), A) !=
% 3.05/3.32 '==>'('==>'('==>'(A, X_19), X_19), A) |
% 3.05/3.32 '==>'('==>'(A, '==>'('==>'(X_19, A), A)), '==>'('==>'(X_19, A), A)) =
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A)),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'(A, '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'('==>'('==>'(X_19, A), A), A), A))),
% 3.05/3.32 [1, 0], $fot('==>'('==>'('==>'(A, X_19), X_19), A))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_13, plain,
% 3.05/3.32 ('==>'('==>'(A, '==>'('==>'(X_19, A), A)), '==>'('==>'(X_19, A), A)) !=
% 3.05/3.32 '==>'('==>'('==>'('==>'(X_19, A), A), A), A) |
% 3.05/3.32 '==>'('==>'(A, '==>'('==>'(X_19, A), A)), '==>'('==>'(X_19, A), A)) =
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'(X_19, A), A), A),
% 3.05/3.32 '==>'('==>'('==>'(A, X_19), X_19), A)))],
% 3.05/3.32 [refute_0_11, refute_0_12])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_14, plain,
% 3.05/3.32 ('==>'('==>'(A, '==>'('==>'(X_19, A), A)), '==>'('==>'(X_19, A), A)) =
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'(A, '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'('==>'('==>'(X_19, A), A), A), A)))],
% 3.05/3.32 [refute_0_2, refute_0_13])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_15, plain,
% 3.05/3.32 ('==>'('==>'(A, '==>'('==>'(X_19, A), A)), '==>'('==>'(X_19, A), A)) !=
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A) |
% 3.05/3.32 '==>'('==>'(A, '==>'('==>'(X_19, A), A)), '==>'('==>'(X_19, A), A)) !=
% 3.05/3.32 '==>'('==>'('==>'('==>'(X_19, A), A), A), A) |
% 3.05/3.32 '==>'('==>'('==>'('==>'(X_19, A), A), A), A) =
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A)),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'(A, '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A))),
% 3.05/3.32 [0],
% 3.05/3.32 $fot('==>'('==>'('==>'('==>'(X_19, A), A), A), A))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_16, plain,
% 3.05/3.32 ('==>'('==>'(A, '==>'('==>'(X_19, A), A)), '==>'('==>'(X_19, A), A)) !=
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A) |
% 3.05/3.32 '==>'('==>'('==>'('==>'(X_19, A), A), A), A) =
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'(A, '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'('==>'('==>'(X_19, A), A), A), A)))],
% 3.05/3.32 [refute_0_2, refute_0_15])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_17, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(X_19, A), A), A), A) =
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'(A, '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'(X_19, A), A)),
% 3.05/3.32 '==>'('==>'('==>'('==>'(A, X_19), X_19), A), A)))],
% 3.05/3.32 [refute_0_14, refute_0_16])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_18, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) =
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_17 :
% 3.05/3.32 [bind(A, $fot('==>'(X_546, 0))), bind(X_19, $fot(0))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_19, plain,
% 3.05/3.32 ('==>'('==>'('==>'(X_5, 0), 0), 0) =
% 3.05/3.32 '==>'('==>'('==>'(0, X_5), X_5), 0)),
% 3.05/3.32 inference(subst, [], [refute_0_10 : [bind(A, $fot(0))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_20, plain, (greater_equal(A, A)),
% 3.05/3.32 inference(canonicalize, [], [normalize_0_5])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_21, plain,
% 3.05/3.32 (greater_equal('==>'(X_28, X_30), '==>'(X_28, X_30))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_20 : [bind(A, $fot('==>'(X_28, X_30)))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_22, plain,
% 3.05/3.32 (~ greater_equal(X6, '==>'(X5, X7)) | greater_equal(add(X5, X6), X7)),
% 3.05/3.32 inference(canonicalize, [], [normalize_0_9])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_23, plain,
% 3.05/3.32 (~ greater_equal('==>'(X_28, X_30), '==>'(X_28, X_30)) |
% 3.05/3.32 greater_equal(add(X_28, '==>'(X_28, X_30)), X_30)),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_22 :
% 3.05/3.32 [bind(X5, $fot(X_28)), bind(X6, $fot('==>'(X_28, X_30))),
% 3.05/3.32 bind(X7, $fot(X_30))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_24, plain,
% 3.05/3.32 (greater_equal(add(X_28, '==>'(X_28, X_30)), X_30)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf(greater_equal('==>'(X_28, X_30), '==>'(X_28, X_30)))],
% 3.05/3.32 [refute_0_21, refute_0_23])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_25, plain, (greater_equal(add(0, '==>'(0, X_32)), X_32)),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_24 :
% 3.05/3.32 [bind(X_28, $fot(0)), bind(X_30, $fot(X_32))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_26, plain, (add(A, 0) = A),
% 3.05/3.32 inference(canonicalize, [], [normalize_0_11])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_27, plain, (add(A, B) = add(B, A)),
% 3.05/3.32 inference(canonicalize, [], [normalize_0_13])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_28, plain, (add(A, 0) = add(0, A)),
% 3.05/3.32 inference(subst, [], [refute_0_27 : [bind(B, $fot(0))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_29, plain,
% 3.05/3.32 (add(A, 0) != A | add(A, 0) != add(0, A) | add(0, A) = A),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal(add(A, 0), A)), [0], $fot(add(0, A))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_30, plain, (add(A, 0) != A | add(0, A) = A),
% 3.05/3.32 inference(resolve, [$cnf($equal(add(A, 0), add(0, A)))],
% 3.05/3.32 [refute_0_28, refute_0_29])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_31, plain, (add(0, A) = A),
% 3.05/3.32 inference(resolve, [$cnf($equal(add(A, 0), A))],
% 3.05/3.32 [refute_0_26, refute_0_30])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_32, plain, (add(0, '==>'(0, X_32)) = '==>'(0, X_32)),
% 3.05/3.32 inference(subst, [], [refute_0_31 : [bind(A, $fot('==>'(0, X_32)))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_33, plain,
% 3.05/3.32 (add(0, '==>'(0, X_32)) != '==>'(0, X_32) |
% 3.05/3.32 ~ greater_equal(add(0, '==>'(0, X_32)), X_32) |
% 3.05/3.32 greater_equal('==>'(0, X_32), X_32)),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf(greater_equal(add(0, '==>'(0, X_32)), X_32)), [0],
% 3.05/3.32 $fot('==>'(0, X_32))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_34, plain,
% 3.05/3.32 (~ greater_equal(add(0, '==>'(0, X_32)), X_32) |
% 3.05/3.32 greater_equal('==>'(0, X_32), X_32)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal(add(0, '==>'(0, X_32)), '==>'(0, X_32)))],
% 3.05/3.32 [refute_0_32, refute_0_33])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_35, plain, (greater_equal('==>'(0, X_32), X_32)),
% 3.05/3.32 inference(resolve, [$cnf(greater_equal(add(0, '==>'(0, X_32)), X_32))],
% 3.05/3.32 [refute_0_25, refute_0_34])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_36, plain, (greater_equal('==>'(0, X_542), X_542)),
% 3.05/3.32 inference(subst, [], [refute_0_35 : [bind(X_32, $fot(X_542))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_37, plain,
% 3.05/3.32 (~ greater_equal(X3, X4) | ~ greater_equal(X4, X3) | X3 = X4),
% 3.05/3.32 inference(canonicalize, [], [normalize_0_15])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_38, plain,
% 3.05/3.32 (~ greater_equal(X_542, '==>'(0, X_542)) |
% 3.05/3.32 ~ greater_equal('==>'(0, X_542), X_542) | '==>'(0, X_542) = X_542),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_37 :
% 3.05/3.32 [bind(X3, $fot('==>'(0, X_542))), bind(X4, $fot(X_542))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_39, plain,
% 3.05/3.32 (~ greater_equal(X_542, '==>'(0, X_542)) | '==>'(0, X_542) = X_542),
% 3.05/3.32 inference(resolve, [$cnf(greater_equal('==>'(0, X_542), X_542))],
% 3.05/3.32 [refute_0_36, refute_0_38])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_40, plain, (greater_equal(A, 0)),
% 3.05/3.32 inference(canonicalize, [], [normalize_0_17])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_41, plain, (greater_equal(X_41, 0)),
% 3.05/3.32 inference(subst, [], [refute_0_40 : [bind(A, $fot(X_41))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_42, plain,
% 3.05/3.32 (~ greater_equal(X8, X9) | greater_equal(add(X8, X10), add(X9, X10))),
% 3.05/3.32 inference(canonicalize, [], [normalize_0_20])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_43, plain,
% 3.05/3.32 (~ greater_equal(X_41, 0) |
% 3.05/3.32 greater_equal(add(X_41, X_40), add(0, X_40))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_42 :
% 3.05/3.32 [bind(X10, $fot(X_40)), bind(X8, $fot(X_41)),
% 3.05/3.32 bind(X9, $fot(0))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_44, plain, (greater_equal(add(X_41, X_40), add(0, X_40))),
% 3.05/3.32 inference(resolve, [$cnf(greater_equal(X_41, 0))],
% 3.05/3.32 [refute_0_41, refute_0_43])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_45, plain, (add(0, X_40) = X_40),
% 3.05/3.32 inference(subst, [], [refute_0_31 : [bind(A, $fot(X_40))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_46, plain,
% 3.05/3.32 (add(0, X_40) != X_40 |
% 3.05/3.32 ~ greater_equal(add(X_41, X_40), add(0, X_40)) |
% 3.05/3.32 greater_equal(add(X_41, X_40), X_40)),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf(greater_equal(add(X_41, X_40), add(0, X_40))), [1],
% 3.05/3.32 $fot(X_40)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_47, plain,
% 3.05/3.32 (~ greater_equal(add(X_41, X_40), add(0, X_40)) |
% 3.05/3.32 greater_equal(add(X_41, X_40), X_40)),
% 3.05/3.32 inference(resolve, [$cnf($equal(add(0, X_40), X_40))],
% 3.05/3.32 [refute_0_45, refute_0_46])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_48, plain, (greater_equal(add(X_41, X_40), X_40)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf(greater_equal(add(X_41, X_40), add(0, X_40)))],
% 3.05/3.32 [refute_0_44, refute_0_47])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_49, plain, (greater_equal(add(X_186, X_188), X_188)),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_48 :
% 3.05/3.32 [bind(X_40, $fot(X_188)), bind(X_41, $fot(X_186))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_50, plain,
% 3.05/3.32 (~ greater_equal(add(X5, X6), X7) | greater_equal(X6, '==>'(X5, X7))),
% 3.05/3.32 inference(canonicalize, [], [normalize_0_21])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_51, plain,
% 3.05/3.32 (~ greater_equal(add(X_186, X_188), X_188) |
% 3.05/3.32 greater_equal(X_188, '==>'(X_186, X_188))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_50 :
% 3.05/3.32 [bind(X5, $fot(X_186)), bind(X6, $fot(X_188)),
% 3.05/3.32 bind(X7, $fot(X_188))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_52, plain, (greater_equal(X_188, '==>'(X_186, X_188))),
% 3.05/3.32 inference(resolve, [$cnf(greater_equal(add(X_186, X_188), X_188))],
% 3.05/3.32 [refute_0_49, refute_0_51])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_53, plain, (greater_equal(X_542, '==>'(0, X_542))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_52 :
% 3.05/3.32 [bind(X_186, $fot(0)), bind(X_188, $fot(X_542))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_54, plain, ('==>'(0, X_542) = X_542),
% 3.05/3.32 inference(resolve, [$cnf(greater_equal(X_542, '==>'(0, X_542)))],
% 3.05/3.32 [refute_0_53, refute_0_39])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_55, plain, ('==>'(0, X_5) = X_5),
% 3.05/3.32 inference(subst, [], [refute_0_54 : [bind(X_542, $fot(X_5))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_56, plain,
% 3.05/3.32 ('==>'(0, X_5) != X_5 |
% 3.05/3.32 '==>'('==>'('==>'(X_5, 0), 0), 0) !=
% 3.05/3.32 '==>'('==>'('==>'(0, X_5), X_5), 0) |
% 3.05/3.32 '==>'('==>'('==>'(X_5, 0), 0), 0) = '==>'('==>'(X_5, X_5), 0)),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'(X_5, 0), 0), 0),
% 3.05/3.32 '==>'('==>'('==>'(0, X_5), X_5), 0))), [1, 0, 0],
% 3.05/3.32 $fot(X_5)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_57, plain,
% 3.05/3.32 ('==>'('==>'('==>'(X_5, 0), 0), 0) !=
% 3.05/3.32 '==>'('==>'('==>'(0, X_5), X_5), 0) |
% 3.05/3.32 '==>'('==>'('==>'(X_5, 0), 0), 0) = '==>'('==>'(X_5, X_5), 0)),
% 3.05/3.32 inference(resolve, [$cnf($equal('==>'(0, X_5), X_5))],
% 3.05/3.32 [refute_0_55, refute_0_56])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_58, plain,
% 3.05/3.32 ('==>'('==>'('==>'(X_5, 0), 0), 0) = '==>'('==>'(X_5, X_5), 0)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'(X_5, 0), 0), 0),
% 3.05/3.32 '==>'('==>'('==>'(0, X_5), X_5), 0)))],
% 3.05/3.32 [refute_0_19, refute_0_57])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_59, plain,
% 3.05/3.32 (greater_equal(add(X_186, X_187), add(X_186, X_187))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_20 : [bind(A, $fot(add(X_186, X_187)))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_60, plain,
% 3.05/3.32 (~ greater_equal(add(X_186, X_187), add(X_186, X_187)) |
% 3.05/3.32 greater_equal(X_187, '==>'(X_186, add(X_186, X_187)))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_50 :
% 3.05/3.32 [bind(X5, $fot(X_186)), bind(X6, $fot(X_187)),
% 3.05/3.32 bind(X7, $fot(add(X_186, X_187)))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_61, plain,
% 3.05/3.32 (greater_equal(X_187, '==>'(X_186, add(X_186, X_187)))),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf(greater_equal(add(X_186, X_187), add(X_186, X_187)))],
% 3.05/3.32 [refute_0_59, refute_0_60])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_62, plain, (greater_equal(0, '==>'(X_191, add(X_191, 0)))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_61 :
% 3.05/3.32 [bind(X_186, $fot(X_191)), bind(X_187, $fot(0))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_63, plain, (add(X_191, 0) = X_191),
% 3.05/3.32 inference(subst, [], [refute_0_26 : [bind(A, $fot(X_191))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_64, plain,
% 3.05/3.32 (add(X_191, 0) != X_191 |
% 3.05/3.32 ~ greater_equal(0, '==>'(X_191, add(X_191, 0))) |
% 3.05/3.32 greater_equal(0, '==>'(X_191, X_191))),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf(greater_equal(0, '==>'(X_191, add(X_191, 0)))),
% 3.05/3.32 [1, 1], $fot(X_191)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_65, plain,
% 3.05/3.32 (~ greater_equal(0, '==>'(X_191, add(X_191, 0))) |
% 3.05/3.32 greater_equal(0, '==>'(X_191, X_191))),
% 3.05/3.32 inference(resolve, [$cnf($equal(add(X_191, 0), X_191))],
% 3.05/3.32 [refute_0_63, refute_0_64])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_66, plain, (greater_equal(0, '==>'(X_191, X_191))),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf(greater_equal(0, '==>'(X_191, add(X_191, 0))))],
% 3.05/3.32 [refute_0_62, refute_0_65])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_67, plain,
% 3.05/3.32 (~ greater_equal(X11, X12) |
% 3.05/3.32 greater_equal('==>'(X12, X13), '==>'(X11, X13))),
% 3.05/3.32 inference(canonicalize, [], [normalize_0_24])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_68, plain,
% 3.05/3.32 (~ greater_equal(0, '==>'(X_191, X_191)) |
% 3.05/3.32 greater_equal('==>'('==>'(X_191, X_191), X_411), '==>'(0, X_411))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_67 :
% 3.05/3.32 [bind(X11, $fot(0)), bind(X12, $fot('==>'(X_191, X_191))),
% 3.05/3.32 bind(X13, $fot(X_411))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_69, plain,
% 3.05/3.32 (greater_equal('==>'('==>'(X_191, X_191), X_411), '==>'(0, X_411))),
% 3.05/3.32 inference(resolve, [$cnf(greater_equal(0, '==>'(X_191, X_191)))],
% 3.05/3.32 [refute_0_66, refute_0_68])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_70, plain,
% 3.05/3.32 (~ greater_equal('==>'(0, X_411), '==>'('==>'(X_191, X_191), X_411)) |
% 3.05/3.32 ~ greater_equal('==>'('==>'(X_191, X_191), X_411), '==>'(0, X_411)) |
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411) = '==>'(0, X_411)),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_37 :
% 3.05/3.32 [bind(X3, $fot('==>'('==>'(X_191, X_191), X_411))),
% 3.05/3.32 bind(X4, $fot('==>'(0, X_411)))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_71, plain,
% 3.05/3.32 (~ greater_equal('==>'(0, X_411), '==>'('==>'(X_191, X_191), X_411)) |
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411) = '==>'(0, X_411)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf(greater_equal('==>'('==>'(X_191, X_191), X_411),
% 3.05/3.32 '==>'(0, X_411)))], [refute_0_69, refute_0_70])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_72, plain, ('==>'(0, X_411) = X_411),
% 3.05/3.32 inference(subst, [], [refute_0_54 : [bind(X_542, $fot(X_411))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_73, plain,
% 3.05/3.32 ('==>'(0, X_411) != X_411 |
% 3.05/3.32 ~ greater_equal(X_411, '==>'('==>'(X_191, X_191), X_411)) |
% 3.05/3.32 greater_equal('==>'(0, X_411), '==>'('==>'(X_191, X_191), X_411))),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf(~ greater_equal('==>'(0, X_411),
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411))), [0],
% 3.05/3.32 $fot(X_411)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_74, plain,
% 3.05/3.32 (~ greater_equal(X_411, '==>'('==>'(X_191, X_191), X_411)) |
% 3.05/3.32 greater_equal('==>'(0, X_411), '==>'('==>'(X_191, X_191), X_411))),
% 3.05/3.32 inference(resolve, [$cnf($equal('==>'(0, X_411), X_411))],
% 3.05/3.32 [refute_0_72, refute_0_73])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_75, plain,
% 3.05/3.32 (~ greater_equal(X_411, '==>'('==>'(X_191, X_191), X_411)) |
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411) = '==>'(0, X_411)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf(greater_equal('==>'(0, X_411),
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411)))],
% 3.05/3.32 [refute_0_74, refute_0_71])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_76, plain,
% 3.05/3.32 ('==>'(0, X_411) != X_411 |
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411) != '==>'(0, X_411) |
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411) = X_411),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'(X_191, X_191), X_411),
% 3.05/3.32 '==>'(0, X_411))), [1], $fot(X_411)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_77, plain,
% 3.05/3.32 ('==>'('==>'(X_191, X_191), X_411) != '==>'(0, X_411) |
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411) = X_411),
% 3.05/3.32 inference(resolve, [$cnf($equal('==>'(0, X_411), X_411))],
% 3.05/3.32 [refute_0_72, refute_0_76])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_78, plain,
% 3.05/3.32 (~ greater_equal(X_411, '==>'('==>'(X_191, X_191), X_411)) |
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411) = X_411),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'(X_191, X_191), X_411),
% 3.05/3.32 '==>'(0, X_411)))], [refute_0_75, refute_0_77])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_79, plain,
% 3.05/3.32 (greater_equal(X_411, '==>'('==>'(X_191, X_191), X_411))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_52 :
% 3.05/3.32 [bind(X_186, $fot('==>'(X_191, X_191))),
% 3.05/3.32 bind(X_188, $fot(X_411))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_80, plain, ('==>'('==>'(X_191, X_191), X_411) = X_411),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf(greater_equal(X_411,
% 3.05/3.32 '==>'('==>'(X_191, X_191), X_411)))],
% 3.05/3.32 [refute_0_79, refute_0_78])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_81, plain, ('==>'('==>'(X_5, X_5), 0) = 0),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_80 :
% 3.05/3.32 [bind(X_191, $fot(X_5)), bind(X_411, $fot(0))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_82, plain,
% 3.05/3.32 ('==>'('==>'(X_5, X_5), 0) != 0 |
% 3.05/3.32 '==>'('==>'('==>'(X_5, 0), 0), 0) != '==>'('==>'(X_5, X_5), 0) |
% 3.05/3.32 '==>'('==>'('==>'(X_5, 0), 0), 0) = 0),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'(X_5, 0), 0), 0),
% 3.05/3.32 '==>'('==>'(X_5, X_5), 0))), [1], $fot(0)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_83, plain,
% 3.05/3.32 ('==>'('==>'('==>'(X_5, 0), 0), 0) != '==>'('==>'(X_5, X_5), 0) |
% 3.05/3.32 '==>'('==>'('==>'(X_5, 0), 0), 0) = 0),
% 3.05/3.32 inference(resolve, [$cnf($equal('==>'('==>'(X_5, X_5), 0), 0))],
% 3.05/3.32 [refute_0_81, refute_0_82])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_84, plain, ('==>'('==>'('==>'(X_5, 0), 0), 0) = 0),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'(X_5, 0), 0), 0),
% 3.05/3.32 '==>'('==>'(X_5, X_5), 0)))],
% 3.05/3.32 [refute_0_58, refute_0_83])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_85, plain, ('==>'('==>'('==>'(X_546, 0), 0), 0) = 0),
% 3.05/3.32 inference(subst, [], [refute_0_84 : [bind(X_5, $fot(X_546))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_86, plain,
% 3.05/3.32 ('==>'('==>'('==>'(X_546, 0), 0), 0) != 0 |
% 3.05/3.32 '==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) !=
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) |
% 3.05/3.32 '==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) =
% 3.05/3.32 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0))),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)),
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)))),
% 3.05/3.32 [1, 0, 0], $fot(0)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_87, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) !=
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) |
% 3.05/3.32 '==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) =
% 3.05/3.32 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0))),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'(X_546, 0), 0), 0), 0))],
% 3.05/3.32 [refute_0_85, refute_0_86])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_88, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) =
% 3.05/3.32 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0))),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)),
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0))))],
% 3.05/3.32 [refute_0_18, refute_0_87])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_89, plain,
% 3.05/3.32 ('==>'('==>'('==>'(0, A), A), A) = '==>'('==>'('==>'(A, 0), 0), A)),
% 3.05/3.32 inference(subst, [], [refute_0_10 : [bind(X_5, $fot(0))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_90, plain, ('==>'(0, A) = A),
% 3.05/3.32 inference(subst, [], [refute_0_54 : [bind(X_542, $fot(A))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_91, plain,
% 3.05/3.32 ('==>'(0, A) != A |
% 3.05/3.32 '==>'('==>'('==>'(0, A), A), A) != '==>'('==>'('==>'(A, 0), 0), A) |
% 3.05/3.32 '==>'('==>'(A, A), A) = '==>'('==>'('==>'(A, 0), 0), A)),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'(0, A), A), A),
% 3.05/3.32 '==>'('==>'('==>'(A, 0), 0), A))), [0, 0, 0],
% 3.05/3.32 $fot(A)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_92, plain,
% 3.05/3.32 ('==>'('==>'('==>'(0, A), A), A) != '==>'('==>'('==>'(A, 0), 0), A) |
% 3.05/3.32 '==>'('==>'(A, A), A) = '==>'('==>'('==>'(A, 0), 0), A)),
% 3.05/3.32 inference(resolve, [$cnf($equal('==>'(0, A), A))],
% 3.05/3.32 [refute_0_90, refute_0_91])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_93, plain,
% 3.05/3.32 ('==>'('==>'(A, A), A) = '==>'('==>'('==>'(A, 0), 0), A)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'(0, A), A), A),
% 3.05/3.32 '==>'('==>'('==>'(A, 0), 0), A)))],
% 3.05/3.32 [refute_0_89, refute_0_92])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_94, plain, ('==>'('==>'(A, A), A) = A),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_80 :
% 3.05/3.32 [bind(X_191, $fot(A)), bind(X_411, $fot(A))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_95, plain,
% 3.05/3.32 ('==>'('==>'(A, A), A) != A |
% 3.05/3.32 '==>'('==>'(A, A), A) != '==>'('==>'('==>'(A, 0), 0), A) |
% 3.05/3.32 A = '==>'('==>'('==>'(A, 0), 0), A)),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'(A, A), A),
% 3.05/3.32 '==>'('==>'('==>'(A, 0), 0), A))), [0],
% 3.05/3.32 $fot(A)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_96, plain,
% 3.05/3.32 ('==>'('==>'(A, A), A) != '==>'('==>'('==>'(A, 0), 0), A) |
% 3.05/3.32 A = '==>'('==>'('==>'(A, 0), 0), A)),
% 3.05/3.32 inference(resolve, [$cnf($equal('==>'('==>'(A, A), A), A))],
% 3.05/3.32 [refute_0_94, refute_0_95])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_97, plain, (A = '==>'('==>'('==>'(A, 0), 0), A)),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'(A, A), A),
% 3.05/3.32 '==>'('==>'('==>'(A, 0), 0), A)))],
% 3.05/3.32 [refute_0_93, refute_0_96])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_98, plain, (X = X), introduced(tautology, [refl, [$fot(X)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_99, plain, (X != X | X != Y | Y = X),
% 3.05/3.32 introduced(tautology, [equality, [$cnf($equal(X, X)), [0], $fot(Y)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_100, plain, (X != Y | Y = X),
% 3.05/3.32 inference(resolve, [$cnf($equal(X, X))], [refute_0_98, refute_0_99])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_101, plain,
% 3.05/3.32 (A != '==>'('==>'('==>'(A, 0), 0), A) |
% 3.05/3.32 '==>'('==>'('==>'(A, 0), 0), A) = A),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_100 :
% 3.05/3.32 [bind(X, $fot(A)),
% 3.05/3.32 bind(Y, $fot('==>'('==>'('==>'(A, 0), 0), A)))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_102, plain, ('==>'('==>'('==>'(A, 0), 0), A) = A),
% 3.05/3.32 inference(resolve, [$cnf($equal(A, '==>'('==>'('==>'(A, 0), 0), A)))],
% 3.05/3.32 [refute_0_97, refute_0_101])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_103, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)) =
% 3.05/3.32 '==>'(X_546, 0)),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_102 : [bind(A, $fot('==>'(X_546, 0)))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_104, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) =
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0))),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [refl,
% 3.05/3.32 [$fot('==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_105, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)) !=
% 3.05/3.32 '==>'(X_546, 0) |
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) !=
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) |
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) = '==>'('==>'(X_546, 0), '==>'(X_546, 0))),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'('==>'('==>'(X_546, 0), 0),
% 3.05/3.32 0), '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)))), [1, 0],
% 3.05/3.32 $fot('==>'(X_546, 0))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_106, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)) !=
% 3.05/3.32 '==>'(X_546, 0) |
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) = '==>'('==>'(X_546, 0), '==>'(X_546, 0))),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0))))],
% 3.05/3.32 [refute_0_104, refute_0_105])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_107, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) = '==>'('==>'(X_546, 0), '==>'(X_546, 0))),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)))],
% 3.05/3.32 [refute_0_103, refute_0_106])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_108, plain, (Y != X | Y != Z | X = Z),
% 3.05/3.32 introduced(tautology, [equality, [$cnf($equal(Y, Z)), [0], $fot(X)]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_109, plain, (X != Y | Y != Z | X = Z),
% 3.05/3.32 inference(resolve, [$cnf($equal(Y, X))],
% 3.05/3.32 [refute_0_100, refute_0_108])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_110, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) !=
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) |
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) != '==>'('==>'(X_546, 0), '==>'(X_546, 0)) |
% 3.05/3.32 '==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) =
% 3.05/3.32 '==>'('==>'(X_546, 0), '==>'(X_546, 0))),
% 3.05/3.32 inference(subst, [],
% 3.05/3.32 [refute_0_109 :
% 3.05/3.32 [bind(X,
% 3.05/3.32 $fot('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)))),
% 3.05/3.32 bind(Y,
% 3.05/3.32 $fot('==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)))),
% 3.05/3.32 bind(Z, $fot('==>'('==>'(X_546, 0), '==>'(X_546, 0))))]])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_111, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)) != '==>'('==>'(X_546, 0), '==>'(X_546, 0)) |
% 3.05/3.32 '==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) =
% 3.05/3.32 '==>'('==>'(X_546, 0), '==>'(X_546, 0))),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)),
% 3.05/3.32 '==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0))))],
% 3.05/3.32 [refute_0_18, refute_0_110])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_112, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) =
% 3.05/3.32 '==>'('==>'(X_546, 0), '==>'(X_546, 0))),
% 3.05/3.32 inference(resolve,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'('==>'('==>'(X_546, 0), 0), 0),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'('==>'(X_546, 0), '==>'(X_546, 0))))],
% 3.05/3.32 [refute_0_107, refute_0_111])).
% 3.05/3.32
% 3.05/3.32 cnf(refute_0_113, plain,
% 3.05/3.32 ('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) !=
% 3.05/3.32 '==>'('==>'(X_546, 0), '==>'(X_546, 0)) |
% 3.05/3.32 '==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)) !=
% 3.05/3.32 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) |
% 3.05/3.32 '==>'('==>'(X_546, 0), '==>'(X_546, 0)) =
% 3.05/3.32 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0))),
% 3.05/3.32 introduced(tautology,
% 3.05/3.32 [equality,
% 3.05/3.32 [$cnf($equal('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)),
% 3.05/3.32 '==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.32 '==>'(X_546, 0)))), [0],
% 3.05/3.32 $fot('==>'('==>'(X_546, 0), '==>'(X_546, 0)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_114, plain,
% 3.05/3.33 ('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)), '==>'(X_546, 0)) !=
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) |
% 3.05/3.33 '==>'('==>'(X_546, 0), '==>'(X_546, 0)) =
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)),
% 3.05/3.33 '==>'('==>'(X_546, 0), '==>'(X_546, 0))))],
% 3.05/3.33 [refute_0_112, refute_0_113])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_115, plain,
% 3.05/3.33 ('==>'('==>'(A, B), B) != '==>'('==>'(B, A), A) |
% 3.05/3.33 '==>'('==>'(B, A), A) = '==>'('==>'(A, B), B)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_100 :
% 3.05/3.33 [bind(X, $fot('==>'('==>'(A, B), B))),
% 3.05/3.33 bind(Y, $fot('==>'('==>'(B, A), A)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_116, plain, ('==>'('==>'(B, A), A) = '==>'('==>'(A, B), B)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'(A, B), B), '==>'('==>'(B, A), A)))],
% 3.05/3.33 [refute_0_1, refute_0_115])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_117, plain,
% 3.05/3.33 ('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) =
% 3.05/3.33 '==>'('==>'('==>'(X_546, 0), 0), 0)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_116 :
% 3.05/3.33 [bind(A, $fot('==>'(X_546, 0))), bind(B, $fot(0))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_118, plain,
% 3.05/3.33 ('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) !=
% 3.05/3.33 '==>'('==>'('==>'(X_546, 0), 0), 0) |
% 3.05/3.33 '==>'('==>'('==>'(X_546, 0), 0), 0) != 0 |
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) = 0),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_109 :
% 3.05/3.33 [bind(X,
% 3.05/3.33 $fot('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)))),
% 3.05/3.33 bind(Y, $fot('==>'('==>'('==>'(X_546, 0), 0), 0))),
% 3.05/3.33 bind(Z, $fot(0))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_119, plain,
% 3.05/3.33 ('==>'('==>'('==>'(X_546, 0), 0), 0) != 0 |
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)),
% 3.05/3.33 '==>'('==>'('==>'(X_546, 0), 0), 0)))],
% 3.05/3.33 [refute_0_117, refute_0_118])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_120, plain,
% 3.05/3.33 ('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(X_546, 0), 0), 0), 0))],
% 3.05/3.33 [refute_0_85, refute_0_119])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_121, plain,
% 3.05/3.33 ('==>'('==>'(X_546, 0), '==>'(X_546, 0)) !=
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) |
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) != 0 |
% 3.05/3.33 '==>'('==>'(X_546, 0), '==>'(X_546, 0)) = 0),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf(~ $equal('==>'('==>'(X_546, 0), '==>'(X_546, 0)),
% 3.05/3.33 0)), [0],
% 3.05/3.33 $fot('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_122, plain,
% 3.05/3.33 ('==>'('==>'(X_546, 0), '==>'(X_546, 0)) !=
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) |
% 3.05/3.33 '==>'('==>'(X_546, 0), '==>'(X_546, 0)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)), 0))],
% 3.05/3.33 [refute_0_120, refute_0_121])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_123, plain,
% 3.05/3.33 ('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)), '==>'(X_546, 0)) !=
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0)) |
% 3.05/3.33 '==>'('==>'(X_546, 0), '==>'(X_546, 0)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'(X_546, 0), '==>'(X_546, 0)),
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0))))],
% 3.05/3.33 [refute_0_114, refute_0_122])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_124, plain, ('==>'('==>'(X_546, 0), '==>'(X_546, 0)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'('==>'(0, '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)), '==>'(X_546, 0)),
% 3.05/3.33 '==>'(X_546, 0)),
% 3.05/3.33 '==>'('==>'(0, '==>'(X_546, 0)), '==>'(X_546, 0))))],
% 3.05/3.33 [refute_0_88, refute_0_123])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_125, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'('==>'(B, 0), 0)) = 0),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_124 : [bind(X_546, $fot('==>'(B, 0)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_126, plain, ('==>'('==>'(0, B), B) = '==>'('==>'(B, 0), 0)),
% 3.05/3.33 inference(subst, [], [refute_0_1 : [bind(A, $fot(0))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_127, plain,
% 3.05/3.33 ('==>'('==>'(0, B), B) != '==>'('==>'(B, 0), 0) |
% 3.05/3.33 '==>'('==>'(B, 0), 0) = '==>'('==>'(0, B), B)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_100 :
% 3.05/3.33 [bind(X, $fot('==>'('==>'(0, B), B))),
% 3.05/3.33 bind(Y, $fot('==>'('==>'(B, 0), 0)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_128, plain, ('==>'('==>'(B, 0), 0) = '==>'('==>'(0, B), B)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)))],
% 3.05/3.33 [refute_0_126, refute_0_127])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_129, plain,
% 3.05/3.33 ('==>'('==>'(B, 0), 0) != '==>'('==>'(0, B), B) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(B, 0), 0)) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) = 0),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(B, 0), 0)), 0)), [0, 1],
% 3.05/3.33 $fot('==>'('==>'(0, B), B))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_130, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'('==>'(B, 0), 0)) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)))],
% 3.05/3.33 [refute_0_128, refute_0_129])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_131, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(B, 0), 0)), 0))],
% 3.05/3.33 [refute_0_125, refute_0_130])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_132, plain, ('==>'(0, B) = B),
% 3.05/3.33 inference(subst, [], [refute_0_54 : [bind(X_542, $fot(B))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_133, plain, ('==>'('==>'(0, B), B) = '==>'('==>'(0, B), B)),
% 3.05/3.33 introduced(tautology, [refl, [$fot('==>'('==>'(0, B), B))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_134, plain,
% 3.05/3.33 ('==>'(0, B) != B | '==>'('==>'(0, B), B) != '==>'('==>'(0, B), B) |
% 3.05/3.33 '==>'('==>'(0, B), B) = '==>'(B, B)),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(0, B), B))), [1, 0], $fot(B)]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_135, plain,
% 3.05/3.33 ('==>'(0, B) != B | '==>'('==>'(0, B), B) = '==>'(B, B)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'(0, B), B), '==>'('==>'(0, B), B)))],
% 3.05/3.33 [refute_0_133, refute_0_134])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_136, plain, ('==>'('==>'(0, B), B) = '==>'(B, B)),
% 3.05/3.33 inference(resolve, [$cnf($equal('==>'(0, B), B))],
% 3.05/3.33 [refute_0_132, refute_0_135])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_137, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) =
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [refl,
% 3.05/3.33 [$fot('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(0, B), B)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_138, plain,
% 3.05/3.33 ('==>'('==>'(0, B), B) != '==>'(B, B) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) !=
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) =
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(0, B), B)),
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(0, B), B)))), [1, 1],
% 3.05/3.33 $fot('==>'(B, B))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_139, plain,
% 3.05/3.33 ('==>'('==>'(0, B), B) != '==>'(B, B) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) =
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(0, B), B)),
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(0, B), B))))],
% 3.05/3.33 [refute_0_137, refute_0_138])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_140, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) =
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B))),
% 3.05/3.33 inference(resolve, [$cnf($equal('==>'('==>'(0, B), B), '==>'(B, B)))],
% 3.05/3.33 [refute_0_136, refute_0_139])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_141, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) !=
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) = 0),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(0, B), B)), 0)), [0],
% 3.05/3.33 $fot('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_142, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(0, B), B)),
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B))))],
% 3.05/3.33 [refute_0_140, refute_0_141])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_143, plain, ('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(0, B), B)), 0))],
% 3.05/3.33 [refute_0_131, refute_0_142])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_144, plain, ('==>'(0, '==>'(B, B)) = '==>'(B, B)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_54 : [bind(X_542, $fot('==>'(B, B)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_145, plain,
% 3.05/3.33 ('==>'('==>'(B, 0), 0) != '==>'('==>'(0, B), B) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'('==>'(B, 0), 0)) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) = 0),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(B, 0), 0)), 0)), [0, 0],
% 3.05/3.33 $fot('==>'('==>'(0, B), B))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_146, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'('==>'(B, 0), 0)) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'(B, 0), 0), '==>'('==>'(0, B), B)))],
% 3.05/3.33 [refute_0_128, refute_0_145])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_147, plain,
% 3.05/3.33 ('==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0),
% 3.05/3.33 '==>'('==>'(B, 0), 0)), 0))],
% 3.05/3.33 [refute_0_125, refute_0_146])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_148, plain,
% 3.05/3.33 ('==>'('==>'(B, B), '==>'('==>'(B, 0), 0)) = '==>'('==>'(B, 0), 0)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_80 :
% 3.05/3.33 [bind(X_191, $fot(B)),
% 3.05/3.33 bind(X_411, $fot('==>'('==>'(B, 0), 0)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_149, plain,
% 3.05/3.33 ('==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) =
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [refl,
% 3.05/3.33 [$fot('==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_150, plain,
% 3.05/3.33 ('==>'('==>'(0, B), B) != '==>'(B, B) |
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) !=
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) |
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) =
% 3.05/3.33 '==>'('==>'(B, B), '==>'('==>'(B, 0), 0))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0)),
% 3.05/3.33 '==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0)))), [1, 0],
% 3.05/3.33 $fot('==>'(B, B))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_151, plain,
% 3.05/3.33 ('==>'('==>'(0, B), B) != '==>'(B, B) |
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) =
% 3.05/3.33 '==>'('==>'(B, B), '==>'('==>'(B, 0), 0))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0)),
% 3.05/3.33 '==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0))))],
% 3.05/3.33 [refute_0_149, refute_0_150])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_152, plain,
% 3.05/3.33 ('==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) =
% 3.05/3.33 '==>'('==>'(B, B), '==>'('==>'(B, 0), 0))),
% 3.05/3.33 inference(resolve, [$cnf($equal('==>'('==>'(0, B), B), '==>'(B, B)))],
% 3.05/3.33 [refute_0_136, refute_0_151])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_153, plain,
% 3.05/3.33 ('==>'('==>'(B, B), '==>'('==>'(B, 0), 0)) != '==>'('==>'(B, 0), 0) |
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) !=
% 3.05/3.33 '==>'('==>'(B, B), '==>'('==>'(B, 0), 0)) |
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) =
% 3.05/3.33 '==>'('==>'(B, 0), 0)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_109 :
% 3.05/3.33 [bind(X,
% 3.05/3.33 $fot('==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0)))),
% 3.05/3.33 bind(Y, $fot('==>'('==>'(B, B), '==>'('==>'(B, 0), 0)))),
% 3.05/3.33 bind(Z, $fot('==>'('==>'(B, 0), 0)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_154, plain,
% 3.05/3.33 ('==>'('==>'(B, B), '==>'('==>'(B, 0), 0)) != '==>'('==>'(B, 0), 0) |
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) =
% 3.05/3.33 '==>'('==>'(B, 0), 0)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0)),
% 3.05/3.33 '==>'('==>'(B, B), '==>'('==>'(B, 0), 0))))],
% 3.05/3.33 [refute_0_152, refute_0_153])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_155, plain,
% 3.05/3.33 ('==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) =
% 3.05/3.33 '==>'('==>'(B, 0), 0)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'(B, B), '==>'('==>'(B, 0), 0)),
% 3.05/3.33 '==>'('==>'(B, 0), 0)))],
% 3.05/3.33 [refute_0_148, refute_0_154])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_156, plain,
% 3.05/3.33 ('==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) !=
% 3.05/3.33 '==>'('==>'(B, 0), 0) | '==>'('==>'(B, 0), 0) = 0),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0)), 0)), [0],
% 3.05/3.33 $fot('==>'('==>'(B, 0), 0))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_157, plain,
% 3.05/3.33 ('==>'('==>'('==>'(0, B), B), '==>'('==>'(B, 0), 0)) != 0 |
% 3.05/3.33 '==>'('==>'(B, 0), 0) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0)), '==>'('==>'(B, 0), 0)))],
% 3.05/3.33 [refute_0_155, refute_0_156])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_158, plain, ('==>'('==>'(B, 0), 0) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(0, B), B),
% 3.05/3.33 '==>'('==>'(B, 0), 0)), 0))],
% 3.05/3.33 [refute_0_147, refute_0_157])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_159, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) =
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [refl, [$fot('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_160, plain,
% 3.05/3.33 ('==>'('==>'(B, 0), 0) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) !=
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) = '==>'(0, '==>'(B, B))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)),
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)))),
% 3.05/3.33 [1, 0], $fot(0)]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_161, plain,
% 3.05/3.33 ('==>'('==>'(B, 0), 0) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) = '==>'(0, '==>'(B, B))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)),
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B))))],
% 3.05/3.33 [refute_0_159, refute_0_160])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_162, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) = '==>'(0, '==>'(B, B))),
% 3.05/3.33 inference(resolve, [$cnf($equal('==>'('==>'(B, 0), 0), 0))],
% 3.05/3.33 [refute_0_158, refute_0_161])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_163, plain,
% 3.05/3.33 ('==>'(0, '==>'(B, B)) != '==>'(B, B) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) != '==>'(0, '==>'(B, B)) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) = '==>'(B, B)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_109 :
% 3.05/3.33 [bind(X, $fot('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)))),
% 3.05/3.33 bind(Y, $fot('==>'(0, '==>'(B, B)))),
% 3.05/3.33 bind(Z, $fot('==>'(B, B)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_164, plain,
% 3.05/3.33 ('==>'(0, '==>'(B, B)) != '==>'(B, B) |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) = '==>'(B, B)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)),
% 3.05/3.33 '==>'(0, '==>'(B, B))))],
% 3.05/3.33 [refute_0_162, refute_0_163])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_165, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) = '==>'(B, B)),
% 3.05/3.33 inference(resolve, [$cnf($equal('==>'(0, '==>'(B, B)), '==>'(B, B)))],
% 3.05/3.33 [refute_0_144, refute_0_164])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_166, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) != 0 |
% 3.05/3.33 '==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) != '==>'(B, B) |
% 3.05/3.33 '==>'(B, B) = 0),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)),
% 3.05/3.33 0)), [0], $fot('==>'(B, B))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_167, plain,
% 3.05/3.33 ('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)) != 0 | '==>'(B, B) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)),
% 3.05/3.33 '==>'(B, B)))], [refute_0_165, refute_0_166])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_168, plain, ('==>'(B, B) = 0),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal('==>'('==>'('==>'(B, 0), 0), '==>'(B, B)), 0))],
% 3.05/3.33 [refute_0_143, refute_0_167])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_169, plain,
% 3.05/3.33 ('==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17) = 0),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_168 : [bind(B, $fot(skolemFOFtoCNF_X17))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_170, plain,
% 3.05/3.33 (~ greater_equal(X_617, '==>'('==>'(X_617, 1), X_617)) |
% 3.05/3.33 ~ greater_equal('==>'('==>'(X_617, 1), X_617), X_617) |
% 3.05/3.33 X_617 = '==>'('==>'(X_617, 1), X_617)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_37 :
% 3.05/3.33 [bind(X3, $fot(X_617)),
% 3.05/3.33 bind(X4, $fot('==>'('==>'(X_617, 1), X_617)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_171, plain,
% 3.05/3.33 (greater_equal(add(X_28, '==>'(X_28, X_42)), X_42)),
% 3.05/3.33 inference(subst, [], [refute_0_24 : [bind(X_30, $fot(X_42))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_172, plain,
% 3.05/3.33 (~ greater_equal(add(X_28, '==>'(X_28, X_42)), X_42) |
% 3.05/3.33 greater_equal(add(add(X_28, '==>'(X_28, X_42)), X_40),
% 3.05/3.33 add(X_42, X_40))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_42 :
% 3.05/3.33 [bind(X10, $fot(X_40)),
% 3.05/3.33 bind(X8, $fot(add(X_28, '==>'(X_28, X_42)))),
% 3.05/3.33 bind(X9, $fot(X_42))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_173, plain,
% 3.05/3.33 (greater_equal(add(add(X_28, '==>'(X_28, X_42)), X_40),
% 3.05/3.33 add(X_42, X_40))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf(greater_equal(add(X_28, '==>'(X_28, X_42)), X_42))],
% 3.05/3.33 [refute_0_171, refute_0_172])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_174, plain, (add(add(A, B), C) = add(A, add(B, C))),
% 3.05/3.33 inference(canonicalize, [], [normalize_0_26])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_175, plain,
% 3.05/3.33 (add(add(X_28, '==>'(X_28, X_42)), X_40) =
% 3.05/3.33 add(X_28, add('==>'(X_28, X_42), X_40))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_174 :
% 3.05/3.33 [bind(A, $fot(X_28)), bind(B, $fot('==>'(X_28, X_42))),
% 3.05/3.33 bind(C, $fot(X_40))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_176, plain,
% 3.05/3.33 (add(add(X_28, '==>'(X_28, X_42)), X_40) !=
% 3.05/3.33 add(X_28, add('==>'(X_28, X_42), X_40)) |
% 3.05/3.33 ~
% 3.05/3.33 greater_equal(add(add(X_28, '==>'(X_28, X_42)), X_40),
% 3.05/3.33 add(X_42, X_40)) |
% 3.05/3.33 greater_equal(add(X_28, add('==>'(X_28, X_42), X_40)),
% 3.05/3.33 add(X_42, X_40))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf(greater_equal(add(add(X_28, '==>'(X_28, X_42)),
% 3.05/3.33 X_40), add(X_42, X_40))), [0],
% 3.05/3.33 $fot(add(X_28, add('==>'(X_28, X_42), X_40)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_177, plain,
% 3.05/3.33 (~
% 3.05/3.33 greater_equal(add(add(X_28, '==>'(X_28, X_42)), X_40),
% 3.05/3.33 add(X_42, X_40)) |
% 3.05/3.33 greater_equal(add(X_28, add('==>'(X_28, X_42), X_40)),
% 3.05/3.33 add(X_42, X_40))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal(add(add(X_28, '==>'(X_28, X_42)), X_40),
% 3.05/3.33 add(X_28, add('==>'(X_28, X_42), X_40))))],
% 3.05/3.33 [refute_0_175, refute_0_176])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_178, plain,
% 3.05/3.33 (greater_equal(add(X_28, add('==>'(X_28, X_42), X_40)),
% 3.05/3.33 add(X_42, X_40))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf(greater_equal(add(add(X_28, '==>'(X_28, X_42)), X_40),
% 3.05/3.33 add(X_42, X_40)))], [refute_0_173, refute_0_177])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_179, plain,
% 3.05/3.33 (greater_equal(add(X_104, add('==>'(X_104, X_105), X_104)),
% 3.05/3.33 add(X_105, X_104))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_178 :
% 3.05/3.33 [bind(X_28, $fot(X_104)), bind(X_40, $fot(X_104)),
% 3.05/3.33 bind(X_42, $fot(X_105))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_180, plain,
% 3.05/3.33 (add(add(X_11, X_13), X_13) = add(X_11, add(X_13, X_13))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_174 :
% 3.05/3.33 [bind(A, $fot(X_11)), bind(B, $fot(X_13)),
% 3.05/3.33 bind(C, $fot(X_13))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_181, plain, (add(A, A) = A),
% 3.05/3.33 inference(canonicalize, [], [normalize_0_28])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_182, plain, (add(X_13, X_13) = X_13),
% 3.05/3.33 inference(subst, [], [refute_0_181 : [bind(A, $fot(X_13))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_183, plain,
% 3.05/3.33 (add(X_13, X_13) != X_13 |
% 3.05/3.33 add(add(X_11, X_13), X_13) != add(X_11, add(X_13, X_13)) |
% 3.05/3.33 add(add(X_11, X_13), X_13) = add(X_11, X_13)),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal(add(add(X_11, X_13), X_13),
% 3.05/3.33 add(X_11, add(X_13, X_13)))), [1, 1],
% 3.05/3.33 $fot(X_13)]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_184, plain,
% 3.05/3.33 (add(add(X_11, X_13), X_13) != add(X_11, add(X_13, X_13)) |
% 3.05/3.33 add(add(X_11, X_13), X_13) = add(X_11, X_13)),
% 3.05/3.33 inference(resolve, [$cnf($equal(add(X_13, X_13), X_13))],
% 3.05/3.33 [refute_0_182, refute_0_183])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_185, plain, (add(add(X_11, X_13), X_13) = add(X_11, X_13)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal(add(add(X_11, X_13), X_13),
% 3.05/3.33 add(X_11, add(X_13, X_13))))],
% 3.05/3.33 [refute_0_180, refute_0_184])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_186, plain, (add(A, B) != add(B, A) | add(B, A) = add(A, B)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_100 :
% 3.05/3.33 [bind(X, $fot(add(A, B))), bind(Y, $fot(add(B, A)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_187, plain, (add(B, A) = add(A, B)),
% 3.05/3.33 inference(resolve, [$cnf($equal(add(A, B), add(B, A)))],
% 3.05/3.33 [refute_0_27, refute_0_186])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_188, plain,
% 3.05/3.33 (add(add(X_11, X_13), X_13) = add(X_13, add(X_11, X_13))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_187 :
% 3.05/3.33 [bind(A, $fot(X_13)), bind(B, $fot(add(X_11, X_13)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_189, plain,
% 3.05/3.33 (add(add(X_11, X_13), X_13) != add(X_11, X_13) |
% 3.05/3.33 add(add(X_11, X_13), X_13) != add(X_13, add(X_11, X_13)) |
% 3.05/3.33 add(X_13, add(X_11, X_13)) = add(X_11, X_13)),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf($equal(add(add(X_11, X_13), X_13), add(X_11, X_13))),
% 3.05/3.33 [0], $fot(add(X_13, add(X_11, X_13)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_190, plain,
% 3.05/3.33 (add(add(X_11, X_13), X_13) != add(X_11, X_13) |
% 3.05/3.33 add(X_13, add(X_11, X_13)) = add(X_11, X_13)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal(add(add(X_11, X_13), X_13),
% 3.05/3.33 add(X_13, add(X_11, X_13))))],
% 3.05/3.33 [refute_0_188, refute_0_189])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_191, plain, (add(X_13, add(X_11, X_13)) = add(X_11, X_13)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal(add(add(X_11, X_13), X_13), add(X_11, X_13)))],
% 3.05/3.33 [refute_0_185, refute_0_190])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_192, plain,
% 3.05/3.33 (add(X_104, add('==>'(X_104, X_105), X_104)) =
% 3.05/3.33 add('==>'(X_104, X_105), X_104)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_191 :
% 3.05/3.33 [bind(X_11, $fot('==>'(X_104, X_105))),
% 3.05/3.33 bind(X_13, $fot(X_104))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_193, plain,
% 3.05/3.33 (add(X_104, add('==>'(X_104, X_105), X_104)) !=
% 3.05/3.33 add('==>'(X_104, X_105), X_104) |
% 3.05/3.33 ~
% 3.05/3.33 greater_equal(add(X_104, add('==>'(X_104, X_105), X_104)),
% 3.05/3.33 add(X_105, X_104)) |
% 3.05/3.33 greater_equal(add('==>'(X_104, X_105), X_104), add(X_105, X_104))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf(greater_equal(add(X_104,
% 3.05/3.33 add('==>'(X_104, X_105), X_104)),
% 3.05/3.33 add(X_105, X_104))), [0],
% 3.05/3.33 $fot(add('==>'(X_104, X_105), X_104))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_194, plain,
% 3.05/3.33 (~
% 3.05/3.33 greater_equal(add(X_104, add('==>'(X_104, X_105), X_104)),
% 3.05/3.33 add(X_105, X_104)) |
% 3.05/3.33 greater_equal(add('==>'(X_104, X_105), X_104), add(X_105, X_104))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal(add(X_104, add('==>'(X_104, X_105), X_104)),
% 3.05/3.33 add('==>'(X_104, X_105), X_104)))],
% 3.05/3.33 [refute_0_192, refute_0_193])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_195, plain,
% 3.05/3.33 (greater_equal(add('==>'(X_104, X_105), X_104), add(X_105, X_104))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf(greater_equal(add(X_104,
% 3.05/3.33 add('==>'(X_104, X_105), X_104)),
% 3.05/3.33 add(X_105, X_104)))], [refute_0_179, refute_0_194])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_196, plain,
% 3.05/3.33 (add('==>'(X_104, X_105), X_104) = add(X_104, '==>'(X_104, X_105))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_187 :
% 3.05/3.33 [bind(A, $fot(X_104)),
% 3.05/3.33 bind(B, $fot('==>'(X_104, X_105)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_197, plain,
% 3.05/3.33 (add('==>'(X_104, X_105), X_104) != add(X_104, '==>'(X_104, X_105)) |
% 3.05/3.33 ~ greater_equal(add('==>'(X_104, X_105), X_104), add(X_105, X_104)) |
% 3.05/3.33 greater_equal(add(X_104, '==>'(X_104, X_105)), add(X_105, X_104))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf(greater_equal(add('==>'(X_104, X_105), X_104),
% 3.05/3.33 add(X_105, X_104))), [0],
% 3.05/3.33 $fot(add(X_104, '==>'(X_104, X_105)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_198, plain,
% 3.05/3.33 (~ greater_equal(add('==>'(X_104, X_105), X_104), add(X_105, X_104)) |
% 3.05/3.33 greater_equal(add(X_104, '==>'(X_104, X_105)), add(X_105, X_104))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal(add('==>'(X_104, X_105), X_104),
% 3.05/3.33 add(X_104, '==>'(X_104, X_105))))],
% 3.05/3.33 [refute_0_196, refute_0_197])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_199, plain,
% 3.05/3.33 (greater_equal(add(X_104, '==>'(X_104, X_105)), add(X_105, X_104))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf(greater_equal(add('==>'(X_104, X_105), X_104),
% 3.05/3.33 add(X_105, X_104)))], [refute_0_195, refute_0_198])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_200, plain,
% 3.05/3.33 (greater_equal(add(X_186, '==>'(X_186, X_105)), add(X_105, X_186))),
% 3.05/3.33 inference(subst, [], [refute_0_199 : [bind(X_104, $fot(X_186))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_201, plain,
% 3.05/3.33 (~ greater_equal(add(X_186, '==>'(X_186, X_105)), add(X_105, X_186)) |
% 3.05/3.33 greater_equal('==>'(X_186, X_105), '==>'(X_186, add(X_105, X_186)))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_50 :
% 3.05/3.33 [bind(X5, $fot(X_186)), bind(X6, $fot('==>'(X_186, X_105))),
% 3.05/3.33 bind(X7, $fot(add(X_105, X_186)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_202, plain,
% 3.05/3.33 (greater_equal('==>'(X_186, X_105), '==>'(X_186, add(X_105, X_186)))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf(greater_equal(add(X_186, '==>'(X_186, X_105)),
% 3.05/3.33 add(X_105, X_186)))], [refute_0_200, refute_0_201])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_203, plain,
% 3.05/3.33 (greater_equal('==>'('==>'(X_105, X_552), X_105),
% 3.05/3.33 '==>'('==>'(X_105, X_552), add(X_105, '==>'(X_105, X_552))))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_202 : [bind(X_186, $fot('==>'(X_105, X_552)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_204, plain,
% 3.05/3.33 (~ greater_equal(add(X_104, '==>'(X_104, X_105)), add(X_105, X_104)) |
% 3.05/3.33 ~ greater_equal(add(X_105, X_104), add(X_104, '==>'(X_104, X_105))) |
% 3.05/3.33 add(X_104, '==>'(X_104, X_105)) = add(X_105, X_104)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_37 :
% 3.05/3.33 [bind(X3, $fot(add(X_104, '==>'(X_104, X_105)))),
% 3.05/3.33 bind(X4, $fot(add(X_105, X_104)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_205, plain,
% 3.05/3.33 (~ greater_equal(add(X_105, X_104), add(X_104, '==>'(X_104, X_105))) |
% 3.05/3.33 add(X_104, '==>'(X_104, X_105)) = add(X_105, X_104)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf(greater_equal(add(X_104, '==>'(X_104, X_105)),
% 3.05/3.33 add(X_105, X_104)))], [refute_0_199, refute_0_204])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_206, plain,
% 3.05/3.33 (~ greater_equal(X_203, '==>'(X_202, X_203)) |
% 3.05/3.33 greater_equal(add(X_203, X10), add('==>'(X_202, X_203), X10))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_42 :
% 3.05/3.33 [bind(X8, $fot(X_203)),
% 3.05/3.33 bind(X9, $fot('==>'(X_202, X_203)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_207, plain, (greater_equal(X_203, '==>'(X_202, X_203))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_52 :
% 3.05/3.33 [bind(X_186, $fot(X_202)), bind(X_188, $fot(X_203))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_208, plain,
% 3.05/3.33 (greater_equal(add(X_203, X10), add('==>'(X_202, X_203), X10))),
% 3.05/3.33 inference(resolve, [$cnf(greater_equal(X_203, '==>'(X_202, X_203)))],
% 3.05/3.33 [refute_0_207, refute_0_206])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_209, plain,
% 3.05/3.33 (greater_equal(add(X_304, X_302), add('==>'(X_303, X_304), X_302))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_208 :
% 3.05/3.33 [bind(X10, $fot(X_302)), bind(X_202, $fot(X_303)),
% 3.05/3.33 bind(X_203, $fot(X_304))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_210, plain,
% 3.05/3.33 (add(X_302, '==>'(X_303, X_304)) = add('==>'(X_303, X_304), X_302)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_27 :
% 3.05/3.33 [bind(A, $fot(X_302)),
% 3.05/3.33 bind(B, $fot('==>'(X_303, X_304)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_211, plain,
% 3.05/3.33 (add(X_302, '==>'(X_303, X_304)) != add('==>'(X_303, X_304), X_302) |
% 3.05/3.33 add('==>'(X_303, X_304), X_302) = add(X_302, '==>'(X_303, X_304))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_100 :
% 3.05/3.33 [bind(X, $fot(add(X_302, '==>'(X_303, X_304)))),
% 3.05/3.33 bind(Y, $fot(add('==>'(X_303, X_304), X_302)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_212, plain,
% 3.05/3.33 (add('==>'(X_303, X_304), X_302) = add(X_302, '==>'(X_303, X_304))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal(add(X_302, '==>'(X_303, X_304)),
% 3.05/3.33 add('==>'(X_303, X_304), X_302)))],
% 3.05/3.33 [refute_0_210, refute_0_211])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_213, plain,
% 3.05/3.33 (add('==>'(X_303, X_304), X_302) != add(X_302, '==>'(X_303, X_304)) |
% 3.05/3.33 ~ greater_equal(add(X_304, X_302), add('==>'(X_303, X_304), X_302)) |
% 3.05/3.33 greater_equal(add(X_304, X_302), add(X_302, '==>'(X_303, X_304)))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf(greater_equal(add(X_304, X_302),
% 3.05/3.33 add('==>'(X_303, X_304), X_302))), [1],
% 3.05/3.33 $fot(add(X_302, '==>'(X_303, X_304)))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_214, plain,
% 3.05/3.33 (~ greater_equal(add(X_304, X_302), add('==>'(X_303, X_304), X_302)) |
% 3.05/3.33 greater_equal(add(X_304, X_302), add(X_302, '==>'(X_303, X_304)))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal(add('==>'(X_303, X_304), X_302),
% 3.05/3.33 add(X_302, '==>'(X_303, X_304))))],
% 3.05/3.33 [refute_0_212, refute_0_213])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_215, plain,
% 3.05/3.33 (greater_equal(add(X_304, X_302), add(X_302, '==>'(X_303, X_304)))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf(greater_equal(add(X_304, X_302),
% 3.05/3.33 add('==>'(X_303, X_304), X_302)))],
% 3.05/3.33 [refute_0_209, refute_0_214])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_216, plain,
% 3.05/3.33 (greater_equal(add(X_105, X_104), add(X_104, '==>'(X_104, X_105)))),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_215 :
% 3.05/3.33 [bind(X_302, $fot(X_104)), bind(X_303, $fot(X_104)),
% 3.05/3.33 bind(X_304, $fot(X_105))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_217, plain,
% 3.05/3.33 (add(X_104, '==>'(X_104, X_105)) = add(X_105, X_104)),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf(greater_equal(add(X_105, X_104),
% 3.05/3.33 add(X_104, '==>'(X_104, X_105))))],
% 3.05/3.33 [refute_0_216, refute_0_205])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_218, plain,
% 3.05/3.33 (add(X_105, '==>'(X_105, X_552)) = add(X_552, X_105)),
% 3.05/3.33 inference(subst, [],
% 3.05/3.33 [refute_0_217 :
% 3.05/3.33 [bind(X_104, $fot(X_105)), bind(X_105, $fot(X_552))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_219, plain,
% 3.05/3.33 (add(X_105, '==>'(X_105, X_552)) != add(X_552, X_105) |
% 3.05/3.33 ~
% 3.05/3.33 greater_equal('==>'('==>'(X_105, X_552), X_105),
% 3.05/3.33 '==>'('==>'(X_105, X_552), add(X_105, '==>'(X_105, X_552)))) |
% 3.05/3.33 greater_equal('==>'('==>'(X_105, X_552), X_105),
% 3.05/3.33 '==>'('==>'(X_105, X_552), add(X_552, X_105)))),
% 3.05/3.33 introduced(tautology,
% 3.05/3.33 [equality,
% 3.05/3.33 [$cnf(greater_equal('==>'('==>'(X_105, X_552), X_105),
% 3.05/3.33 '==>'('==>'(X_105, X_552),
% 3.05/3.33 add(X_105, '==>'(X_105, X_552))))), [1, 1],
% 3.05/3.33 $fot(add(X_552, X_105))]])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_220, plain,
% 3.05/3.33 (~
% 3.05/3.33 greater_equal('==>'('==>'(X_105, X_552), X_105),
% 3.05/3.33 '==>'('==>'(X_105, X_552), add(X_105, '==>'(X_105, X_552)))) |
% 3.05/3.33 greater_equal('==>'('==>'(X_105, X_552), X_105),
% 3.05/3.33 '==>'('==>'(X_105, X_552), add(X_552, X_105)))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf($equal(add(X_105, '==>'(X_105, X_552)),
% 3.05/3.33 add(X_552, X_105)))], [refute_0_218, refute_0_219])).
% 3.05/3.33
% 3.05/3.33 cnf(refute_0_221, plain,
% 3.05/3.33 (greater_equal('==>'('==>'(X_105, X_552), X_105),
% 3.05/3.33 '==>'('==>'(X_105, X_552), add(X_552, X_105)))),
% 3.05/3.33 inference(resolve,
% 3.05/3.33 [$cnf(greater_equal('==>'('==>'(X_105, X_552), X_105),
% 3.05/3.33 '==>'('==>'(X_105, X_552),
% 3.05/3.33 add(X_105, '==>'(X_105, X_552)))))],
% 3.05/3.33 [refute_0_203, refute_0_220])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_222, plain,
% 3.05/3.34 (greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), add(1, X_615)))),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_221 :
% 3.05/3.34 [bind(X_105, $fot(X_615)), bind(X_552, $fot(1))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_223, plain, (add(A, 1) = 1),
% 3.05/3.34 inference(canonicalize, [], [normalize_0_30])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_224, plain, (add(A, 1) = add(1, A)),
% 3.05/3.34 inference(subst, [], [refute_0_27 : [bind(B, $fot(1))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_225, plain,
% 3.05/3.34 (add(A, 1) != add(1, A) | add(A, 1) != 1 | add(1, A) = 1),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf($equal(add(A, 1), 1)), [0], $fot(add(1, A))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_226, plain, (add(A, 1) != 1 | add(1, A) = 1),
% 3.05/3.34 inference(resolve, [$cnf($equal(add(A, 1), add(1, A)))],
% 3.05/3.34 [refute_0_224, refute_0_225])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_227, plain, (add(1, A) = 1),
% 3.05/3.34 inference(resolve, [$cnf($equal(add(A, 1), 1))],
% 3.05/3.34 [refute_0_223, refute_0_226])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_228, plain, (add(1, X_615) = 1),
% 3.05/3.34 inference(subst, [], [refute_0_227 : [bind(A, $fot(X_615))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_229, plain,
% 3.05/3.34 (add(1, X_615) != 1 |
% 3.05/3.34 ~
% 3.05/3.34 greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), add(1, X_615))) |
% 3.05/3.34 greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), 1))),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), add(1, X_615)))), [1, 1],
% 3.05/3.34 $fot(1)]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_230, plain,
% 3.05/3.34 (~
% 3.05/3.34 greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), add(1, X_615))) |
% 3.05/3.34 greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), 1))),
% 3.05/3.34 inference(resolve, [$cnf($equal(add(1, X_615), 1))],
% 3.05/3.34 [refute_0_228, refute_0_229])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_231, plain,
% 3.05/3.34 (greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), 1))),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), add(1, X_615))))],
% 3.05/3.34 [refute_0_222, refute_0_230])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_232, plain,
% 3.05/3.34 (~ greater_equal(X_553, '==>'('==>'(X_553, 1), 1)) |
% 3.05/3.34 ~ greater_equal('==>'('==>'(X_553, 1), 1), X_553) |
% 3.05/3.34 X_553 = '==>'('==>'(X_553, 1), 1)),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_37 :
% 3.05/3.34 [bind(X3, $fot(X_553)),
% 3.05/3.34 bind(X4, $fot('==>'('==>'(X_553, 1), 1)))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_233, plain,
% 3.05/3.34 (~ greater_equal(add(1, X_187), X_188) |
% 3.05/3.34 greater_equal(X_187, '==>'(1, X_188))),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_50 :
% 3.05/3.34 [bind(X5, $fot(1)), bind(X6, $fot(X_187)),
% 3.05/3.34 bind(X7, $fot(X_188))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_234, plain, (add(1, X_187) = 1),
% 3.05/3.34 inference(subst, [], [refute_0_227 : [bind(A, $fot(X_187))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_235, plain,
% 3.05/3.34 (add(1, X_187) != 1 | ~ greater_equal(1, X_188) |
% 3.05/3.34 greater_equal(add(1, X_187), X_188)),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf(~ greater_equal(add(1, X_187), X_188)), [0],
% 3.05/3.34 $fot(1)]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_236, plain,
% 3.05/3.34 (~ greater_equal(1, X_188) | greater_equal(add(1, X_187), X_188)),
% 3.05/3.34 inference(resolve, [$cnf($equal(add(1, X_187), 1))],
% 3.05/3.34 [refute_0_234, refute_0_235])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_237, plain,
% 3.05/3.34 (~ greater_equal(1, X_188) | greater_equal(X_187, '==>'(1, X_188))),
% 3.05/3.34 inference(resolve, [$cnf(greater_equal(add(1, X_187), X_188))],
% 3.05/3.34 [refute_0_236, refute_0_233])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_238, plain, (greater_equal(add(1, '==>'(1, X_32)), X_32)),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_24 :
% 3.05/3.34 [bind(X_28, $fot(1)), bind(X_30, $fot(X_32))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_239, plain, (add(1, '==>'(1, X_32)) = 1),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_227 : [bind(A, $fot('==>'(1, X_32)))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_240, plain,
% 3.05/3.34 (add(1, '==>'(1, X_32)) != 1 |
% 3.05/3.34 ~ greater_equal(add(1, '==>'(1, X_32)), X_32) |
% 3.05/3.34 greater_equal(1, X_32)),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf(greater_equal(add(1, '==>'(1, X_32)), X_32)), [0],
% 3.05/3.34 $fot(1)]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_241, plain,
% 3.05/3.34 (~ greater_equal(add(1, '==>'(1, X_32)), X_32) |
% 3.05/3.34 greater_equal(1, X_32)),
% 3.05/3.34 inference(resolve, [$cnf($equal(add(1, '==>'(1, X_32)), 1))],
% 3.05/3.34 [refute_0_239, refute_0_240])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_242, plain, (greater_equal(1, X_32)),
% 3.05/3.34 inference(resolve, [$cnf(greater_equal(add(1, '==>'(1, X_32)), X_32))],
% 3.05/3.34 [refute_0_238, refute_0_241])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_243, plain, (greater_equal(1, X_188)),
% 3.05/3.34 inference(subst, [], [refute_0_242 : [bind(X_32, $fot(X_188))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_244, plain, (greater_equal(X_187, '==>'(1, X_188))),
% 3.05/3.34 inference(resolve, [$cnf(greater_equal(1, X_188))],
% 3.05/3.34 [refute_0_243, refute_0_237])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_245, plain, (greater_equal(X_409, '==>'(1, X_188))),
% 3.05/3.34 inference(subst, [], [refute_0_244 : [bind(X_187, $fot(X_409))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_246, plain,
% 3.05/3.34 (~ greater_equal(X_409, '==>'(1, X_188)) |
% 3.05/3.34 greater_equal('==>'('==>'(1, X_188), X_411), '==>'(X_409, X_411))),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_67 :
% 3.05/3.34 [bind(X11, $fot(X_409)), bind(X12, $fot('==>'(1, X_188))),
% 3.05/3.34 bind(X13, $fot(X_411))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_247, plain,
% 3.05/3.34 (greater_equal('==>'('==>'(1, X_188), X_411), '==>'(X_409, X_411))),
% 3.05/3.34 inference(resolve, [$cnf(greater_equal(X_409, '==>'(1, X_188)))],
% 3.05/3.34 [refute_0_245, refute_0_246])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_248, plain,
% 3.05/3.34 (greater_equal('==>'('==>'(1, X_422), X_422), '==>'(X_421, X_422))),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_247 :
% 3.05/3.34 [bind(X_188, $fot(X_422)), bind(X_409, $fot(X_421)),
% 3.05/3.34 bind(X_411, $fot(X_422))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_249, plain,
% 3.05/3.34 ('==>'('==>'(X_422, 1), 1) = '==>'('==>'(1, X_422), X_422)),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_1 : [bind(A, $fot(X_422)), bind(B, $fot(1))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_250, plain,
% 3.05/3.34 ('==>'('==>'(X_422, 1), 1) != '==>'('==>'(1, X_422), X_422) |
% 3.05/3.34 '==>'('==>'(1, X_422), X_422) = '==>'('==>'(X_422, 1), 1)),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_100 :
% 3.05/3.34 [bind(X, $fot('==>'('==>'(X_422, 1), 1))),
% 3.05/3.34 bind(Y, $fot('==>'('==>'(1, X_422), X_422)))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_251, plain,
% 3.05/3.34 ('==>'('==>'(1, X_422), X_422) = '==>'('==>'(X_422, 1), 1)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'('==>'(X_422, 1), 1),
% 3.05/3.34 '==>'('==>'(1, X_422), X_422)))],
% 3.05/3.34 [refute_0_249, refute_0_250])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_252, plain,
% 3.05/3.34 ('==>'('==>'(1, X_422), X_422) != '==>'('==>'(X_422, 1), 1) |
% 3.05/3.34 ~ greater_equal('==>'('==>'(1, X_422), X_422), '==>'(X_421, X_422)) |
% 3.05/3.34 greater_equal('==>'('==>'(X_422, 1), 1), '==>'(X_421, X_422))),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(1, X_422), X_422),
% 3.05/3.34 '==>'(X_421, X_422))), [0],
% 3.05/3.34 $fot('==>'('==>'(X_422, 1), 1))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_253, plain,
% 3.05/3.34 (~ greater_equal('==>'('==>'(1, X_422), X_422), '==>'(X_421, X_422)) |
% 3.05/3.34 greater_equal('==>'('==>'(X_422, 1), 1), '==>'(X_421, X_422))),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'('==>'(1, X_422), X_422),
% 3.05/3.34 '==>'('==>'(X_422, 1), 1)))],
% 3.05/3.34 [refute_0_251, refute_0_252])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_254, plain,
% 3.05/3.34 (greater_equal('==>'('==>'(X_422, 1), 1), '==>'(X_421, X_422))),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(1, X_422), X_422),
% 3.05/3.34 '==>'(X_421, X_422)))],
% 3.05/3.34 [refute_0_248, refute_0_253])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_255, plain,
% 3.05/3.34 (greater_equal('==>'('==>'(X_422, 1), 1), '==>'(0, X_422))),
% 3.05/3.34 inference(subst, [], [refute_0_254 : [bind(X_421, $fot(0))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_256, plain, ('==>'(0, X_422) = X_422),
% 3.05/3.34 inference(subst, [], [refute_0_54 : [bind(X_542, $fot(X_422))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_257, plain,
% 3.05/3.34 ('==>'(0, X_422) != X_422 |
% 3.05/3.34 ~ greater_equal('==>'('==>'(X_422, 1), 1), '==>'(0, X_422)) |
% 3.05/3.34 greater_equal('==>'('==>'(X_422, 1), 1), X_422)),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(X_422, 1), 1),
% 3.05/3.34 '==>'(0, X_422))), [1], $fot(X_422)]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_258, plain,
% 3.05/3.34 (~ greater_equal('==>'('==>'(X_422, 1), 1), '==>'(0, X_422)) |
% 3.05/3.34 greater_equal('==>'('==>'(X_422, 1), 1), X_422)),
% 3.05/3.34 inference(resolve, [$cnf($equal('==>'(0, X_422), X_422))],
% 3.05/3.34 [refute_0_256, refute_0_257])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_259, plain, (greater_equal('==>'('==>'(X_422, 1), 1), X_422)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(X_422, 1), 1),
% 3.05/3.34 '==>'(0, X_422)))], [refute_0_255, refute_0_258])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_260, plain, (greater_equal('==>'('==>'(X_553, 1), 1), X_553)),
% 3.05/3.34 inference(subst, [], [refute_0_259 : [bind(X_422, $fot(X_553))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_261, plain,
% 3.05/3.34 (~ greater_equal(X_553, '==>'('==>'(X_553, 1), 1)) |
% 3.05/3.34 X_553 = '==>'('==>'(X_553, 1), 1)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(X_553, 1), 1), X_553))],
% 3.05/3.34 [refute_0_260, refute_0_232])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_262, plain,
% 3.05/3.34 (greater_equal(X_203, '==>'('==>'(B, X_203), X_203))),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_52 :
% 3.05/3.34 [bind(X_186, $fot('==>'(B, X_203))),
% 3.05/3.34 bind(X_188, $fot(X_203))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_263, plain,
% 3.05/3.34 ('==>'('==>'(X_203, B), B) = '==>'('==>'(B, X_203), X_203)),
% 3.05/3.34 inference(subst, [], [refute_0_1 : [bind(A, $fot(X_203))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_264, plain,
% 3.05/3.34 ('==>'('==>'(X_203, B), B) != '==>'('==>'(B, X_203), X_203) |
% 3.05/3.34 '==>'('==>'(B, X_203), X_203) = '==>'('==>'(X_203, B), B)),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_100 :
% 3.05/3.34 [bind(X, $fot('==>'('==>'(X_203, B), B))),
% 3.05/3.34 bind(Y, $fot('==>'('==>'(B, X_203), X_203)))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_265, plain,
% 3.05/3.34 ('==>'('==>'(B, X_203), X_203) = '==>'('==>'(X_203, B), B)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'('==>'(X_203, B), B),
% 3.05/3.34 '==>'('==>'(B, X_203), X_203)))],
% 3.05/3.34 [refute_0_263, refute_0_264])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_266, plain,
% 3.05/3.34 ('==>'('==>'(B, X_203), X_203) != '==>'('==>'(X_203, B), B) |
% 3.05/3.34 ~ greater_equal(X_203, '==>'('==>'(B, X_203), X_203)) |
% 3.05/3.34 greater_equal(X_203, '==>'('==>'(X_203, B), B))),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf(greater_equal(X_203, '==>'('==>'(B, X_203), X_203))),
% 3.05/3.34 [1], $fot('==>'('==>'(X_203, B), B))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_267, plain,
% 3.05/3.34 (~ greater_equal(X_203, '==>'('==>'(B, X_203), X_203)) |
% 3.05/3.34 greater_equal(X_203, '==>'('==>'(X_203, B), B))),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'('==>'(B, X_203), X_203),
% 3.05/3.34 '==>'('==>'(X_203, B), B)))],
% 3.05/3.34 [refute_0_265, refute_0_266])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_268, plain, (greater_equal(X_203, '==>'('==>'(X_203, B), B))),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf(greater_equal(X_203, '==>'('==>'(B, X_203), X_203)))],
% 3.05/3.34 [refute_0_262, refute_0_267])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_269, plain, (greater_equal(X_553, '==>'('==>'(X_553, 1), 1))),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_268 :
% 3.05/3.34 [bind(B, $fot(1)), bind(X_203, $fot(X_553))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_270, plain, (X_553 = '==>'('==>'(X_553, 1), 1)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf(greater_equal(X_553, '==>'('==>'(X_553, 1), 1)))],
% 3.05/3.34 [refute_0_269, refute_0_261])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_271, plain,
% 3.05/3.34 (X_553 != '==>'('==>'(X_553, 1), 1) |
% 3.05/3.34 '==>'('==>'(X_553, 1), 1) = X_553),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_100 :
% 3.05/3.34 [bind(X, $fot(X_553)),
% 3.05/3.34 bind(Y, $fot('==>'('==>'(X_553, 1), 1)))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_272, plain, ('==>'('==>'(X_553, 1), 1) = X_553),
% 3.05/3.34 inference(resolve, [$cnf($equal(X_553, '==>'('==>'(X_553, 1), 1)))],
% 3.05/3.34 [refute_0_270, refute_0_271])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_273, plain, ('==>'('==>'(X_615, 1), 1) = X_615),
% 3.05/3.34 inference(subst, [], [refute_0_272 : [bind(X_553, $fot(X_615))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_274, plain,
% 3.05/3.34 ('==>'('==>'(X_615, 1), 1) != X_615 |
% 3.05/3.34 ~
% 3.05/3.34 greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), 1)) |
% 3.05/3.34 greater_equal('==>'('==>'(X_615, 1), X_615), X_615)),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), 1))), [1], $fot(X_615)]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_275, plain,
% 3.05/3.34 (~
% 3.05/3.34 greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), 1)) |
% 3.05/3.34 greater_equal('==>'('==>'(X_615, 1), X_615), X_615)),
% 3.05/3.34 inference(resolve, [$cnf($equal('==>'('==>'(X_615, 1), 1), X_615))],
% 3.05/3.34 [refute_0_273, refute_0_274])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_276, plain,
% 3.05/3.34 (greater_equal('==>'('==>'(X_615, 1), X_615), X_615)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(X_615, 1), X_615),
% 3.05/3.34 '==>'('==>'(X_615, 1), 1)))],
% 3.05/3.34 [refute_0_231, refute_0_275])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_277, plain,
% 3.05/3.34 (greater_equal('==>'('==>'(X_617, 1), X_617), X_617)),
% 3.05/3.34 inference(subst, [], [refute_0_276 : [bind(X_615, $fot(X_617))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_278, plain,
% 3.05/3.34 (~ greater_equal(X_617, '==>'('==>'(X_617, 1), X_617)) |
% 3.05/3.34 X_617 = '==>'('==>'(X_617, 1), X_617)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf(greater_equal('==>'('==>'(X_617, 1), X_617), X_617))],
% 3.05/3.34 [refute_0_277, refute_0_170])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_279, plain,
% 3.05/3.34 (greater_equal(X_617, '==>'('==>'(X_617, 1), X_617))),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_52 :
% 3.05/3.34 [bind(X_186, $fot('==>'(X_617, 1))),
% 3.05/3.34 bind(X_188, $fot(X_617))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_280, plain, (X_617 = '==>'('==>'(X_617, 1), X_617)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf(greater_equal(X_617, '==>'('==>'(X_617, 1), X_617)))],
% 3.05/3.34 [refute_0_279, refute_0_278])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_281, plain,
% 3.05/3.34 (X_617 != '==>'('==>'(X_617, 1), X_617) |
% 3.05/3.34 '==>'('==>'(X_617, 1), X_617) = X_617),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_100 :
% 3.05/3.34 [bind(X, $fot(X_617)),
% 3.05/3.34 bind(Y, $fot('==>'('==>'(X_617, 1), X_617)))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_282, plain, ('==>'('==>'(X_617, 1), X_617) = X_617),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal(X_617, '==>'('==>'(X_617, 1), X_617)))],
% 3.05/3.34 [refute_0_280, refute_0_281])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_283, plain,
% 3.05/3.34 ('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17) =
% 3.05/3.34 skolemFOFtoCNF_X17),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_282 : [bind(X_617, $fot(skolemFOFtoCNF_X17))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_284, plain,
% 3.05/3.34 ('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) =
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17)),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [refl,
% 3.05/3.34 [$fot('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_285, plain,
% 3.05/3.34 ('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) !=
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) |
% 3.05/3.34 '==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17) !=
% 3.05/3.34 skolemFOFtoCNF_X17 |
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) =
% 3.05/3.34 '==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17)),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf($equal('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17),
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17))),
% 3.05/3.34 [1, 0], $fot(skolemFOFtoCNF_X17)]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_286, plain,
% 3.05/3.34 ('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17) !=
% 3.05/3.34 skolemFOFtoCNF_X17 |
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) =
% 3.05/3.34 '==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17),
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17)))],
% 3.05/3.34 [refute_0_284, refute_0_285])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_287, plain,
% 3.05/3.34 ('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) =
% 3.05/3.34 '==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17)),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17))],
% 3.05/3.34 [refute_0_283, refute_0_286])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_288, plain,
% 3.05/3.34 ('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) !=
% 3.05/3.34 '==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17) |
% 3.05/3.34 '==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17) != 0 |
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) = 0),
% 3.05/3.34 inference(subst, [],
% 3.05/3.34 [refute_0_109 :
% 3.05/3.34 [bind(X,
% 3.05/3.34 $fot('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17))),
% 3.05/3.34 bind(Y,
% 3.05/3.34 $fot('==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17))),
% 3.05/3.34 bind(Z, $fot(0))]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_289, plain,
% 3.05/3.34 ('==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17) != 0 |
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) = 0),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17),
% 3.05/3.34 '==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17)))],
% 3.05/3.34 [refute_0_287, refute_0_288])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_290, plain,
% 3.05/3.34 ('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) = 0),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'(skolemFOFtoCNF_X17, skolemFOFtoCNF_X17),
% 3.05/3.34 0))], [refute_0_169, refute_0_289])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_291, plain,
% 3.05/3.34 (0 != 0 |
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) != 0 |
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) = 0),
% 3.05/3.34 introduced(tautology,
% 3.05/3.34 [equality,
% 3.05/3.34 [$cnf($equal('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17), 0)),
% 3.05/3.34 [1], $fot(0)]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_292, plain,
% 3.05/3.34 (0 != 0 |
% 3.05/3.34 '==>'('==>'('==>'(skolemFOFtoCNF_X17, 1), skolemFOFtoCNF_X17),
% 3.05/3.34 skolemFOFtoCNF_X17) = 0),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17), 0))],
% 3.05/3.34 [refute_0_290, refute_0_291])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_293, plain, (0 != 0),
% 3.05/3.34 inference(resolve,
% 3.05/3.34 [$cnf($equal('==>'('==>'('==>'(skolemFOFtoCNF_X17, 1),
% 3.05/3.34 skolemFOFtoCNF_X17), skolemFOFtoCNF_X17), 0))],
% 3.05/3.34 [refute_0_292, refute_0_0])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_294, plain, (0 = 0),
% 3.05/3.34 introduced(tautology, [refl, [$fot(0)]])).
% 3.05/3.34
% 3.05/3.34 cnf(refute_0_295, plain, ($false),
% 3.05/3.34 inference(resolve, [$cnf($equal(0, 0))],
% 3.05/3.34 [refute_0_294, refute_0_293])).
% 3.05/3.34 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.05/3.34
%------------------------------------------------------------------------------