Twee---2.7.UNS-Prf.s

%------------------------------------------------------------------------------
% File     : Twee---2.7
% Problem  : LCL068-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n007.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 : Tue Sep 29 11:48:57 AM UTC 2026

% Result   : Unsatisfiable 49.08s 6.74s
% Output   : Proof 63.92s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : LCL068-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.07  % Command  : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45  % Computer : n007.cluster.edu
% 0.19/0.45  % Model    : x86_64 x86_64
% 0.19/0.45  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45  % Memory   : 8046.5625MB
% 0.19/0.45  % OS       : Linux 6.8.0-71-generic
% 0.19/0.45  % CPULimit : 300
% 0.19/0.45  % WCLimit  : 300
% 0.19/0.45  % DateTime : Sun Sep 27 15:18:39 UTC 2026
% 0.19/0.45  % CPUTime  : 
% 0.19/0.45  Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 49.08/6.74  Command-line arguments: --flatten --complete-subsets
% 49.08/6.74  
% 49.08/6.74  % SZS status Unsatisfiable
% 49.08/6.74  
% 59.94/8.13  % SZS output start Proof
% 59.94/8.13  Axiom 1 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 59.94/8.13  Axiom 2 (cn_19): is_a_theorem(implies(implies(implies(X, Y), Z), implies(Y, Z))) = true.
% 59.94/8.13  Axiom 3 (cn_37): is_a_theorem(implies(implies(implies(X, Y), Z), implies(not(X), Z))) = true.
% 59.94/8.13  Axiom 4 (condensed_detachment): ifeq(is_a_theorem(implies(X, Y)), true, ifeq(is_a_theorem(X), true, is_a_theorem(Y), true), true) = true.
% 59.94/8.16  Axiom 5 (cn_59): is_a_theorem(implies(implies(not(X), Y), implies(implies(Z, Y), implies(implies(X, Z), Y)))) = true.
% 59.94/8.16  
% 59.94/8.16  Goal 1 (prove_cn_2): is_a_theorem(implies(implies(not(a), a), a)) = true.
% 59.94/8.16  Proof:
% 59.94/8.16    is_a_theorem(implies(implies(not(a), a), a))
% 59.94/8.16  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.16    ifeq(true, true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.16  = { by axiom 4 (condensed_detachment) R->L }
% 59.94/8.16    ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true, ifeq(is_a_theorem(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a))), true, is_a_theorem(implies(a, a)), true), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.16  = { by axiom 2 (cn_19) }
% 59.94/8.16    ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true, ifeq(true, true, is_a_theorem(implies(a, a)), true), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.17  = { by axiom 1 (ifeq_axiom) }
% 59.94/8.17    ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.17  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.17    ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.17  = { by axiom 4 (condensed_detachment) R->L }
% 59.94/8.17    ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a)), implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))))), true, ifeq(is_a_theorem(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a))), true, is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true), true), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.17  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.17    ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a)), implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))))), true, ifeq(ifeq(true, true, is_a_theorem(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a))), true), true, is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true), true), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.17  = { by axiom 2 (cn_19) R->L }
% 59.94/8.17    ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a)), implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), a), implies(a, a))), true, is_a_theorem(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a))), true), true, is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true), true), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.18  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.18    ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a)), implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))))), true, ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), a), implies(a, a))), true, is_a_theorem(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a))), true), true), true, is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true), true), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.18  = { by axiom 3 (cn_37) R->L }
% 59.94/8.18    ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a)), implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(implies(X, implies(Y, a)), a), a), implies(a, a)), implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a)))), true, ifeq(is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), a), implies(a, a))), true, is_a_theorem(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a))), true), true), true, is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true), true), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.18  = { by axiom 4 (condensed_detachment) }
% 59.94/8.18    ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a)), implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))))), true, ifeq(true, true, is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true), true), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.18  = { by axiom 1 (ifeq_axiom) }
% 59.94/8.18    ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(X, implies(Y, a)), a)), implies(a, a)), implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))))), true, is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.19  = { by axiom 5 (cn_59) }
% 59.94/8.19    ifeq(ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.19  = { by axiom 1 (ifeq_axiom) }
% 59.94/8.19    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.19  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.19    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true, ifeq(true, true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.19  = { by axiom 2 (cn_19) R->L }
% 59.94/8.19    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(Y, a), a), implies(a, a)), implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a)))), true, ifeq(is_a_theorem(implies(implies(implies(Y, a), a), implies(a, a))), true, is_a_theorem(implies(implies(implies(implies(X, implies(Y, a)), a), implies(implies(Y, a), a)), implies(a, a))), true), true), true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.19  = { by axiom 4 (condensed_detachment) }
% 59.94/8.19    ifeq(ifeq(true, true, is_a_theorem(implies(a, a)), true), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.19  = { by axiom 1 (ifeq_axiom) }
% 59.94/8.19    ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true)
% 59.94/8.19  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.19    ifeq(true, true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.19  = { by axiom 4 (condensed_detachment) R->L }
% 59.94/8.19    ifeq(ifeq(is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true, ifeq(is_a_theorem(implies(a, implies(implies(not(a), a), a))), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.19  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.19    ifeq(ifeq(is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true, ifeq(ifeq(true, true, is_a_theorem(implies(a, implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.20  = { by axiom 2 (cn_19) R->L }
% 59.94/8.20    ifeq(ifeq(is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(Z, implies(not(a), a)), a), implies(implies(not(a), a), a))), true, is_a_theorem(implies(a, implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.20  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.20    ifeq(ifeq(is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true, ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(implies(Z, implies(not(a), a)), a), implies(implies(not(a), a), a))), true, is_a_theorem(implies(a, implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.20  = { by axiom 2 (cn_19) R->L }
% 59.94/8.20    ifeq(ifeq(is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(Z, implies(not(a), a)), a), implies(implies(not(a), a), a)), implies(a, implies(implies(not(a), a), a)))), true, ifeq(is_a_theorem(implies(implies(implies(Z, implies(not(a), a)), a), implies(implies(not(a), a), a))), true, is_a_theorem(implies(a, implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.20  = { by axiom 4 (condensed_detachment) }
% 59.94/8.20    ifeq(ifeq(is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true, ifeq(true, true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.20  = { by axiom 1 (ifeq_axiom) }
% 59.94/8.20    ifeq(ifeq(is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.20  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.20    ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.20  = { by axiom 5 (cn_59) R->L }
% 59.94/8.20    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 59.94/8.20  = { by axiom 1 (ifeq_axiom) R->L }
% 59.94/8.20    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(true, true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.21  = { by axiom 4 (condensed_detachment) R->L }
% 60.76/8.21    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.21  = { by axiom 1 (ifeq_axiom) R->L }
% 60.76/8.22    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.22  = { by axiom 4 (condensed_detachment) R->L }
% 60.76/8.22    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(is_a_theorem(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.23  = { by axiom 1 (ifeq_axiom) R->L }
% 60.76/8.23    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(ifeq(true, true, is_a_theorem(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.23  = { by axiom 4 (condensed_detachment) R->L }
% 60.76/8.24    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(W, not(a)), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(implies(implies(W, not(a)), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.24  = { by axiom 2 (cn_19) }
% 60.76/8.25    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(implies(W, not(a)), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.25  = { by axiom 1 (ifeq_axiom) }
% 60.76/8.25    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(W, not(a)), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.26  = { by axiom 2 (cn_19) }
% 60.76/8.26    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.27  = { by axiom 1 (ifeq_axiom) }
% 60.76/8.27    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.28  = { by axiom 1 (ifeq_axiom) R->L }
% 60.76/8.28    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.28  = { by axiom 3 (cn_37) R->L }
% 60.76/8.29    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.29  = { by axiom 4 (condensed_detachment) }
% 60.76/8.29    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(true, true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.29  = { by axiom 1 (ifeq_axiom) }
% 60.76/8.29    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(not(a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))))), true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.30  = { by axiom 5 (cn_59) }
% 60.76/8.30    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 60.76/8.30  = { by axiom 1 (ifeq_axiom) }
% 60.76/8.31    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 61.55/8.31  = { by axiom 1 (ifeq_axiom) R->L }
% 61.55/8.31    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(true, true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 61.55/8.32  = { by axiom 4 (condensed_detachment) R->L }
% 61.55/8.32    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 61.55/8.32  = { by axiom 2 (cn_19) }
% 61.55/8.32    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(true, true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 61.55/8.33  = { by axiom 1 (ifeq_axiom) }
% 61.55/8.33    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 61.55/8.35  = { by axiom 1 (ifeq_axiom) R->L }
% 61.55/8.35    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 61.55/8.36  = { by axiom 4 (condensed_detachment) R->L }
% 61.55/8.37    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(is_a_theorem(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 61.55/8.38  = { by axiom 1 (ifeq_axiom) R->L }
% 61.55/8.39    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(ifeq(true, true, is_a_theorem(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 61.55/8.40  = { by axiom 2 (cn_19) R->L }
% 62.35/8.41    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 62.35/8.42  = { by axiom 1 (ifeq_axiom) R->L }
% 62.35/8.43    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 62.35/8.43  = { by axiom 3 (cn_37) R->L }
% 62.35/8.44    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 62.35/8.45  = { by axiom 4 (condensed_detachment) }
% 62.35/8.46    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(true, true, is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 62.35/8.47  = { by axiom 1 (ifeq_axiom) }
% 62.35/8.47    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 62.35/8.48  = { by axiom 5 (cn_59) }
% 62.35/8.49    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 62.35/8.49  = { by axiom 1 (ifeq_axiom) }
% 62.35/8.49    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 62.35/8.50  = { by axiom 1 (ifeq_axiom) R->L }
% 62.35/8.50    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(true, true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 62.35/8.50  = { by axiom 2 (cn_19) R->L }
% 63.12/8.51    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(is_a_theorem(implies(implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(implies(implies(V, implies(U, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(U, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.51  = { by axiom 4 (condensed_detachment) }
% 63.12/8.51    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(true, true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.51  = { by axiom 1 (ifeq_axiom) }
% 63.12/8.51    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.51  = { by axiom 4 (condensed_detachment) }
% 63.12/8.52    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.52  = { by axiom 1 (ifeq_axiom) }
% 63.12/8.52    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.52  = { by axiom 1 (ifeq_axiom) R->L }
% 63.12/8.52    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.52  = { by axiom 4 (condensed_detachment) R->L }
% 63.12/8.52    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.52  = { by axiom 5 (cn_59) }
% 63.12/8.53    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.53  = { by axiom 1 (ifeq_axiom) }
% 63.12/8.53    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.53  = { by axiom 1 (ifeq_axiom) R->L }
% 63.12/8.53    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.54  = { by axiom 4 (condensed_detachment) R->L }
% 63.12/8.54    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.54  = { by axiom 2 (cn_19) }
% 63.12/8.55    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(true, true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.56  = { by axiom 1 (ifeq_axiom) }
% 63.12/8.56    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.57  = { by axiom 1 (ifeq_axiom) R->L }
% 63.12/8.57    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.58  = { by axiom 4 (condensed_detachment) R->L }
% 63.12/8.59    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(is_a_theorem(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.12/8.60  = { by axiom 1 (ifeq_axiom) R->L }
% 63.92/8.61    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(ifeq(true, true, is_a_theorem(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.62  = { by axiom 2 (cn_19) R->L }
% 63.92/8.63    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.64  = { by axiom 1 (ifeq_axiom) R->L }
% 63.92/8.64    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.65  = { by axiom 3 (cn_37) R->L }
% 63.92/8.67    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.67  = { by axiom 4 (condensed_detachment) }
% 63.92/8.67    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, ifeq(true, true, is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.68  = { by axiom 1 (ifeq_axiom) }
% 63.92/8.68    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))))), true, is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.69  = { by axiom 5 (cn_59) }
% 63.92/8.69    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.70  = { by axiom 1 (ifeq_axiom) }
% 63.92/8.70    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.70  = { by axiom 1 (ifeq_axiom) R->L }
% 63.92/8.71    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(true, true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.71  = { by axiom 2 (cn_19) R->L }
% 63.92/8.71    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))))), true, ifeq(is_a_theorem(implies(implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(implies(implies(T, implies(S, implies(not(a), implies(implies(not(a), a), a)))), implies(not(a), implies(implies(not(a), a), a))), implies(implies(S, implies(not(a), implies(implies(not(a), a), a))), implies(not(a), implies(implies(not(a), a), a)))), implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))))), true), true), true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.72  = { by axiom 4 (condensed_detachment) }
% 63.92/8.72    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.72  = { by axiom 1 (ifeq_axiom) }
% 63.92/8.72    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.72  = { by axiom 1 (ifeq_axiom) R->L }
% 63.92/8.73    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.73  = { by axiom 3 (cn_37) R->L }
% 63.92/8.73    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(not(not(a)), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.73  = { by axiom 4 (condensed_detachment) }
% 63.92/8.73    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.74  = { by axiom 1 (ifeq_axiom) }
% 63.92/8.74    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.74  = { by axiom 1 (ifeq_axiom) R->L }
% 63.92/8.74    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(true, true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.74  = { by axiom 4 (condensed_detachment) R->L }
% 63.92/8.74    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a))), implies(a, implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(a, implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.74  = { by axiom 2 (cn_19) }
% 63.92/8.75    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(a, implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.75  = { by axiom 1 (ifeq_axiom) }
% 63.92/8.75    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(a, implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.75  = { by axiom 1 (ifeq_axiom) R->L }
% 63.92/8.76    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(true, true, is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(a, implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.76  = { by axiom 2 (cn_19) R->L }
% 63.92/8.76    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(X2, not(a)), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(a, implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.76  = { by axiom 1 (ifeq_axiom) R->L }
% 63.92/8.76    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(true, true, ifeq(is_a_theorem(implies(implies(implies(X2, not(a)), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(a, implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.76  = { by axiom 2 (cn_19) R->L }
% 63.92/8.77    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(implies(implies(X2, not(a)), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a))), implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(implies(implies(X2, not(a)), implies(implies(not(a), a), a)), implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(implies(not(a), a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(a, implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.77  = { by axiom 4 (condensed_detachment) }
% 63.92/8.77    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(true, true, is_a_theorem(implies(a, implies(not(a), implies(implies(not(a), a), a)))), true), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.77  = { by axiom 1 (ifeq_axiom) }
% 63.92/8.77    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(ifeq(is_a_theorem(implies(implies(a, implies(not(a), implies(implies(not(a), a), a))), implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(a, implies(not(a), implies(implies(not(a), a), a)))), true, is_a_theorem(implies(implies(not(a), a), implies(not(a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.77  = { by axiom 4 (condensed_detachment) }
% 63.92/8.77    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(ifeq(true, true, is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.77  = { by axiom 1 (ifeq_axiom) }
% 63.92/8.78    ifeq(ifeq(ifeq(is_a_theorem(implies(implies(not(a), implies(implies(not(a), a), a)), implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a))))), true, ifeq(is_a_theorem(implies(not(a), implies(implies(not(a), a), a))), true, is_a_theorem(implies(implies(a, implies(implies(not(a), a), a)), implies(implies(a, a), implies(implies(not(a), a), a)))), true), true), true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.78  = { by axiom 4 (condensed_detachment) }
% 63.92/8.78    ifeq(ifeq(true, true, is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.78  = { by axiom 1 (ifeq_axiom) }
% 63.92/8.78    ifeq(is_a_theorem(implies(implies(a, a), implies(implies(not(a), a), a))), true, ifeq(is_a_theorem(implies(a, a)), true, is_a_theorem(implies(implies(not(a), a), a)), true), true)
% 63.92/8.78  = { by axiom 4 (condensed_detachment) }
% 63.92/8.78    true
% 63.92/8.78  % SZS output end Proof
% 63.92/8.78  
% 63.92/8.78  RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------