%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : HWV007-1 : TPTP v9.0.0. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:08:52 AM UTC 2025
% Result : Unsatisfiable 0.47s 0.71s
% Output : Proof 0.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : HWV007-1 : TPTP v9.0.0. Released v2.1.0.
% 0.10/0.11 % Command : run_E %s %d THM
% 0.12/0.32 % Computer : n011.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 17:19:26 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.47/0.71 % SZS status Unsatisfiable
% 0.47/0.71 % SZS output start Proof
% 0.47/0.71 tff(value_type, type, (
% 0.47/0.71 value: ( $i * $i ) > $o)).
% 0.47/0.71 tff(n1_type, type, (
% 0.47/0.71 n1: $i)).
% 0.47/0.71 tff(out_type, type, (
% 0.47/0.71 out: ( $i * $i ) > $i)).
% 0.47/0.71 tff(h2_type, type, (
% 0.47/0.71 h2: $i > $i)).
% 0.47/0.71 tff(f_type, type, (
% 0.47/0.71 f: $i)).
% 0.47/0.71 tff(s_type, type, (
% 0.47/0.71 s: $i)).
% 0.47/0.71 tff(connection_type, type, (
% 0.47/0.71 connection: ( $i * $i ) > $o)).
% 0.47/0.71 tff(type_type, type, (
% 0.47/0.71 type: ( $i * $i ) > $o)).
% 0.47/0.71 tff(fulladder_type, type, (
% 0.47/0.71 fulladder: $i)).
% 0.47/0.71 tff(and1_type, type, (
% 0.47/0.71 and1: $i > $i)).
% 0.47/0.71 tff(mode_type, type, (
% 0.47/0.71 mode: ( $i * $i ) > $o)).
% 0.47/0.71 tff(ok_type, type, (
% 0.47/0.71 ok: $i)).
% 0.47/0.71 tff(abnormal_type, type, (
% 0.47/0.71 abnormal: $i)).
% 0.47/0.71 tff(or1_type, type, (
% 0.47/0.71 or1: $i > $i)).
% 0.47/0.71 tff(n0_type, type, (
% 0.47/0.71 n0: $i)).
% 0.47/0.71 tff(in_type, type, (
% 0.47/0.71 in: ( $i * $i ) > $i)).
% 0.47/0.71 tff(n2_type, type, (
% 0.47/0.71 n2: $i)).
% 0.47/0.71 tff(h1_type, type, (
% 0.47/0.71 h1: $i > $i)).
% 0.47/0.71 tff(c_type, type, (
% 0.47/0.71 c: $i)).
% 0.47/0.71 tff(and2_type, type, (
% 0.47/0.71 and2: $i > $i)).
% 0.47/0.71 tff(equal_value_type, type, (
% 0.47/0.71 equal_value: ( $i * $i ) > $o)).
% 0.47/0.71 tff(halfadder_type, type, (
% 0.47/0.71 halfadder: $i)).
% 0.47/0.71 tff(and_type, type, (
% 0.47/0.71 and: $i)).
% 0.47/0.71 tff(or_type, type, (
% 0.47/0.71 or: $i)).
% 0.47/0.71 tff(not1_type, type, (
% 0.47/0.71 not1: $i > $i)).
% 0.47/0.71 tff(not_type, type, (
% 0.47/0.71 not: $i)).
% 0.47/0.71 tff(1,plain,
% 0.47/0.71 (type(f, fulladder) <=> type(f, fulladder)),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(2,axiom,(type(f, fulladder)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','f_isa_fulladder')).
% 0.47/0.71 tff(3,plain,
% 0.47/0.71 (type(f, fulladder)),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.47/0.71 tff(4,plain,
% 0.47/0.71 (^[X: $i] : refl(((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X)))) <=> ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X)))))),
% 0.47/0.71 inference(bind,[status(th)],[])).
% 0.47/0.71 tff(5,plain,
% 0.47/0.71 (![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))),
% 0.47/0.71 inference(quant_intro,[status(thm)],[4])).
% 0.47/0.71 tff(6,plain,
% 0.47/0.71 (![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(7,axiom,(![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_connection_outs_outsh2')).
% 0.47/0.71 tff(8,plain,
% 0.47/0.71 (![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[7, 6])).
% 0.47/0.71 tff(9,plain,(
% 0.47/0.71 ![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))),
% 0.47/0.71 inference(skolemize,[status(sab)],[8])).
% 0.47/0.71 tff(10,plain,
% 0.47/0.71 (![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.47/0.71 tff(11,plain,
% 0.47/0.71 (((~![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))) | ((~type(f, fulladder)) | connection(out(s, f), out(s, h2(f))))) <=> ((~![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))) | (~type(f, fulladder)) | connection(out(s, f), out(s, h2(f))))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(12,plain,
% 0.47/0.71 ((~![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))) | ((~type(f, fulladder)) | connection(out(s, f), out(s, h2(f))))),
% 0.47/0.71 inference(quant_inst,[status(thm)],[])).
% 0.47/0.71 tff(13,plain,
% 0.47/0.71 ((~![X: $i] : ((~type(X, fulladder)) | connection(out(s, X), out(s, h2(X))))) | (~type(f, fulladder)) | connection(out(s, f), out(s, h2(f)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.47/0.71 tff(14,plain,
% 0.47/0.71 (connection(out(s, f), out(s, h2(f)))),
% 0.47/0.71 inference(unit_resolution,[status(thm)],[13, 10, 3])).
% 0.47/0.71 tff(15,plain,
% 0.47/0.71 (value(out(s, f), n1) <=> value(out(s, f), n1)),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(16,axiom,(value(out(s, f), n1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','outs_1')).
% 0.47/0.71 tff(17,plain,
% 0.47/0.71 (value(out(s, f), n1)),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.47/0.71 tff(18,plain,
% 0.47/0.71 (^[V: $i, P2: $i, P1: $i] : refl((value(P2, V) | (~value(P1, V)) | (~connection(P1, P2))) <=> (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2))))),
% 0.47/0.71 inference(bind,[status(th)],[])).
% 0.47/0.71 tff(19,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2))) <=> ![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))),
% 0.47/0.71 inference(quant_intro,[status(thm)],[18])).
% 0.47/0.71 tff(20,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2))) <=> ![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(21,plain,
% 0.47/0.71 (^[V: $i, P2: $i, P1: $i] : rewrite((((~connection(P1, P2)) | (~value(P1, V))) | value(P2, V)) <=> (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2))))),
% 0.47/0.71 inference(bind,[status(th)],[])).
% 0.47/0.71 tff(22,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (((~connection(P1, P2)) | (~value(P1, V))) | value(P2, V)) <=> ![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))),
% 0.47/0.71 inference(quant_intro,[status(thm)],[21])).
% 0.47/0.71 tff(23,axiom,(![V: $i, P2: $i, P1: $i] : (((~connection(P1, P2)) | (~value(P1, V))) | value(P2, V))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','value_propagation1')).
% 0.47/0.71 tff(24,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[23, 22])).
% 0.47/0.71 tff(25,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[24, 20])).
% 0.47/0.71 tff(26,plain,(
% 0.47/0.71 ![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))),
% 0.47/0.71 inference(skolemize,[status(sab)],[25])).
% 0.47/0.71 tff(27,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[26, 19])).
% 0.47/0.71 tff(28,plain,
% 0.47/0.71 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f)))) | value(out(s, h2(f)), n1))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f)))) | value(out(s, h2(f)), n1))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(29,plain,
% 0.47/0.71 ((value(out(s, h2(f)), n1) | (~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f))))) <=> ((~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f)))) | value(out(s, h2(f)), n1))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(30,plain,
% 0.47/0.71 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(s, h2(f)), n1) | (~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f)))) | value(out(s, h2(f)), n1)))),
% 0.47/0.71 inference(monotonicity,[status(thm)],[29])).
% 0.47/0.71 tff(31,plain,
% 0.47/0.71 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(s, h2(f)), n1) | (~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f)))) | value(out(s, h2(f)), n1))),
% 0.47/0.71 inference(transitivity,[status(thm)],[30, 28])).
% 0.47/0.71 tff(32,plain,
% 0.47/0.71 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(s, h2(f)), n1) | (~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f)))))),
% 0.47/0.71 inference(quant_inst,[status(thm)],[])).
% 0.47/0.71 tff(33,plain,
% 0.47/0.71 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(s, f), n1)) | (~connection(out(s, f), out(s, h2(f)))) | value(out(s, h2(f)), n1)),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[32, 31])).
% 0.47/0.71 tff(34,plain,
% 0.47/0.71 (value(out(s, h2(f)), n1)),
% 0.47/0.71 inference(unit_resolution,[status(thm)],[33, 27, 17, 14])).
% 0.47/0.71 tff(35,assumption,(value(out(c, h1(f)), n0)), introduced(assumption)).
% 0.47/0.71 tff(36,plain,
% 0.47/0.71 (^[X: $i] : refl(((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X)))) <=> ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X)))))),
% 0.47/0.71 inference(bind,[status(th)],[])).
% 0.47/0.71 tff(37,plain,
% 0.47/0.71 (![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))),
% 0.47/0.71 inference(quant_intro,[status(thm)],[36])).
% 0.47/0.71 tff(38,plain,
% 0.47/0.71 (![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(39,axiom,(![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_connection_inc_in2h1')).
% 0.47/0.71 tff(40,plain,
% 0.47/0.71 (![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[39, 38])).
% 0.47/0.71 tff(41,plain,(
% 0.47/0.71 ![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))),
% 0.47/0.71 inference(skolemize,[status(sab)],[40])).
% 0.47/0.71 tff(42,plain,
% 0.47/0.71 (![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[41, 37])).
% 0.47/0.71 tff(43,plain,
% 0.47/0.71 (((~![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))) | ((~type(f, fulladder)) | connection(in(c, f), in(n2, h1(f))))) <=> ((~![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))) | (~type(f, fulladder)) | connection(in(c, f), in(n2, h1(f))))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(44,plain,
% 0.47/0.71 ((~![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))) | ((~type(f, fulladder)) | connection(in(c, f), in(n2, h1(f))))),
% 0.47/0.71 inference(quant_inst,[status(thm)],[])).
% 0.47/0.71 tff(45,plain,
% 0.47/0.71 ((~![X: $i] : ((~type(X, fulladder)) | connection(in(c, X), in(n2, h1(X))))) | (~type(f, fulladder)) | connection(in(c, f), in(n2, h1(f)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[44, 43])).
% 0.47/0.71 tff(46,plain,
% 0.47/0.71 (connection(in(c, f), in(n2, h1(f)))),
% 0.47/0.71 inference(unit_resolution,[status(thm)],[45, 42, 3])).
% 0.47/0.71 tff(47,plain,
% 0.47/0.71 (value(in(c, f), n1) <=> value(in(c, f), n1)),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(48,axiom,(value(in(c, f), n1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','inc_1')).
% 0.47/0.71 tff(49,plain,
% 0.47/0.71 (value(in(c, f), n1)),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.47/0.71 tff(50,plain,
% 0.47/0.71 ((~equal_value(n0, n1)) <=> (~equal_value(n0, n1))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(51,axiom,(~equal_value(n0, n1)), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','equal_value1')).
% 0.47/0.71 tff(52,plain,
% 0.47/0.71 (~equal_value(n0, n1)),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[51, 50])).
% 0.47/0.71 tff(53,plain,
% 0.47/0.71 (^[P: $i, V1: $i, V2: $i] : refl((equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1))) <=> (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1))))),
% 0.47/0.71 inference(bind,[status(th)],[])).
% 0.47/0.71 tff(54,plain,
% 0.47/0.71 (![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1))) <=> ![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))),
% 0.47/0.71 inference(quant_intro,[status(thm)],[53])).
% 0.47/0.71 tff(55,plain,
% 0.47/0.71 (![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1))) <=> ![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(56,plain,
% 0.47/0.71 (^[P: $i, V1: $i, V2: $i] : trans(monotonicity(rewrite(((~value(P, V1)) | (~value(P, V2))) <=> ((~value(P, V2)) | (~value(P, V1)))), ((((~value(P, V1)) | (~value(P, V2))) | equal_value(V1, V2)) <=> (((~value(P, V2)) | (~value(P, V1))) | equal_value(V1, V2)))), rewrite((((~value(P, V2)) | (~value(P, V1))) | equal_value(V1, V2)) <=> (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))), ((((~value(P, V1)) | (~value(P, V2))) | equal_value(V1, V2)) <=> (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))))),
% 0.47/0.71 inference(bind,[status(th)],[])).
% 0.47/0.71 tff(57,plain,
% 0.47/0.71 (![P: $i, V1: $i, V2: $i] : (((~value(P, V1)) | (~value(P, V2))) | equal_value(V1, V2)) <=> ![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))),
% 0.47/0.71 inference(quant_intro,[status(thm)],[56])).
% 0.47/0.71 tff(58,axiom,(![P: $i, V1: $i, V2: $i] : (((~value(P, V1)) | (~value(P, V2))) | equal_value(V1, V2))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','unique_value')).
% 0.47/0.71 tff(59,plain,
% 0.47/0.71 (![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.47/0.71 tff(60,plain,
% 0.47/0.71 (![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[59, 55])).
% 0.47/0.71 tff(61,plain,(
% 0.47/0.71 ![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))),
% 0.47/0.71 inference(skolemize,[status(sab)],[60])).
% 0.47/0.71 tff(62,plain,
% 0.47/0.71 (![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[61, 54])).
% 0.47/0.71 tff(63,plain,
% 0.47/0.71 (((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n0, n1) | (~value(in(c, f), n1)) | (~value(in(c, f), n0)))) <=> ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | equal_value(n0, n1) | (~value(in(c, f), n1)) | (~value(in(c, f), n0)))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(64,plain,
% 0.47/0.71 ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n0, n1) | (~value(in(c, f), n1)) | (~value(in(c, f), n0)))),
% 0.47/0.71 inference(quant_inst,[status(thm)],[])).
% 0.47/0.71 tff(65,plain,
% 0.47/0.71 ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | equal_value(n0, n1) | (~value(in(c, f), n1)) | (~value(in(c, f), n0))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.47/0.71 tff(66,plain,
% 0.47/0.71 (~value(in(c, f), n0)),
% 0.47/0.71 inference(unit_resolution,[status(thm)],[65, 62, 52, 49])).
% 0.47/0.71 tff(67,plain,
% 0.47/0.71 (^[V: $i, P2: $i, P1: $i] : refl((value(P1, V) | (~connection(P1, P2)) | (~value(P2, V))) <=> (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V))))),
% 0.47/0.71 inference(bind,[status(th)],[])).
% 0.47/0.71 tff(68,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V))) <=> ![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))),
% 0.47/0.71 inference(quant_intro,[status(thm)],[67])).
% 0.47/0.71 tff(69,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V))) <=> ![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))),
% 0.47/0.71 inference(rewrite,[status(thm)],[])).
% 0.47/0.71 tff(70,plain,
% 0.47/0.71 (^[V: $i, P2: $i, P1: $i] : rewrite((((~connection(P1, P2)) | (~value(P2, V))) | value(P1, V)) <=> (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V))))),
% 0.47/0.71 inference(bind,[status(th)],[])).
% 0.47/0.71 tff(71,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (((~connection(P1, P2)) | (~value(P2, V))) | value(P1, V)) <=> ![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))),
% 0.47/0.71 inference(quant_intro,[status(thm)],[70])).
% 0.47/0.71 tff(72,axiom,(![V: $i, P2: $i, P1: $i] : (((~connection(P1, P2)) | (~value(P2, V))) | value(P1, V))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','value_propagation2')).
% 0.47/0.71 tff(73,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[72, 71])).
% 0.47/0.71 tff(74,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[73, 69])).
% 0.47/0.71 tff(75,plain,(
% 0.47/0.71 ![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))),
% 0.47/0.71 inference(skolemize,[status(sab)],[74])).
% 0.47/0.71 tff(76,plain,
% 0.47/0.71 (![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))),
% 0.47/0.71 inference(modus_ponens,[status(thm)],[75, 68])).
% 0.47/0.71 tff(77,plain,
% 0.47/0.71 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(c, f), n0) | (~connection(in(c, f), in(n2, h1(f)))) | (~value(in(n2, h1(f)), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(c, f), n0) | (~connection(in(c, f), in(n2, h1(f)))) | (~value(in(n2, h1(f)), n0)))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(78,plain,
% 0.47/0.72 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(c, f), n0) | (~connection(in(c, f), in(n2, h1(f)))) | (~value(in(n2, h1(f)), n0)))),
% 0.47/0.72 inference(quant_inst,[status(thm)],[])).
% 0.47/0.72 tff(79,plain,
% 0.47/0.72 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(c, f), n0) | (~connection(in(c, f), in(n2, h1(f)))) | (~value(in(n2, h1(f)), n0))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[78, 77])).
% 0.47/0.72 tff(80,plain,
% 0.47/0.72 (~value(in(n2, h1(f)), n0)),
% 0.47/0.72 inference(unit_resolution,[status(thm)],[79, 76, 66, 46])).
% 0.47/0.72 tff(81,plain,
% 0.47/0.72 (^[X: $i] : refl(((~type(X, fulladder)) | type(h1(X), halfadder)) <=> ((~type(X, fulladder)) | type(h1(X), halfadder)))),
% 0.47/0.72 inference(bind,[status(th)],[])).
% 0.47/0.72 tff(82,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder)) <=> ![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))),
% 0.47/0.72 inference(quant_intro,[status(thm)],[81])).
% 0.47/0.72 tff(83,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder)) <=> ![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(84,axiom,(![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_halfadder1')).
% 0.47/0.72 tff(85,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[84, 83])).
% 0.47/0.72 tff(86,plain,(
% 0.47/0.72 ![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))),
% 0.47/0.72 inference(skolemize,[status(sab)],[85])).
% 0.47/0.72 tff(87,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[86, 82])).
% 0.47/0.72 tff(88,plain,
% 0.47/0.72 (((~![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))) | ((~type(f, fulladder)) | type(h1(f), halfadder))) <=> ((~![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))) | (~type(f, fulladder)) | type(h1(f), halfadder))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(89,plain,
% 0.47/0.72 ((~![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))) | ((~type(f, fulladder)) | type(h1(f), halfadder))),
% 0.47/0.72 inference(quant_inst,[status(thm)],[])).
% 0.47/0.72 tff(90,plain,
% 0.47/0.72 ((~![X: $i] : ((~type(X, fulladder)) | type(h1(X), halfadder))) | (~type(f, fulladder)) | type(h1(f), halfadder)),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[89, 88])).
% 0.47/0.72 tff(91,plain,
% 0.47/0.72 (type(h1(f), halfadder)),
% 0.47/0.72 inference(unit_resolution,[status(thm)],[90, 87, 3])).
% 0.47/0.72 tff(92,plain,
% 0.47/0.72 (^[X: $i] : refl(((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X)))) <=> ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X)))))),
% 0.47/0.72 inference(bind,[status(th)],[])).
% 0.47/0.72 tff(93,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))),
% 0.47/0.72 inference(quant_intro,[status(thm)],[92])).
% 0.47/0.72 tff(94,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(95,axiom,(![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_connection_in2_in2and2')).
% 0.47/0.72 tff(96,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[95, 94])).
% 0.47/0.72 tff(97,plain,(
% 0.47/0.72 ![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))),
% 0.47/0.72 inference(skolemize,[status(sab)],[96])).
% 0.47/0.72 tff(98,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[97, 93])).
% 0.47/0.72 tff(99,plain,
% 0.47/0.72 (((~![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))) | ((~type(h1(f), halfadder)) | connection(in(n2, h1(f)), in(n2, and2(h1(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))) | (~type(h1(f), halfadder)) | connection(in(n2, h1(f)), in(n2, and2(h1(f)))))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(100,plain,
% 0.47/0.72 ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))) | ((~type(h1(f), halfadder)) | connection(in(n2, h1(f)), in(n2, and2(h1(f)))))),
% 0.47/0.72 inference(quant_inst,[status(thm)],[])).
% 0.47/0.72 tff(101,plain,
% 0.47/0.72 ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, and2(X))))) | (~type(h1(f), halfadder)) | connection(in(n2, h1(f)), in(n2, and2(h1(f))))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[100, 99])).
% 0.47/0.72 tff(102,plain,
% 0.47/0.72 (connection(in(n2, h1(f)), in(n2, and2(h1(f))))),
% 0.47/0.72 inference(unit_resolution,[status(thm)],[101, 98, 91])).
% 0.47/0.72 tff(103,plain,
% 0.47/0.72 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h1(f)), n0) | (~value(in(n2, and2(h1(f))), n0)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n2, h1(f)), n0) | (~value(in(n2, and2(h1(f))), n0)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(104,plain,
% 0.47/0.72 ((value(in(n2, h1(f)), n0) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))) | (~value(in(n2, and2(h1(f))), n0))) <=> (value(in(n2, h1(f)), n0) | (~value(in(n2, and2(h1(f))), n0)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(105,plain,
% 0.47/0.72 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h1(f)), n0) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))) | (~value(in(n2, and2(h1(f))), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h1(f)), n0) | (~value(in(n2, and2(h1(f))), n0)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f)))))))),
% 0.47/0.72 inference(monotonicity,[status(thm)],[104])).
% 0.47/0.72 tff(106,plain,
% 0.47/0.72 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h1(f)), n0) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))) | (~value(in(n2, and2(h1(f))), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n2, h1(f)), n0) | (~value(in(n2, and2(h1(f))), n0)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))))),
% 0.47/0.72 inference(transitivity,[status(thm)],[105, 103])).
% 0.47/0.72 tff(107,plain,
% 0.47/0.72 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h1(f)), n0) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))) | (~value(in(n2, and2(h1(f))), n0)))),
% 0.47/0.72 inference(quant_inst,[status(thm)],[])).
% 0.47/0.72 tff(108,plain,
% 0.47/0.72 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n2, h1(f)), n0) | (~value(in(n2, and2(h1(f))), n0)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f)))))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[107, 106])).
% 0.47/0.72 tff(109,plain,
% 0.47/0.72 (~value(in(n2, and2(h1(f))), n0)),
% 0.47/0.72 inference(unit_resolution,[status(thm)],[108, 76, 102, 80])).
% 0.47/0.72 tff(110,plain,
% 0.47/0.72 (^[X: $i] : refl(((~type(X, halfadder)) | type(and2(X), and)) <=> ((~type(X, halfadder)) | type(and2(X), and)))),
% 0.47/0.72 inference(bind,[status(th)],[])).
% 0.47/0.72 tff(111,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, halfadder)) | type(and2(X), and)) <=> ![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))),
% 0.47/0.72 inference(quant_intro,[status(thm)],[110])).
% 0.47/0.72 tff(112,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, halfadder)) | type(and2(X), and)) <=> ![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(113,axiom,(![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_and2')).
% 0.47/0.72 tff(114,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[113, 112])).
% 0.47/0.72 tff(115,plain,(
% 0.47/0.72 ![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))),
% 0.47/0.72 inference(skolemize,[status(sab)],[114])).
% 0.47/0.72 tff(116,plain,
% 0.47/0.72 (![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[115, 111])).
% 0.47/0.72 tff(117,plain,
% 0.47/0.72 (((~![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))) | ((~type(h1(f), halfadder)) | type(and2(h1(f)), and))) <=> ((~![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))) | (~type(h1(f), halfadder)) | type(and2(h1(f)), and))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(118,plain,
% 0.47/0.72 ((~![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))) | ((~type(h1(f), halfadder)) | type(and2(h1(f)), and))),
% 0.47/0.72 inference(quant_inst,[status(thm)],[])).
% 0.47/0.72 tff(119,plain,
% 0.47/0.72 ((~![X: $i] : ((~type(X, halfadder)) | type(and2(X), and))) | (~type(h1(f), halfadder)) | type(and2(h1(f)), and)),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.47/0.72 tff(120,plain,
% 0.47/0.72 (type(and2(h1(f)), and)),
% 0.47/0.72 inference(unit_resolution,[status(thm)],[119, 116, 91])).
% 0.47/0.72 tff(121,plain,
% 0.47/0.72 ((~mode(and2(h1(f)), abnormal)) <=> (~mode(and2(h1(f)), abnormal))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(122,axiom,(~mode(and2(h1(f)), abnormal)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','diagnosis_and2h1')).
% 0.47/0.72 tff(123,plain,
% 0.47/0.72 (~mode(and2(h1(f)), abnormal)),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[122, 121])).
% 0.47/0.72 tff(124,plain,
% 0.47/0.72 (^[Any: $i, K: $i] : refl((mode(K, abnormal) | mode(K, ok) | (~type(K, Any))) <=> (mode(K, abnormal) | mode(K, ok) | (~type(K, Any))))),
% 0.47/0.72 inference(bind,[status(th)],[])).
% 0.47/0.72 tff(125,plain,
% 0.47/0.72 (![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any))) <=> ![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))),
% 0.47/0.72 inference(quant_intro,[status(thm)],[124])).
% 0.47/0.72 tff(126,plain,
% 0.47/0.72 (![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any))) <=> ![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(127,plain,
% 0.47/0.72 (^[Any: $i, K: $i] : rewrite((((~type(K, Any)) | mode(K, ok)) | mode(K, abnormal)) <=> (mode(K, abnormal) | mode(K, ok) | (~type(K, Any))))),
% 0.47/0.72 inference(bind,[status(th)],[])).
% 0.47/0.72 tff(128,plain,
% 0.47/0.72 (![Any: $i, K: $i] : (((~type(K, Any)) | mode(K, ok)) | mode(K, abnormal)) <=> ![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))),
% 0.47/0.72 inference(quant_intro,[status(thm)],[127])).
% 0.47/0.72 tff(129,axiom,(![Any: $i, K: $i] : (((~type(K, Any)) | mode(K, ok)) | mode(K, abnormal))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','ok_or_abnormal')).
% 0.47/0.72 tff(130,plain,
% 0.47/0.72 (![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[129, 128])).
% 0.47/0.72 tff(131,plain,
% 0.47/0.72 (![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[130, 126])).
% 0.47/0.72 tff(132,plain,(
% 0.47/0.72 ![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))),
% 0.47/0.72 inference(skolemize,[status(sab)],[131])).
% 0.47/0.72 tff(133,plain,
% 0.47/0.72 (![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[132, 125])).
% 0.47/0.72 tff(134,plain,
% 0.47/0.72 (((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(and2(h1(f)), abnormal) | mode(and2(h1(f)), ok) | (~type(and2(h1(f)), and)))) <=> ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(and2(h1(f)), abnormal) | mode(and2(h1(f)), ok) | (~type(and2(h1(f)), and)))),
% 0.47/0.72 inference(rewrite,[status(thm)],[])).
% 0.47/0.72 tff(135,plain,
% 0.47/0.72 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(and2(h1(f)), abnormal) | mode(and2(h1(f)), ok) | (~type(and2(h1(f)), and)))),
% 0.47/0.72 inference(quant_inst,[status(thm)],[])).
% 0.47/0.72 tff(136,plain,
% 0.47/0.72 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(and2(h1(f)), abnormal) | mode(and2(h1(f)), ok) | (~type(and2(h1(f)), and))),
% 0.47/0.72 inference(modus_ponens,[status(thm)],[135, 134])).
% 0.47/0.72 tff(137,plain,
% 0.47/0.72 (mode(and2(h1(f)), ok)),
% 0.57/0.72 inference(unit_resolution,[status(thm)],[136, 133, 123, 120])).
% 0.57/0.72 tff(138,plain,
% 0.57/0.72 (^[X: $i] : refl(((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X)))) <=> ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X)))))),
% 0.57/0.72 inference(bind,[status(th)],[])).
% 0.57/0.72 tff(139,plain,
% 0.57/0.72 (![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))),
% 0.57/0.72 inference(quant_intro,[status(thm)],[138])).
% 0.57/0.72 tff(140,plain,
% 0.57/0.72 (![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))),
% 0.57/0.72 inference(rewrite,[status(thm)],[])).
% 0.57/0.72 tff(141,axiom,(![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_connection_in2_in1h1')).
% 0.57/0.72 tff(142,plain,
% 0.57/0.72 (![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))),
% 0.57/0.72 inference(modus_ponens,[status(thm)],[141, 140])).
% 0.57/0.72 tff(143,plain,(
% 0.57/0.72 ![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))),
% 0.57/0.72 inference(skolemize,[status(sab)],[142])).
% 0.57/0.72 tff(144,plain,
% 0.57/0.72 (![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))),
% 0.57/0.72 inference(modus_ponens,[status(thm)],[143, 139])).
% 0.57/0.72 tff(145,plain,
% 0.57/0.72 (((~![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))) | ((~type(f, fulladder)) | connection(in(n2, f), in(n1, h1(f))))) <=> ((~![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))) | (~type(f, fulladder)) | connection(in(n2, f), in(n1, h1(f))))),
% 0.57/0.72 inference(rewrite,[status(thm)],[])).
% 0.57/0.72 tff(146,plain,
% 0.57/0.72 ((~![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))) | ((~type(f, fulladder)) | connection(in(n2, f), in(n1, h1(f))))),
% 0.57/0.72 inference(quant_inst,[status(thm)],[])).
% 0.57/0.72 tff(147,plain,
% 0.57/0.72 ((~![X: $i] : ((~type(X, fulladder)) | connection(in(n2, X), in(n1, h1(X))))) | (~type(f, fulladder)) | connection(in(n2, f), in(n1, h1(f)))),
% 0.57/0.72 inference(modus_ponens,[status(thm)],[146, 145])).
% 0.57/0.72 tff(148,plain,
% 0.57/0.72 (connection(in(n2, f), in(n1, h1(f)))),
% 0.57/0.72 inference(unit_resolution,[status(thm)],[147, 144, 3])).
% 0.57/0.72 tff(149,plain,
% 0.57/0.72 (value(in(n2, f), n1) <=> value(in(n2, f), n1)),
% 0.57/0.72 inference(rewrite,[status(thm)],[])).
% 0.57/0.72 tff(150,axiom,(value(in(n2, f), n1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','in2_0')).
% 0.57/0.72 tff(151,plain,
% 0.57/0.72 (value(in(n2, f), n1)),
% 0.57/0.72 inference(modus_ponens,[status(thm)],[150, 149])).
% 0.57/0.72 tff(152,plain,
% 0.57/0.72 (((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n0, n1) | (~value(in(n2, f), n1)) | (~value(in(n2, f), n0)))) <=> ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | equal_value(n0, n1) | (~value(in(n2, f), n1)) | (~value(in(n2, f), n0)))),
% 0.57/0.72 inference(rewrite,[status(thm)],[])).
% 0.57/0.72 tff(153,plain,
% 0.57/0.72 ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n0, n1) | (~value(in(n2, f), n1)) | (~value(in(n2, f), n0)))),
% 0.57/0.72 inference(quant_inst,[status(thm)],[])).
% 0.57/0.72 tff(154,plain,
% 0.57/0.72 ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | equal_value(n0, n1) | (~value(in(n2, f), n1)) | (~value(in(n2, f), n0))),
% 0.57/0.72 inference(modus_ponens,[status(thm)],[153, 152])).
% 0.57/0.72 tff(155,plain,
% 0.57/0.72 (~value(in(n2, f), n0)),
% 0.57/0.72 inference(unit_resolution,[status(thm)],[154, 62, 52, 151])).
% 0.57/0.72 tff(156,plain,
% 0.57/0.72 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, f), n0) | (~connection(in(n2, f), in(n1, h1(f)))) | (~value(in(n1, h1(f)), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n2, f), n0) | (~connection(in(n2, f), in(n1, h1(f)))) | (~value(in(n1, h1(f)), n0)))),
% 0.57/0.72 inference(rewrite,[status(thm)],[])).
% 0.57/0.72 tff(157,plain,
% 0.57/0.72 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, f), n0) | (~connection(in(n2, f), in(n1, h1(f)))) | (~value(in(n1, h1(f)), n0)))),
% 0.57/0.72 inference(quant_inst,[status(thm)],[])).
% 0.57/0.72 tff(158,plain,
% 0.57/0.72 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n2, f), n0) | (~connection(in(n2, f), in(n1, h1(f)))) | (~value(in(n1, h1(f)), n0))),
% 0.57/0.72 inference(modus_ponens,[status(thm)],[157, 156])).
% 0.57/0.72 tff(159,plain,
% 0.57/0.72 (~value(in(n1, h1(f)), n0)),
% 0.57/0.72 inference(unit_resolution,[status(thm)],[158, 76, 155, 148])).
% 0.57/0.72 tff(160,plain,
% 0.57/0.72 (^[X: $i] : refl(((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X)))) <=> ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X)))))),
% 0.57/0.72 inference(bind,[status(th)],[])).
% 0.57/0.72 tff(161,plain,
% 0.57/0.72 (![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))),
% 0.57/0.72 inference(quant_intro,[status(thm)],[160])).
% 0.57/0.72 tff(162,plain,
% 0.57/0.72 (![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))),
% 0.57/0.72 inference(rewrite,[status(thm)],[])).
% 0.57/0.72 tff(163,axiom,(![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_connection_in1_in1and2')).
% 0.57/0.72 tff(164,plain,
% 0.57/0.72 (![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))),
% 0.57/0.72 inference(modus_ponens,[status(thm)],[163, 162])).
% 0.57/0.72 tff(165,plain,(
% 0.57/0.72 ![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))),
% 0.57/0.72 inference(skolemize,[status(sab)],[164])).
% 0.57/0.72 tff(166,plain,
% 0.57/0.72 (![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))),
% 0.57/0.72 inference(modus_ponens,[status(thm)],[165, 161])).
% 0.57/0.72 tff(167,plain,
% 0.57/0.72 (((~![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))) | ((~type(h1(f), halfadder)) | connection(in(n1, h1(f)), in(n1, and2(h1(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))) | (~type(h1(f), halfadder)) | connection(in(n1, h1(f)), in(n1, and2(h1(f)))))),
% 0.57/0.72 inference(rewrite,[status(thm)],[])).
% 0.57/0.72 tff(168,plain,
% 0.57/0.72 ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))) | ((~type(h1(f), halfadder)) | connection(in(n1, h1(f)), in(n1, and2(h1(f)))))),
% 0.57/0.72 inference(quant_inst,[status(thm)],[])).
% 0.57/0.72 tff(169,plain,
% 0.57/0.72 ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, and2(X))))) | (~type(h1(f), halfadder)) | connection(in(n1, h1(f)), in(n1, and2(h1(f))))),
% 0.57/0.72 inference(modus_ponens,[status(thm)],[168, 167])).
% 0.57/0.72 tff(170,plain,
% 0.57/0.72 (connection(in(n1, h1(f)), in(n1, and2(h1(f))))),
% 0.57/0.72 inference(unit_resolution,[status(thm)],[169, 166, 91])).
% 0.57/0.72 tff(171,plain,
% 0.57/0.72 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n1, h1(f)), n0) | (~value(in(n1, and2(h1(f))), n0)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n1, h1(f)), n0) | (~value(in(n1, and2(h1(f))), n0)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))))),
% 0.57/0.72 inference(rewrite,[status(thm)],[])).
% 0.57/0.72 tff(172,plain,
% 0.57/0.72 ((value(in(n1, h1(f)), n0) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))) | (~value(in(n1, and2(h1(f))), n0))) <=> (value(in(n1, h1(f)), n0) | (~value(in(n1, and2(h1(f))), n0)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))))),
% 0.57/0.72 inference(rewrite,[status(thm)],[])).
% 0.57/0.72 tff(173,plain,
% 0.57/0.72 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n1, h1(f)), n0) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))) | (~value(in(n1, and2(h1(f))), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n1, h1(f)), n0) | (~value(in(n1, and2(h1(f))), n0)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f)))))))),
% 0.57/0.72 inference(monotonicity,[status(thm)],[172])).
% 0.57/0.72 tff(174,plain,
% 0.57/0.72 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n1, h1(f)), n0) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))) | (~value(in(n1, and2(h1(f))), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n1, h1(f)), n0) | (~value(in(n1, and2(h1(f))), n0)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))))),
% 0.57/0.73 inference(transitivity,[status(thm)],[173, 171])).
% 0.57/0.73 tff(175,plain,
% 0.57/0.73 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n1, h1(f)), n0) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))) | (~value(in(n1, and2(h1(f))), n0)))),
% 0.57/0.73 inference(quant_inst,[status(thm)],[])).
% 0.57/0.73 tff(176,plain,
% 0.57/0.73 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n1, h1(f)), n0) | (~value(in(n1, and2(h1(f))), n0)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f)))))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[175, 174])).
% 0.57/0.73 tff(177,plain,
% 0.57/0.73 (~value(in(n1, and2(h1(f))), n0)),
% 0.57/0.73 inference(unit_resolution,[status(thm)],[176, 76, 170, 159])).
% 0.57/0.73 tff(178,plain,
% 0.57/0.73 (^[K: $i] : refl(((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0))) <=> ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0))))),
% 0.57/0.73 inference(bind,[status(th)],[])).
% 0.57/0.73 tff(179,plain,
% 0.57/0.73 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0))) <=> ![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))),
% 0.57/0.73 inference(quant_intro,[status(thm)],[178])).
% 0.57/0.73 tff(180,plain,
% 0.57/0.73 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0))) <=> ![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(181,plain,
% 0.57/0.73 (^[K: $i] : trans(monotonicity(trans(monotonicity(rewrite((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n0))) <=> ((~mode(K, ok)) | (~type(K, and)) | (~value(out(n1, K), n0)))), (((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n0))) | value(in(n1, K), n0)) <=> (((~mode(K, ok)) | (~type(K, and)) | (~value(out(n1, K), n0))) | value(in(n1, K), n0)))), rewrite((((~mode(K, ok)) | (~type(K, and)) | (~value(out(n1, K), n0))) | value(in(n1, K), n0)) <=> ((~mode(K, ok)) | (~type(K, and)) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))), (((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n0))) | value(in(n1, K), n0)) <=> ((~mode(K, ok)) | (~type(K, and)) | value(in(n1, K), n0) | (~value(out(n1, K), n0))))), ((((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n0))) | value(in(n1, K), n0)) | value(in(n2, K), n0)) <=> (((~mode(K, ok)) | (~type(K, and)) | value(in(n1, K), n0) | (~value(out(n1, K), n0))) | value(in(n2, K), n0)))), rewrite((((~mode(K, ok)) | (~type(K, and)) | value(in(n1, K), n0) | (~value(out(n1, K), n0))) | value(in(n2, K), n0)) <=> ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))), ((((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n0))) | value(in(n1, K), n0)) | value(in(n2, K), n0)) <=> ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))))),
% 0.57/0.73 inference(bind,[status(th)],[])).
% 0.57/0.73 tff(182,plain,
% 0.57/0.73 (![K: $i] : (((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n0))) | value(in(n1, K), n0)) | value(in(n2, K), n0)) <=> ![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))),
% 0.57/0.73 inference(quant_intro,[status(thm)],[181])).
% 0.57/0.73 tff(183,axiom,(![K: $i] : (((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n0))) | value(in(n1, K), n0)) | value(in(n2, K), n0))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','and_0_00')).
% 0.57/0.73 tff(184,plain,
% 0.57/0.73 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[183, 182])).
% 0.57/0.73 tff(185,plain,
% 0.57/0.73 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[184, 180])).
% 0.57/0.73 tff(186,plain,(
% 0.57/0.73 ![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))),
% 0.57/0.73 inference(skolemize,[status(sab)],[185])).
% 0.57/0.73 tff(187,plain,
% 0.57/0.73 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[186, 179])).
% 0.57/0.73 tff(188,plain,
% 0.57/0.73 (((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))) | ((~mode(and2(h1(f)), ok)) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)) | value(in(n2, and2(h1(f))), n0) | (~type(and2(h1(f)), and)))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))) | (~mode(and2(h1(f)), ok)) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)) | value(in(n2, and2(h1(f))), n0) | (~type(and2(h1(f)), and)))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(189,plain,
% 0.57/0.73 (((~mode(and2(h1(f)), ok)) | (~type(and2(h1(f)), and)) | value(in(n2, and2(h1(f))), n0) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0))) <=> ((~mode(and2(h1(f)), ok)) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)) | value(in(n2, and2(h1(f))), n0) | (~type(and2(h1(f)), and)))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(190,plain,
% 0.57/0.73 (((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))) | ((~mode(and2(h1(f)), ok)) | (~type(and2(h1(f)), and)) | value(in(n2, and2(h1(f))), n0) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))) | ((~mode(and2(h1(f)), ok)) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)) | value(in(n2, and2(h1(f))), n0) | (~type(and2(h1(f)), and))))),
% 0.57/0.73 inference(monotonicity,[status(thm)],[189])).
% 0.57/0.73 tff(191,plain,
% 0.57/0.73 (((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))) | ((~mode(and2(h1(f)), ok)) | (~type(and2(h1(f)), and)) | value(in(n2, and2(h1(f))), n0) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))) | (~mode(and2(h1(f)), ok)) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)) | value(in(n2, and2(h1(f))), n0) | (~type(and2(h1(f)), and)))),
% 0.57/0.73 inference(transitivity,[status(thm)],[190, 188])).
% 0.57/0.73 tff(192,plain,
% 0.57/0.73 ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))) | ((~mode(and2(h1(f)), ok)) | (~type(and2(h1(f)), and)) | value(in(n2, and2(h1(f))), n0) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)))),
% 0.57/0.73 inference(quant_inst,[status(thm)],[])).
% 0.57/0.73 tff(193,plain,
% 0.57/0.73 ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(in(n2, K), n0) | value(in(n1, K), n0) | (~value(out(n1, K), n0)))) | (~mode(and2(h1(f)), ok)) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)) | value(in(n2, and2(h1(f))), n0) | (~type(and2(h1(f)), and))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[192, 191])).
% 0.57/0.73 tff(194,plain,
% 0.57/0.73 ((~mode(and2(h1(f)), ok)) | value(in(n1, and2(h1(f))), n0) | (~value(out(n1, and2(h1(f))), n0)) | value(in(n2, and2(h1(f))), n0)),
% 0.57/0.73 inference(unit_resolution,[status(thm)],[193, 187, 120])).
% 0.57/0.73 tff(195,plain,
% 0.57/0.73 (~value(out(n1, and2(h1(f))), n0)),
% 0.57/0.73 inference(unit_resolution,[status(thm)],[194, 177, 137, 109])).
% 0.57/0.73 tff(196,plain,
% 0.57/0.73 (^[X: $i] : refl(((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X)))) <=> ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X)))))),
% 0.57/0.73 inference(bind,[status(th)],[])).
% 0.57/0.73 tff(197,plain,
% 0.57/0.73 (![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))),
% 0.57/0.73 inference(quant_intro,[status(thm)],[196])).
% 0.57/0.73 tff(198,plain,
% 0.57/0.73 (![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(199,axiom,(![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_connection_outc_out1and2')).
% 0.57/0.73 tff(200,plain,
% 0.57/0.73 (![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[199, 198])).
% 0.57/0.73 tff(201,plain,(
% 0.57/0.73 ![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))),
% 0.57/0.73 inference(skolemize,[status(sab)],[200])).
% 0.57/0.73 tff(202,plain,
% 0.57/0.73 (![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[201, 197])).
% 0.57/0.73 tff(203,plain,
% 0.57/0.73 (((~![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))) | ((~type(h1(f), halfadder)) | connection(out(c, h1(f)), out(n1, and2(h1(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))) | (~type(h1(f), halfadder)) | connection(out(c, h1(f)), out(n1, and2(h1(f)))))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(204,plain,
% 0.57/0.73 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))) | ((~type(h1(f), halfadder)) | connection(out(c, h1(f)), out(n1, and2(h1(f)))))),
% 0.57/0.73 inference(quant_inst,[status(thm)],[])).
% 0.57/0.73 tff(205,plain,
% 0.57/0.73 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(c, X), out(n1, and2(X))))) | (~type(h1(f), halfadder)) | connection(out(c, h1(f)), out(n1, and2(h1(f))))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[204, 203])).
% 0.57/0.73 tff(206,plain,
% 0.57/0.73 (connection(out(c, h1(f)), out(n1, and2(h1(f))))),
% 0.57/0.73 inference(unit_resolution,[status(thm)],[205, 202, 91])).
% 0.57/0.73 tff(207,plain,
% 0.57/0.73 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(n1, and2(h1(f))), n0) | (~value(out(c, h1(f)), n0)) | (~connection(out(c, h1(f)), out(n1, and2(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | value(out(n1, and2(h1(f))), n0) | (~value(out(c, h1(f)), n0)) | (~connection(out(c, h1(f)), out(n1, and2(h1(f))))))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(208,plain,
% 0.57/0.73 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(n1, and2(h1(f))), n0) | (~value(out(c, h1(f)), n0)) | (~connection(out(c, h1(f)), out(n1, and2(h1(f))))))),
% 0.57/0.73 inference(quant_inst,[status(thm)],[])).
% 0.57/0.73 tff(209,plain,
% 0.57/0.73 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | value(out(n1, and2(h1(f))), n0) | (~value(out(c, h1(f)), n0)) | (~connection(out(c, h1(f)), out(n1, and2(h1(f)))))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[208, 207])).
% 0.57/0.73 tff(210,plain,
% 0.57/0.73 ($false),
% 0.57/0.73 inference(unit_resolution,[status(thm)],[209, 27, 206, 195, 35])).
% 0.57/0.73 tff(211,plain,(~value(out(c, h1(f)), n0)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.73 tff(212,plain,
% 0.57/0.73 (^[X: $i] : refl(((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X)))) <=> ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X)))))),
% 0.57/0.73 inference(bind,[status(th)],[])).
% 0.57/0.73 tff(213,plain,
% 0.57/0.73 (![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))),
% 0.57/0.73 inference(quant_intro,[status(thm)],[212])).
% 0.57/0.73 tff(214,plain,
% 0.57/0.73 (![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(215,axiom,(![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_connection_outch1_in2or1')).
% 0.57/0.73 tff(216,plain,
% 0.57/0.73 (![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[215, 214])).
% 0.57/0.73 tff(217,plain,(
% 0.57/0.73 ![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))),
% 0.57/0.73 inference(skolemize,[status(sab)],[216])).
% 0.57/0.73 tff(218,plain,
% 0.57/0.73 (![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[217, 213])).
% 0.57/0.73 tff(219,plain,
% 0.57/0.73 (((~![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))) | ((~type(f, fulladder)) | connection(out(c, h1(f)), in(n2, or1(f))))) <=> ((~![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))) | (~type(f, fulladder)) | connection(out(c, h1(f)), in(n2, or1(f))))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(220,plain,
% 0.57/0.73 ((~![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))) | ((~type(f, fulladder)) | connection(out(c, h1(f)), in(n2, or1(f))))),
% 0.57/0.73 inference(quant_inst,[status(thm)],[])).
% 0.57/0.73 tff(221,plain,
% 0.57/0.73 ((~![X: $i] : ((~type(X, fulladder)) | connection(out(c, h1(X)), in(n2, or1(X))))) | (~type(f, fulladder)) | connection(out(c, h1(f)), in(n2, or1(f)))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[220, 219])).
% 0.57/0.73 tff(222,plain,
% 0.57/0.73 (connection(out(c, h1(f)), in(n2, or1(f)))),
% 0.57/0.73 inference(unit_resolution,[status(thm)],[221, 218, 3])).
% 0.57/0.73 tff(223,plain,
% 0.57/0.73 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | ((~value(in(n2, or1(f)), n0)) | value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(in(n2, or1(f)), n0)) | value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f)))))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(224,plain,
% 0.57/0.73 ((value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f)))) | (~value(in(n2, or1(f)), n0))) <=> ((~value(in(n2, or1(f)), n0)) | value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f)))))),
% 0.57/0.73 inference(rewrite,[status(thm)],[])).
% 0.57/0.73 tff(225,plain,
% 0.57/0.73 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f)))) | (~value(in(n2, or1(f)), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | ((~value(in(n2, or1(f)), n0)) | value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f))))))),
% 0.57/0.73 inference(monotonicity,[status(thm)],[224])).
% 0.57/0.73 tff(226,plain,
% 0.57/0.73 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f)))) | (~value(in(n2, or1(f)), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(in(n2, or1(f)), n0)) | value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f)))))),
% 0.57/0.73 inference(transitivity,[status(thm)],[225, 223])).
% 0.57/0.73 tff(227,plain,
% 0.57/0.73 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f)))) | (~value(in(n2, or1(f)), n0)))),
% 0.57/0.73 inference(quant_inst,[status(thm)],[])).
% 0.57/0.73 tff(228,plain,
% 0.57/0.73 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(in(n2, or1(f)), n0)) | value(out(c, h1(f)), n0) | (~connection(out(c, h1(f)), in(n2, or1(f))))),
% 0.57/0.73 inference(modus_ponens,[status(thm)],[227, 226])).
% 0.57/0.73 tff(229,plain,
% 0.57/0.73 ((~value(in(n2, or1(f)), n0)) | value(out(c, h1(f)), n0)),
% 0.57/0.73 inference(unit_resolution,[status(thm)],[228, 76, 222])).
% 0.57/0.73 tff(230,plain,
% 0.57/0.73 (~value(in(n2, or1(f)), n0)),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[229, 211])).
% 0.57/0.74 tff(231,assumption,(~value(out(n1, or1(f)), n0)), introduced(assumption)).
% 0.57/0.74 tff(232,plain,
% 0.57/0.74 (^[X: $i] : refl(((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X)))) <=> ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X)))))),
% 0.57/0.74 inference(bind,[status(th)],[])).
% 0.57/0.74 tff(233,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))),
% 0.57/0.74 inference(quant_intro,[status(thm)],[232])).
% 0.57/0.74 tff(234,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(235,axiom,(![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_connection_outc_out1or1')).
% 0.57/0.74 tff(236,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[235, 234])).
% 0.57/0.74 tff(237,plain,(
% 0.57/0.74 ![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))),
% 0.57/0.74 inference(skolemize,[status(sab)],[236])).
% 0.57/0.74 tff(238,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[237, 233])).
% 0.57/0.74 tff(239,plain,
% 0.57/0.74 (((~![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))) | ((~type(f, fulladder)) | connection(out(c, f), out(n1, or1(f))))) <=> ((~![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))) | (~type(f, fulladder)) | connection(out(c, f), out(n1, or1(f))))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(240,plain,
% 0.57/0.74 ((~![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))) | ((~type(f, fulladder)) | connection(out(c, f), out(n1, or1(f))))),
% 0.57/0.74 inference(quant_inst,[status(thm)],[])).
% 0.57/0.74 tff(241,plain,
% 0.57/0.74 ((~![X: $i] : ((~type(X, fulladder)) | connection(out(c, X), out(n1, or1(X))))) | (~type(f, fulladder)) | connection(out(c, f), out(n1, or1(f)))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[240, 239])).
% 0.57/0.74 tff(242,plain,
% 0.57/0.74 (connection(out(c, f), out(n1, or1(f)))),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[241, 238, 3])).
% 0.57/0.74 tff(243,plain,
% 0.57/0.74 (value(out(c, f), n0) <=> value(out(c, f), n0)),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(244,axiom,(value(out(c, f), n0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','outc_0')).
% 0.57/0.74 tff(245,plain,
% 0.57/0.74 (value(out(c, f), n0)),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[244, 243])).
% 0.57/0.74 tff(246,plain,
% 0.57/0.74 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f)))) | value(out(n1, or1(f)), n0))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f)))) | value(out(n1, or1(f)), n0))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(247,plain,
% 0.57/0.74 ((value(out(n1, or1(f)), n0) | (~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f))))) <=> ((~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f)))) | value(out(n1, or1(f)), n0))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(248,plain,
% 0.57/0.74 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(n1, or1(f)), n0) | (~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f)))) | value(out(n1, or1(f)), n0)))),
% 0.57/0.74 inference(monotonicity,[status(thm)],[247])).
% 0.57/0.74 tff(249,plain,
% 0.57/0.74 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(n1, or1(f)), n0) | (~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f)))) | value(out(n1, or1(f)), n0))),
% 0.57/0.74 inference(transitivity,[status(thm)],[248, 246])).
% 0.57/0.74 tff(250,plain,
% 0.57/0.74 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(n1, or1(f)), n0) | (~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f)))))),
% 0.57/0.74 inference(quant_inst,[status(thm)],[])).
% 0.57/0.74 tff(251,plain,
% 0.57/0.74 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(c, f), n0)) | (~connection(out(c, f), out(n1, or1(f)))) | value(out(n1, or1(f)), n0)),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[250, 249])).
% 0.57/0.74 tff(252,plain,
% 0.57/0.74 ($false),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[251, 27, 245, 242, 231])).
% 0.57/0.74 tff(253,plain,(value(out(n1, or1(f)), n0)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.74 tff(254,plain,
% 0.57/0.74 (^[X: $i] : refl(((~type(X, fulladder)) | type(or1(X), or)) <=> ((~type(X, fulladder)) | type(or1(X), or)))),
% 0.57/0.74 inference(bind,[status(th)],[])).
% 0.57/0.74 tff(255,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | type(or1(X), or)) <=> ![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))),
% 0.57/0.74 inference(quant_intro,[status(thm)],[254])).
% 0.57/0.74 tff(256,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | type(or1(X), or)) <=> ![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(257,axiom,(![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_or1')).
% 0.57/0.74 tff(258,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[257, 256])).
% 0.57/0.74 tff(259,plain,(
% 0.57/0.74 ![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))),
% 0.57/0.74 inference(skolemize,[status(sab)],[258])).
% 0.57/0.74 tff(260,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[259, 255])).
% 0.57/0.74 tff(261,plain,
% 0.57/0.74 (((~![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))) | ((~type(f, fulladder)) | type(or1(f), or))) <=> ((~![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))) | (~type(f, fulladder)) | type(or1(f), or))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(262,plain,
% 0.57/0.74 ((~![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))) | ((~type(f, fulladder)) | type(or1(f), or))),
% 0.57/0.74 inference(quant_inst,[status(thm)],[])).
% 0.57/0.74 tff(263,plain,
% 0.57/0.74 ((~![X: $i] : ((~type(X, fulladder)) | type(or1(X), or))) | (~type(f, fulladder)) | type(or1(f), or)),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[262, 261])).
% 0.57/0.74 tff(264,plain,
% 0.57/0.74 (type(or1(f), or)),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[263, 260, 3])).
% 0.57/0.74 tff(265,plain,
% 0.57/0.74 (^[K: $i] : refl(((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or))) <=> ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or))))),
% 0.57/0.74 inference(bind,[status(th)],[])).
% 0.57/0.74 tff(266,plain,
% 0.57/0.74 (![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or))) <=> ![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))),
% 0.57/0.74 inference(quant_intro,[status(thm)],[265])).
% 0.57/0.74 tff(267,plain,
% 0.57/0.74 (![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or))) <=> ![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(268,plain,
% 0.57/0.74 (^[K: $i] : trans(monotonicity(rewrite((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n0))) <=> ((~mode(K, ok)) | (~value(out(n1, K), n0)) | (~type(K, or)))), (((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n0))) | value(in(n2, K), n0)) <=> (((~mode(K, ok)) | (~value(out(n1, K), n0)) | (~type(K, or))) | value(in(n2, K), n0)))), rewrite((((~mode(K, ok)) | (~value(out(n1, K), n0)) | (~type(K, or))) | value(in(n2, K), n0)) <=> ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))), (((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n0))) | value(in(n2, K), n0)) <=> ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))))),
% 0.57/0.74 inference(bind,[status(th)],[])).
% 0.57/0.74 tff(269,plain,
% 0.57/0.74 (![K: $i] : ((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n0))) | value(in(n2, K), n0)) <=> ![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))),
% 0.57/0.74 inference(quant_intro,[status(thm)],[268])).
% 0.57/0.74 tff(270,axiom,(![K: $i] : ((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n0))) | value(in(n2, K), n0))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','or_0_01')).
% 0.57/0.74 tff(271,plain,
% 0.57/0.74 (![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[270, 269])).
% 0.57/0.74 tff(272,plain,
% 0.57/0.74 (![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[271, 267])).
% 0.57/0.74 tff(273,plain,(
% 0.57/0.74 ![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))),
% 0.57/0.74 inference(skolemize,[status(sab)],[272])).
% 0.57/0.74 tff(274,plain,
% 0.57/0.74 (![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[273, 266])).
% 0.57/0.74 tff(275,plain,
% 0.57/0.74 (((~![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))) | ((~mode(or1(f), ok)) | (~value(out(n1, or1(f)), n0)) | value(in(n2, or1(f)), n0) | (~type(or1(f), or)))) <=> ((~![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))) | (~mode(or1(f), ok)) | (~value(out(n1, or1(f)), n0)) | value(in(n2, or1(f)), n0) | (~type(or1(f), or)))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(276,plain,
% 0.57/0.74 (((~mode(or1(f), ok)) | value(in(n2, or1(f)), n0) | (~value(out(n1, or1(f)), n0)) | (~type(or1(f), or))) <=> ((~mode(or1(f), ok)) | (~value(out(n1, or1(f)), n0)) | value(in(n2, or1(f)), n0) | (~type(or1(f), or)))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(277,plain,
% 0.57/0.74 (((~![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))) | ((~mode(or1(f), ok)) | value(in(n2, or1(f)), n0) | (~value(out(n1, or1(f)), n0)) | (~type(or1(f), or)))) <=> ((~![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))) | ((~mode(or1(f), ok)) | (~value(out(n1, or1(f)), n0)) | value(in(n2, or1(f)), n0) | (~type(or1(f), or))))),
% 0.57/0.74 inference(monotonicity,[status(thm)],[276])).
% 0.57/0.74 tff(278,plain,
% 0.57/0.74 (((~![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))) | ((~mode(or1(f), ok)) | value(in(n2, or1(f)), n0) | (~value(out(n1, or1(f)), n0)) | (~type(or1(f), or)))) <=> ((~![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))) | (~mode(or1(f), ok)) | (~value(out(n1, or1(f)), n0)) | value(in(n2, or1(f)), n0) | (~type(or1(f), or)))),
% 0.57/0.74 inference(transitivity,[status(thm)],[277, 275])).
% 0.57/0.74 tff(279,plain,
% 0.57/0.74 ((~![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))) | ((~mode(or1(f), ok)) | value(in(n2, or1(f)), n0) | (~value(out(n1, or1(f)), n0)) | (~type(or1(f), or)))),
% 0.57/0.74 inference(quant_inst,[status(thm)],[])).
% 0.57/0.74 tff(280,plain,
% 0.57/0.74 ((~![K: $i] : ((~mode(K, ok)) | value(in(n2, K), n0) | (~value(out(n1, K), n0)) | (~type(K, or)))) | (~mode(or1(f), ok)) | (~value(out(n1, or1(f)), n0)) | value(in(n2, or1(f)), n0) | (~type(or1(f), or))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[279, 278])).
% 0.57/0.74 tff(281,plain,
% 0.57/0.74 ((~mode(or1(f), ok)) | (~value(out(n1, or1(f)), n0)) | value(in(n2, or1(f)), n0)),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[280, 274, 264])).
% 0.57/0.74 tff(282,plain,
% 0.57/0.74 ((~mode(or1(f), ok)) | value(in(n2, or1(f)), n0)),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[281, 253])).
% 0.57/0.74 tff(283,plain,
% 0.57/0.74 (~mode(or1(f), ok)),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[282, 230])).
% 0.57/0.74 tff(284,plain,
% 0.57/0.74 (((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(or1(f), abnormal) | mode(or1(f), ok) | (~type(or1(f), or)))) <=> ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(or1(f), abnormal) | mode(or1(f), ok) | (~type(or1(f), or)))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(285,plain,
% 0.57/0.74 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(or1(f), abnormal) | mode(or1(f), ok) | (~type(or1(f), or)))),
% 0.57/0.74 inference(quant_inst,[status(thm)],[])).
% 0.57/0.74 tff(286,plain,
% 0.57/0.74 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(or1(f), abnormal) | mode(or1(f), ok) | (~type(or1(f), or))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[285, 284])).
% 0.57/0.74 tff(287,plain,
% 0.57/0.74 (mode(or1(f), abnormal) | mode(or1(f), ok)),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[286, 133, 264])).
% 0.57/0.74 tff(288,plain,
% 0.57/0.74 (mode(or1(f), abnormal)),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[287, 283])).
% 0.57/0.74 tff(289,plain,
% 0.57/0.74 (((~mode(or1(f), abnormal)) | (~mode(and1(h2(f)), abnormal))) <=> ((~mode(or1(f), abnormal)) | (~mode(and1(h2(f)), abnormal)))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(290,axiom,((~mode(or1(f), abnormal)) | (~mode(and1(h2(f)), abnormal))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','diagnosis_or1_and1h2')).
% 0.57/0.74 tff(291,plain,
% 0.57/0.74 ((~mode(or1(f), abnormal)) | (~mode(and1(h2(f)), abnormal))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[290, 289])).
% 0.57/0.74 tff(292,plain,
% 0.57/0.74 (~mode(and1(h2(f)), abnormal)),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[291, 288])).
% 0.57/0.74 tff(293,plain,
% 0.57/0.74 (^[X: $i] : refl(((~type(X, fulladder)) | type(h2(X), halfadder)) <=> ((~type(X, fulladder)) | type(h2(X), halfadder)))),
% 0.57/0.74 inference(bind,[status(th)],[])).
% 0.57/0.74 tff(294,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder)) <=> ![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))),
% 0.57/0.74 inference(quant_intro,[status(thm)],[293])).
% 0.57/0.74 tff(295,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder)) <=> ![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(296,axiom,(![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_halfadder2')).
% 0.57/0.74 tff(297,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[296, 295])).
% 0.57/0.74 tff(298,plain,(
% 0.57/0.74 ![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))),
% 0.57/0.74 inference(skolemize,[status(sab)],[297])).
% 0.57/0.74 tff(299,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[298, 294])).
% 0.57/0.74 tff(300,plain,
% 0.57/0.74 (((~![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))) | ((~type(f, fulladder)) | type(h2(f), halfadder))) <=> ((~![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))) | (~type(f, fulladder)) | type(h2(f), halfadder))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(301,plain,
% 0.57/0.74 ((~![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))) | ((~type(f, fulladder)) | type(h2(f), halfadder))),
% 0.57/0.74 inference(quant_inst,[status(thm)],[])).
% 0.57/0.74 tff(302,plain,
% 0.57/0.74 ((~![X: $i] : ((~type(X, fulladder)) | type(h2(X), halfadder))) | (~type(f, fulladder)) | type(h2(f), halfadder)),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[301, 300])).
% 0.57/0.74 tff(303,plain,
% 0.57/0.74 (type(h2(f), halfadder)),
% 0.57/0.74 inference(unit_resolution,[status(thm)],[302, 299, 3])).
% 0.57/0.74 tff(304,plain,
% 0.57/0.74 (^[X: $i] : refl(((~type(X, halfadder)) | type(and1(X), and)) <=> ((~type(X, halfadder)) | type(and1(X), and)))),
% 0.57/0.74 inference(bind,[status(th)],[])).
% 0.57/0.74 tff(305,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, halfadder)) | type(and1(X), and)) <=> ![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))),
% 0.57/0.74 inference(quant_intro,[status(thm)],[304])).
% 0.57/0.74 tff(306,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, halfadder)) | type(and1(X), and)) <=> ![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(307,axiom,(![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_and1')).
% 0.57/0.74 tff(308,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[307, 306])).
% 0.57/0.74 tff(309,plain,(
% 0.57/0.74 ![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))),
% 0.57/0.74 inference(skolemize,[status(sab)],[308])).
% 0.57/0.74 tff(310,plain,
% 0.57/0.74 (![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[309, 305])).
% 0.57/0.74 tff(311,plain,
% 0.57/0.74 (((~![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))) | ((~type(h2(f), halfadder)) | type(and1(h2(f)), and))) <=> ((~![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))) | (~type(h2(f), halfadder)) | type(and1(h2(f)), and))),
% 0.57/0.74 inference(rewrite,[status(thm)],[])).
% 0.57/0.74 tff(312,plain,
% 0.57/0.74 ((~![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))) | ((~type(h2(f), halfadder)) | type(and1(h2(f)), and))),
% 0.57/0.74 inference(quant_inst,[status(thm)],[])).
% 0.57/0.74 tff(313,plain,
% 0.57/0.74 ((~![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))) | (~type(h2(f), halfadder)) | type(and1(h2(f)), and)),
% 0.57/0.74 inference(modus_ponens,[status(thm)],[312, 311])).
% 0.57/0.75 tff(314,plain,
% 0.57/0.75 (type(and1(h2(f)), and)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[313, 310, 303])).
% 0.57/0.75 tff(315,plain,
% 0.57/0.75 (((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(and1(h2(f)), abnormal) | mode(and1(h2(f)), ok) | (~type(and1(h2(f)), and)))) <=> ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(and1(h2(f)), abnormal) | mode(and1(h2(f)), ok) | (~type(and1(h2(f)), and)))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(316,plain,
% 0.57/0.75 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(and1(h2(f)), abnormal) | mode(and1(h2(f)), ok) | (~type(and1(h2(f)), and)))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(317,plain,
% 0.57/0.75 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(and1(h2(f)), abnormal) | mode(and1(h2(f)), ok) | (~type(and1(h2(f)), and))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[316, 315])).
% 0.57/0.75 tff(318,plain,
% 0.57/0.75 (mode(and1(h2(f)), abnormal) | mode(and1(h2(f)), ok)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[317, 133, 314])).
% 0.57/0.75 tff(319,plain,
% 0.57/0.75 (mode(and1(h2(f)), ok)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[318, 292])).
% 0.57/0.75 tff(320,plain,
% 0.57/0.75 (((~mode(or1(f), abnormal)) | (~mode(or1(h2(f)), abnormal))) <=> ((~mode(or1(f), abnormal)) | (~mode(or1(h2(f)), abnormal)))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(321,axiom,((~mode(or1(f), abnormal)) | (~mode(or1(h2(f)), abnormal))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','diagnosis_or1_or1h2')).
% 0.57/0.75 tff(322,plain,
% 0.57/0.75 ((~mode(or1(f), abnormal)) | (~mode(or1(h2(f)), abnormal))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[321, 320])).
% 0.57/0.75 tff(323,plain,
% 0.57/0.75 (~mode(or1(h2(f)), abnormal)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[322, 288])).
% 0.57/0.75 tff(324,plain,
% 0.57/0.75 (^[X: $i] : refl(((~type(X, halfadder)) | type(or1(X), or)) <=> ((~type(X, halfadder)) | type(or1(X), or)))),
% 0.57/0.75 inference(bind,[status(th)],[])).
% 0.57/0.75 tff(325,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | type(or1(X), or)) <=> ![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))),
% 0.57/0.75 inference(quant_intro,[status(thm)],[324])).
% 0.57/0.75 tff(326,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | type(or1(X), or)) <=> ![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(327,axiom,(![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_or1')).
% 0.57/0.75 tff(328,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[327, 326])).
% 0.57/0.75 tff(329,plain,(
% 0.57/0.75 ![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))),
% 0.57/0.75 inference(skolemize,[status(sab)],[328])).
% 0.57/0.75 tff(330,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[329, 325])).
% 0.57/0.75 tff(331,plain,
% 0.57/0.75 (((~![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))) | ((~type(h2(f), halfadder)) | type(or1(h2(f)), or))) <=> ((~![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))) | (~type(h2(f), halfadder)) | type(or1(h2(f)), or))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(332,plain,
% 0.57/0.75 ((~![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))) | ((~type(h2(f), halfadder)) | type(or1(h2(f)), or))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(333,plain,
% 0.57/0.75 ((~![X: $i] : ((~type(X, halfadder)) | type(or1(X), or))) | (~type(h2(f), halfadder)) | type(or1(h2(f)), or)),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[332, 331])).
% 0.57/0.75 tff(334,plain,
% 0.57/0.75 (type(or1(h2(f)), or)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[333, 330, 303])).
% 0.57/0.75 tff(335,plain,
% 0.57/0.75 (((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(or1(h2(f)), abnormal) | mode(or1(h2(f)), ok) | (~type(or1(h2(f)), or)))) <=> ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(or1(h2(f)), abnormal) | mode(or1(h2(f)), ok) | (~type(or1(h2(f)), or)))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(336,plain,
% 0.57/0.75 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(or1(h2(f)), abnormal) | mode(or1(h2(f)), ok) | (~type(or1(h2(f)), or)))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(337,plain,
% 0.57/0.75 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(or1(h2(f)), abnormal) | mode(or1(h2(f)), ok) | (~type(or1(h2(f)), or))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[336, 335])).
% 0.57/0.75 tff(338,plain,
% 0.57/0.75 (mode(or1(h2(f)), abnormal) | mode(or1(h2(f)), ok)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[337, 133, 334])).
% 0.57/0.75 tff(339,plain,
% 0.57/0.75 (mode(or1(h2(f)), ok)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[338, 323])).
% 0.57/0.75 tff(340,plain,
% 0.57/0.75 (^[X: $i] : refl(((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X)))) <=> ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X)))))),
% 0.57/0.75 inference(bind,[status(th)],[])).
% 0.57/0.75 tff(341,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))),
% 0.57/0.75 inference(quant_intro,[status(thm)],[340])).
% 0.57/0.75 tff(342,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(343,axiom,(![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_connection_in2_in2or1')).
% 0.57/0.75 tff(344,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[343, 342])).
% 0.57/0.75 tff(345,plain,(
% 0.57/0.75 ![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))),
% 0.57/0.75 inference(skolemize,[status(sab)],[344])).
% 0.57/0.75 tff(346,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[345, 341])).
% 0.57/0.75 tff(347,plain,
% 0.57/0.75 (((~![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))) | ((~type(h2(f), halfadder)) | connection(in(n2, h2(f)), in(n2, or1(h2(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))) | (~type(h2(f), halfadder)) | connection(in(n2, h2(f)), in(n2, or1(h2(f)))))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(348,plain,
% 0.57/0.75 ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))) | ((~type(h2(f), halfadder)) | connection(in(n2, h2(f)), in(n2, or1(h2(f)))))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(349,plain,
% 0.57/0.75 ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n2, X), in(n2, or1(X))))) | (~type(h2(f), halfadder)) | connection(in(n2, h2(f)), in(n2, or1(h2(f))))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[348, 347])).
% 0.57/0.75 tff(350,plain,
% 0.57/0.75 (connection(in(n2, h2(f)), in(n2, or1(h2(f))))),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[349, 346, 303])).
% 0.57/0.75 tff(351,plain,
% 0.57/0.75 (((~mode(or1(f), abnormal)) | (~mode(and1(h1(f)), abnormal))) <=> ((~mode(or1(f), abnormal)) | (~mode(and1(h1(f)), abnormal)))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(352,axiom,((~mode(or1(f), abnormal)) | (~mode(and1(h1(f)), abnormal))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','diagnosis_or1_and1h1')).
% 0.57/0.75 tff(353,plain,
% 0.57/0.75 ((~mode(or1(f), abnormal)) | (~mode(and1(h1(f)), abnormal))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[352, 351])).
% 0.57/0.75 tff(354,plain,
% 0.57/0.75 (~mode(and1(h1(f)), abnormal)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[353, 288])).
% 0.57/0.75 tff(355,plain,
% 0.57/0.75 (((~![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))) | ((~type(h1(f), halfadder)) | type(and1(h1(f)), and))) <=> ((~![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))) | (~type(h1(f), halfadder)) | type(and1(h1(f)), and))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(356,plain,
% 0.57/0.75 ((~![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))) | ((~type(h1(f), halfadder)) | type(and1(h1(f)), and))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(357,plain,
% 0.57/0.75 ((~![X: $i] : ((~type(X, halfadder)) | type(and1(X), and))) | (~type(h1(f), halfadder)) | type(and1(h1(f)), and)),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[356, 355])).
% 0.57/0.75 tff(358,plain,
% 0.57/0.75 (type(and1(h1(f)), and)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[357, 310, 91])).
% 0.57/0.75 tff(359,plain,
% 0.57/0.75 (((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(and1(h1(f)), abnormal) | mode(and1(h1(f)), ok) | (~type(and1(h1(f)), and)))) <=> ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(and1(h1(f)), abnormal) | mode(and1(h1(f)), ok) | (~type(and1(h1(f)), and)))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(360,plain,
% 0.57/0.75 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(and1(h1(f)), abnormal) | mode(and1(h1(f)), ok) | (~type(and1(h1(f)), and)))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(361,plain,
% 0.57/0.75 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(and1(h1(f)), abnormal) | mode(and1(h1(f)), ok) | (~type(and1(h1(f)), and))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[360, 359])).
% 0.57/0.75 tff(362,plain,
% 0.57/0.75 (mode(and1(h1(f)), abnormal) | mode(and1(h1(f)), ok)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[361, 133, 358])).
% 0.57/0.75 tff(363,plain,
% 0.57/0.75 (mode(and1(h1(f)), ok)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[362, 354])).
% 0.57/0.75 tff(364,plain,
% 0.57/0.75 (((~mode(or1(f), abnormal)) | (~mode(not1(h1(f)), abnormal))) <=> ((~mode(or1(f), abnormal)) | (~mode(not1(h1(f)), abnormal)))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(365,axiom,((~mode(or1(f), abnormal)) | (~mode(not1(h1(f)), abnormal))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','diagnosis_or1_not1h1')).
% 0.57/0.75 tff(366,plain,
% 0.57/0.75 ((~mode(or1(f), abnormal)) | (~mode(not1(h1(f)), abnormal))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[365, 364])).
% 0.57/0.75 tff(367,plain,
% 0.57/0.75 (~mode(not1(h1(f)), abnormal)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[366, 288])).
% 0.57/0.75 tff(368,plain,
% 0.57/0.75 (^[X: $i] : refl(((~type(X, halfadder)) | type(not1(X), not)) <=> ((~type(X, halfadder)) | type(not1(X), not)))),
% 0.57/0.75 inference(bind,[status(th)],[])).
% 0.57/0.75 tff(369,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | type(not1(X), not)) <=> ![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))),
% 0.57/0.75 inference(quant_intro,[status(thm)],[368])).
% 0.57/0.75 tff(370,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | type(not1(X), not)) <=> ![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(371,axiom,(![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_not1')).
% 0.57/0.75 tff(372,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[371, 370])).
% 0.57/0.75 tff(373,plain,(
% 0.57/0.75 ![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))),
% 0.57/0.75 inference(skolemize,[status(sab)],[372])).
% 0.57/0.75 tff(374,plain,
% 0.57/0.75 (![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[373, 369])).
% 0.57/0.75 tff(375,plain,
% 0.57/0.75 (((~![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))) | ((~type(h1(f), halfadder)) | type(not1(h1(f)), not))) <=> ((~![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))) | (~type(h1(f), halfadder)) | type(not1(h1(f)), not))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(376,plain,
% 0.57/0.75 ((~![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))) | ((~type(h1(f), halfadder)) | type(not1(h1(f)), not))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(377,plain,
% 0.57/0.75 ((~![X: $i] : ((~type(X, halfadder)) | type(not1(X), not))) | (~type(h1(f), halfadder)) | type(not1(h1(f)), not)),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[376, 375])).
% 0.57/0.75 tff(378,plain,
% 0.57/0.75 (type(not1(h1(f)), not)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[377, 374, 91])).
% 0.57/0.75 tff(379,plain,
% 0.57/0.75 (((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(not1(h1(f)), abnormal) | mode(not1(h1(f)), ok) | (~type(not1(h1(f)), not)))) <=> ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(not1(h1(f)), abnormal) | mode(not1(h1(f)), ok) | (~type(not1(h1(f)), not)))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(380,plain,
% 0.57/0.75 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | (mode(not1(h1(f)), abnormal) | mode(not1(h1(f)), ok) | (~type(not1(h1(f)), not)))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(381,plain,
% 0.57/0.75 ((~![Any: $i, K: $i] : (mode(K, abnormal) | mode(K, ok) | (~type(K, Any)))) | mode(not1(h1(f)), abnormal) | mode(not1(h1(f)), ok) | (~type(not1(h1(f)), not))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[380, 379])).
% 0.57/0.75 tff(382,plain,
% 0.57/0.75 (mode(not1(h1(f)), abnormal) | mode(not1(h1(f)), ok)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[381, 133, 378])).
% 0.57/0.75 tff(383,plain,
% 0.57/0.75 (mode(not1(h1(f)), ok)),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[382, 367])).
% 0.57/0.75 tff(384,assumption,(~value(in(n1, not1(h1(f))), n1)), introduced(assumption)).
% 0.57/0.75 tff(385,assumption,(~value(in(n1, h1(f)), n1)), introduced(assumption)).
% 0.57/0.75 tff(386,plain,
% 0.57/0.75 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f)))) | value(in(n1, h1(f)), n1))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f)))) | value(in(n1, h1(f)), n1))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(387,plain,
% 0.57/0.75 ((value(in(n1, h1(f)), n1) | (~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f))))) <=> ((~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f)))) | value(in(n1, h1(f)), n1))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(388,plain,
% 0.57/0.75 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n1, h1(f)), n1) | (~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f)))) | value(in(n1, h1(f)), n1)))),
% 0.57/0.75 inference(monotonicity,[status(thm)],[387])).
% 0.57/0.75 tff(389,plain,
% 0.57/0.75 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n1, h1(f)), n1) | (~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f)))) | value(in(n1, h1(f)), n1))),
% 0.57/0.75 inference(transitivity,[status(thm)],[388, 386])).
% 0.57/0.75 tff(390,plain,
% 0.57/0.75 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n1, h1(f)), n1) | (~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f)))))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(391,plain,
% 0.57/0.75 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(in(n2, f), n1)) | (~connection(in(n2, f), in(n1, h1(f)))) | value(in(n1, h1(f)), n1)),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[390, 389])).
% 0.57/0.75 tff(392,plain,
% 0.57/0.75 ($false),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[391, 27, 151, 148, 385])).
% 0.57/0.75 tff(393,plain,(value(in(n1, h1(f)), n1)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.75 tff(394,assumption,(~value(in(n1, and2(h1(f))), n1)), introduced(assumption)).
% 0.57/0.75 tff(395,plain,
% 0.57/0.75 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n1, and2(h1(f))), n1) | (~value(in(n1, h1(f)), n1)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | value(in(n1, and2(h1(f))), n1) | (~value(in(n1, h1(f)), n1)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(396,plain,
% 0.57/0.75 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n1, and2(h1(f))), n1) | (~value(in(n1, h1(f)), n1)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f))))))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(397,plain,
% 0.57/0.75 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | value(in(n1, and2(h1(f))), n1) | (~value(in(n1, h1(f)), n1)) | (~connection(in(n1, h1(f)), in(n1, and2(h1(f)))))),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[396, 395])).
% 0.57/0.75 tff(398,plain,
% 0.57/0.75 ($false),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[397, 27, 170, 394, 393])).
% 0.57/0.75 tff(399,plain,(value(in(n1, and2(h1(f))), n1)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.75 tff(400,assumption,(~value(in(n2, h1(f)), n1)), introduced(assumption)).
% 0.57/0.75 tff(401,plain,
% 0.57/0.75 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f)))) | value(in(n2, h1(f)), n1))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f)))) | value(in(n2, h1(f)), n1))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(402,plain,
% 0.57/0.75 ((value(in(n2, h1(f)), n1) | (~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f))))) <=> ((~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f)))) | value(in(n2, h1(f)), n1))),
% 0.57/0.75 inference(rewrite,[status(thm)],[])).
% 0.57/0.75 tff(403,plain,
% 0.57/0.75 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n2, h1(f)), n1) | (~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f)))) | value(in(n2, h1(f)), n1)))),
% 0.57/0.75 inference(monotonicity,[status(thm)],[402])).
% 0.57/0.75 tff(404,plain,
% 0.57/0.75 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n2, h1(f)), n1) | (~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f)))) | value(in(n2, h1(f)), n1))),
% 0.57/0.75 inference(transitivity,[status(thm)],[403, 401])).
% 0.57/0.75 tff(405,plain,
% 0.57/0.75 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n2, h1(f)), n1) | (~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f)))))),
% 0.57/0.75 inference(quant_inst,[status(thm)],[])).
% 0.57/0.75 tff(406,plain,
% 0.57/0.75 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(in(c, f), n1)) | (~connection(in(c, f), in(n2, h1(f)))) | value(in(n2, h1(f)), n1)),
% 0.57/0.75 inference(modus_ponens,[status(thm)],[405, 404])).
% 0.57/0.75 tff(407,plain,
% 0.57/0.75 ($false),
% 0.57/0.75 inference(unit_resolution,[status(thm)],[406, 27, 49, 46, 400])).
% 0.57/0.75 tff(408,plain,(value(in(n2, h1(f)), n1)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.75 tff(409,assumption,(~value(in(n2, and2(h1(f))), n1)), introduced(assumption)).
% 0.57/0.75 tff(410,plain,
% 0.57/0.75 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n2, and2(h1(f))), n1) | (~value(in(n2, h1(f)), n1)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | value(in(n2, and2(h1(f))), n1) | (~value(in(n2, h1(f)), n1)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))))),
% 0.57/0.76 inference(rewrite,[status(thm)],[])).
% 0.57/0.76 tff(411,plain,
% 0.57/0.76 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n2, and2(h1(f))), n1) | (~value(in(n2, h1(f)), n1)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f))))))),
% 0.57/0.76 inference(quant_inst,[status(thm)],[])).
% 0.57/0.76 tff(412,plain,
% 0.57/0.76 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | value(in(n2, and2(h1(f))), n1) | (~value(in(n2, h1(f)), n1)) | (~connection(in(n2, h1(f)), in(n2, and2(h1(f)))))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[411, 410])).
% 0.57/0.76 tff(413,plain,
% 0.57/0.76 ($false),
% 0.57/0.76 inference(unit_resolution,[status(thm)],[412, 27, 102, 409, 408])).
% 0.57/0.76 tff(414,plain,(value(in(n2, and2(h1(f))), n1)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.76 tff(415,plain,
% 0.57/0.76 (^[K: $i] : refl(((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1))) <=> ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1))))),
% 0.57/0.76 inference(bind,[status(th)],[])).
% 0.57/0.76 tff(416,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1))) <=> ![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))),
% 0.57/0.76 inference(quant_intro,[status(thm)],[415])).
% 0.57/0.76 tff(417,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1))) <=> ![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))),
% 0.57/0.76 inference(rewrite,[status(thm)],[])).
% 0.57/0.76 tff(418,plain,
% 0.57/0.76 (^[K: $i] : trans(monotonicity(trans(monotonicity(rewrite((((~mode(K, ok)) | (~type(K, and))) | (~value(in(n1, K), n1))) <=> ((~mode(K, ok)) | (~type(K, and)) | (~value(in(n1, K), n1)))), (((((~mode(K, ok)) | (~type(K, and))) | (~value(in(n1, K), n1))) | (~value(in(n2, K), n1))) <=> (((~mode(K, ok)) | (~type(K, and)) | (~value(in(n1, K), n1))) | (~value(in(n2, K), n1))))), rewrite((((~mode(K, ok)) | (~type(K, and)) | (~value(in(n1, K), n1))) | (~value(in(n2, K), n1))) <=> ((~mode(K, ok)) | (~type(K, and)) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))), (((((~mode(K, ok)) | (~type(K, and))) | (~value(in(n1, K), n1))) | (~value(in(n2, K), n1))) <=> ((~mode(K, ok)) | (~type(K, and)) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1))))), ((((((~mode(K, ok)) | (~type(K, and))) | (~value(in(n1, K), n1))) | (~value(in(n2, K), n1))) | value(out(n1, K), n1)) <=> (((~mode(K, ok)) | (~type(K, and)) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1))) | value(out(n1, K), n1)))), rewrite((((~mode(K, ok)) | (~type(K, and)) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1))) | value(out(n1, K), n1)) <=> ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))), ((((((~mode(K, ok)) | (~type(K, and))) | (~value(in(n1, K), n1))) | (~value(in(n2, K), n1))) | value(out(n1, K), n1)) <=> ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))))),
% 0.57/0.76 inference(bind,[status(th)],[])).
% 0.57/0.76 tff(419,plain,
% 0.57/0.76 (![K: $i] : (((((~mode(K, ok)) | (~type(K, and))) | (~value(in(n1, K), n1))) | (~value(in(n2, K), n1))) | value(out(n1, K), n1)) <=> ![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))),
% 0.57/0.76 inference(quant_intro,[status(thm)],[418])).
% 0.57/0.76 tff(420,axiom,(![K: $i] : (((((~mode(K, ok)) | (~type(K, and))) | (~value(in(n1, K), n1))) | (~value(in(n2, K), n1))) | value(out(n1, K), n1))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','and_11_1')).
% 0.57/0.76 tff(421,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[420, 419])).
% 0.57/0.76 tff(422,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[421, 417])).
% 0.57/0.76 tff(423,plain,(
% 0.57/0.76 ![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))),
% 0.57/0.76 inference(skolemize,[status(sab)],[422])).
% 0.57/0.76 tff(424,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[423, 416])).
% 0.57/0.76 tff(425,plain,
% 0.57/0.76 (((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))) | ((~mode(and2(h1(f)), ok)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n1, and2(h1(f))), n1)) | (~type(and2(h1(f)), and)) | (~value(in(n2, and2(h1(f))), n1)))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))) | (~mode(and2(h1(f)), ok)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n1, and2(h1(f))), n1)) | (~type(and2(h1(f)), and)) | (~value(in(n2, and2(h1(f))), n1)))),
% 0.57/0.76 inference(rewrite,[status(thm)],[])).
% 0.57/0.76 tff(426,plain,
% 0.57/0.76 (((~mode(and2(h1(f)), ok)) | (~type(and2(h1(f)), and)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n2, and2(h1(f))), n1)) | (~value(in(n1, and2(h1(f))), n1))) <=> ((~mode(and2(h1(f)), ok)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n1, and2(h1(f))), n1)) | (~type(and2(h1(f)), and)) | (~value(in(n2, and2(h1(f))), n1)))),
% 0.57/0.76 inference(rewrite,[status(thm)],[])).
% 0.57/0.76 tff(427,plain,
% 0.57/0.76 (((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))) | ((~mode(and2(h1(f)), ok)) | (~type(and2(h1(f)), and)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n2, and2(h1(f))), n1)) | (~value(in(n1, and2(h1(f))), n1)))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))) | ((~mode(and2(h1(f)), ok)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n1, and2(h1(f))), n1)) | (~type(and2(h1(f)), and)) | (~value(in(n2, and2(h1(f))), n1))))),
% 0.57/0.76 inference(monotonicity,[status(thm)],[426])).
% 0.57/0.76 tff(428,plain,
% 0.57/0.76 (((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))) | ((~mode(and2(h1(f)), ok)) | (~type(and2(h1(f)), and)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n2, and2(h1(f))), n1)) | (~value(in(n1, and2(h1(f))), n1)))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))) | (~mode(and2(h1(f)), ok)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n1, and2(h1(f))), n1)) | (~type(and2(h1(f)), and)) | (~value(in(n2, and2(h1(f))), n1)))),
% 0.57/0.76 inference(transitivity,[status(thm)],[427, 425])).
% 0.57/0.76 tff(429,plain,
% 0.57/0.76 ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))) | ((~mode(and2(h1(f)), ok)) | (~type(and2(h1(f)), and)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n2, and2(h1(f))), n1)) | (~value(in(n1, and2(h1(f))), n1)))),
% 0.57/0.76 inference(quant_inst,[status(thm)],[])).
% 0.57/0.76 tff(430,plain,
% 0.57/0.76 ((~![K: $i] : ((~mode(K, ok)) | (~type(K, and)) | value(out(n1, K), n1) | (~value(in(n2, K), n1)) | (~value(in(n1, K), n1)))) | (~mode(and2(h1(f)), ok)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n1, and2(h1(f))), n1)) | (~type(and2(h1(f)), and)) | (~value(in(n2, and2(h1(f))), n1))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[429, 428])).
% 0.57/0.76 tff(431,plain,
% 0.57/0.76 ((~mode(and2(h1(f)), ok)) | value(out(n1, and2(h1(f))), n1) | (~value(in(n1, and2(h1(f))), n1)) | (~value(in(n2, and2(h1(f))), n1))),
% 0.57/0.76 inference(unit_resolution,[status(thm)],[430, 424, 120])).
% 0.57/0.76 tff(432,plain,
% 0.57/0.76 (value(out(n1, and2(h1(f))), n1) | (~value(in(n1, and2(h1(f))), n1)) | (~value(in(n2, and2(h1(f))), n1))),
% 0.57/0.76 inference(unit_resolution,[status(thm)],[431, 137])).
% 0.57/0.76 tff(433,plain,
% 0.57/0.76 (value(out(n1, and2(h1(f))), n1) | (~value(in(n1, and2(h1(f))), n1))),
% 0.57/0.76 inference(unit_resolution,[status(thm)],[432, 414])).
% 0.57/0.76 tff(434,plain,
% 0.57/0.76 (value(out(n1, and2(h1(f))), n1)),
% 0.57/0.76 inference(unit_resolution,[status(thm)],[433, 399])).
% 0.57/0.76 tff(435,plain,
% 0.57/0.76 (^[X: $i] : refl(((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X)))) <=> ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X)))))),
% 0.57/0.76 inference(bind,[status(th)],[])).
% 0.57/0.76 tff(436,plain,
% 0.57/0.76 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))),
% 0.57/0.76 inference(quant_intro,[status(thm)],[435])).
% 0.57/0.76 tff(437,plain,
% 0.57/0.76 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))),
% 0.57/0.76 inference(rewrite,[status(thm)],[])).
% 0.57/0.76 tff(438,axiom,(![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_connection_out1and2_in1not1')).
% 0.57/0.76 tff(439,plain,
% 0.57/0.76 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[438, 437])).
% 0.57/0.76 tff(440,plain,(
% 0.57/0.76 ![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))),
% 0.57/0.76 inference(skolemize,[status(sab)],[439])).
% 0.57/0.76 tff(441,plain,
% 0.57/0.76 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[440, 436])).
% 0.57/0.76 tff(442,plain,
% 0.57/0.76 (((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))) | ((~type(h1(f), halfadder)) | connection(out(n1, and2(h1(f))), in(n1, not1(h1(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))) | (~type(h1(f), halfadder)) | connection(out(n1, and2(h1(f))), in(n1, not1(h1(f)))))),
% 0.57/0.76 inference(rewrite,[status(thm)],[])).
% 0.57/0.76 tff(443,plain,
% 0.57/0.76 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))) | ((~type(h1(f), halfadder)) | connection(out(n1, and2(h1(f))), in(n1, not1(h1(f)))))),
% 0.57/0.76 inference(quant_inst,[status(thm)],[])).
% 0.57/0.76 tff(444,plain,
% 0.57/0.76 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, and2(X)), in(n1, not1(X))))) | (~type(h1(f), halfadder)) | connection(out(n1, and2(h1(f))), in(n1, not1(h1(f))))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[443, 442])).
% 0.57/0.76 tff(445,plain,
% 0.57/0.76 (connection(out(n1, and2(h1(f))), in(n1, not1(h1(f))))),
% 0.57/0.76 inference(unit_resolution,[status(thm)],[444, 441, 91])).
% 0.57/0.76 tff(446,plain,
% 0.57/0.76 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(out(n1, and2(h1(f))), n1)) | value(in(n1, not1(h1(f))), n1) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(n1, and2(h1(f))), n1)) | value(in(n1, not1(h1(f))), n1) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f))))))),
% 0.57/0.76 inference(rewrite,[status(thm)],[])).
% 0.57/0.76 tff(447,plain,
% 0.57/0.76 ((value(in(n1, not1(h1(f))), n1) | (~value(out(n1, and2(h1(f))), n1)) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f)))))) <=> ((~value(out(n1, and2(h1(f))), n1)) | value(in(n1, not1(h1(f))), n1) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f))))))),
% 0.57/0.76 inference(rewrite,[status(thm)],[])).
% 0.57/0.76 tff(448,plain,
% 0.57/0.76 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n1, not1(h1(f))), n1) | (~value(out(n1, and2(h1(f))), n1)) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(out(n1, and2(h1(f))), n1)) | value(in(n1, not1(h1(f))), n1) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f)))))))),
% 0.57/0.76 inference(monotonicity,[status(thm)],[447])).
% 0.57/0.76 tff(449,plain,
% 0.57/0.76 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n1, not1(h1(f))), n1) | (~value(out(n1, and2(h1(f))), n1)) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(n1, and2(h1(f))), n1)) | value(in(n1, not1(h1(f))), n1) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f))))))),
% 0.57/0.76 inference(transitivity,[status(thm)],[448, 446])).
% 0.57/0.76 tff(450,plain,
% 0.57/0.76 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n1, not1(h1(f))), n1) | (~value(out(n1, and2(h1(f))), n1)) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f))))))),
% 0.57/0.76 inference(quant_inst,[status(thm)],[])).
% 0.57/0.76 tff(451,plain,
% 0.57/0.76 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(n1, and2(h1(f))), n1)) | value(in(n1, not1(h1(f))), n1) | (~connection(out(n1, and2(h1(f))), in(n1, not1(h1(f)))))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[450, 449])).
% 0.57/0.76 tff(452,plain,
% 0.57/0.76 ($false),
% 0.57/0.76 inference(unit_resolution,[status(thm)],[451, 27, 445, 434, 384])).
% 0.57/0.76 tff(453,plain,(value(in(n1, not1(h1(f))), n1)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.76 tff(454,plain,
% 0.57/0.76 (^[K: $i] : refl(((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not))) <=> ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not))))),
% 0.57/0.76 inference(bind,[status(th)],[])).
% 0.57/0.76 tff(455,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not))) <=> ![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))),
% 0.57/0.76 inference(quant_intro,[status(thm)],[454])).
% 0.57/0.76 tff(456,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not))) <=> ![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))),
% 0.57/0.76 inference(rewrite,[status(thm)],[])).
% 0.57/0.76 tff(457,plain,
% 0.57/0.76 (^[K: $i] : trans(monotonicity(rewrite((((~mode(K, ok)) | (~type(K, not))) | (~value(in(n1, K), n1))) <=> ((~mode(K, ok)) | (~value(in(n1, K), n1)) | (~type(K, not)))), (((((~mode(K, ok)) | (~type(K, not))) | (~value(in(n1, K), n1))) | value(out(n1, K), n0)) <=> (((~mode(K, ok)) | (~value(in(n1, K), n1)) | (~type(K, not))) | value(out(n1, K), n0)))), rewrite((((~mode(K, ok)) | (~value(in(n1, K), n1)) | (~type(K, not))) | value(out(n1, K), n0)) <=> ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))), (((((~mode(K, ok)) | (~type(K, not))) | (~value(in(n1, K), n1))) | value(out(n1, K), n0)) <=> ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))))),
% 0.57/0.76 inference(bind,[status(th)],[])).
% 0.57/0.76 tff(458,plain,
% 0.57/0.76 (![K: $i] : ((((~mode(K, ok)) | (~type(K, not))) | (~value(in(n1, K), n1))) | value(out(n1, K), n0)) <=> ![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))),
% 0.57/0.76 inference(quant_intro,[status(thm)],[457])).
% 0.57/0.76 tff(459,axiom,(![K: $i] : ((((~mode(K, ok)) | (~type(K, not))) | (~value(in(n1, K), n1))) | value(out(n1, K), n0))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','not_1_0_fw')).
% 0.57/0.76 tff(460,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[459, 458])).
% 0.57/0.76 tff(461,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[460, 456])).
% 0.57/0.76 tff(462,plain,(
% 0.57/0.76 ![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))),
% 0.57/0.76 inference(skolemize,[status(sab)],[461])).
% 0.57/0.76 tff(463,plain,
% 0.57/0.76 (![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))),
% 0.57/0.76 inference(modus_ponens,[status(thm)],[462, 455])).
% 0.57/0.76 tff(464,plain,
% 0.57/0.76 (((~![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))) | ((~mode(not1(h1(f)), ok)) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)) | value(out(n1, not1(h1(f))), n0))) <=> ((~![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))) | (~mode(not1(h1(f)), ok)) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)) | value(out(n1, not1(h1(f))), n0))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(465,plain,
% 0.57/0.77 (((~mode(not1(h1(f)), ok)) | value(out(n1, not1(h1(f))), n0) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not))) <=> ((~mode(not1(h1(f)), ok)) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)) | value(out(n1, not1(h1(f))), n0))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(466,plain,
% 0.57/0.77 (((~![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))) | ((~mode(not1(h1(f)), ok)) | value(out(n1, not1(h1(f))), n0) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)))) <=> ((~![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))) | ((~mode(not1(h1(f)), ok)) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)) | value(out(n1, not1(h1(f))), n0)))),
% 0.57/0.77 inference(monotonicity,[status(thm)],[465])).
% 0.57/0.77 tff(467,plain,
% 0.57/0.77 (((~![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))) | ((~mode(not1(h1(f)), ok)) | value(out(n1, not1(h1(f))), n0) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)))) <=> ((~![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))) | (~mode(not1(h1(f)), ok)) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)) | value(out(n1, not1(h1(f))), n0))),
% 0.57/0.77 inference(transitivity,[status(thm)],[466, 464])).
% 0.57/0.77 tff(468,plain,
% 0.57/0.77 ((~![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))) | ((~mode(not1(h1(f)), ok)) | value(out(n1, not1(h1(f))), n0) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)))),
% 0.57/0.77 inference(quant_inst,[status(thm)],[])).
% 0.57/0.77 tff(469,plain,
% 0.57/0.77 ((~![K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(n1, K), n1)) | (~type(K, not)))) | (~mode(not1(h1(f)), ok)) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)) | value(out(n1, not1(h1(f))), n0)),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[468, 467])).
% 0.57/0.77 tff(470,plain,
% 0.57/0.77 ((~mode(not1(h1(f)), ok)) | (~value(in(n1, not1(h1(f))), n1)) | (~type(not1(h1(f)), not)) | value(out(n1, not1(h1(f))), n0)),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[469, 463])).
% 0.57/0.77 tff(471,plain,
% 0.57/0.77 ((~mode(not1(h1(f)), ok)) | (~value(in(n1, not1(h1(f))), n1)) | value(out(n1, not1(h1(f))), n0)),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[470, 378])).
% 0.57/0.77 tff(472,plain,
% 0.57/0.77 ((~mode(not1(h1(f)), ok)) | value(out(n1, not1(h1(f))), n0)),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[471, 453])).
% 0.57/0.77 tff(473,plain,
% 0.57/0.77 (value(out(n1, not1(h1(f))), n0)),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[472, 383])).
% 0.57/0.77 tff(474,assumption,(~value(in(n2, and1(h1(f))), n0)), introduced(assumption)).
% 0.57/0.77 tff(475,plain,
% 0.57/0.77 (^[X: $i] : refl(((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X)))) <=> ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X)))))),
% 0.57/0.77 inference(bind,[status(th)],[])).
% 0.57/0.77 tff(476,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))),
% 0.57/0.77 inference(quant_intro,[status(thm)],[475])).
% 0.57/0.77 tff(477,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(478,axiom,(![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_connection_out1not1_in2and1')).
% 0.57/0.77 tff(479,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[478, 477])).
% 0.57/0.77 tff(480,plain,(
% 0.57/0.77 ![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))),
% 0.57/0.77 inference(skolemize,[status(sab)],[479])).
% 0.57/0.77 tff(481,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[480, 476])).
% 0.57/0.77 tff(482,plain,
% 0.57/0.77 (((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))) | ((~type(h1(f), halfadder)) | connection(out(n1, not1(h1(f))), in(n2, and1(h1(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))) | (~type(h1(f), halfadder)) | connection(out(n1, not1(h1(f))), in(n2, and1(h1(f)))))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(483,plain,
% 0.57/0.77 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))) | ((~type(h1(f), halfadder)) | connection(out(n1, not1(h1(f))), in(n2, and1(h1(f)))))),
% 0.57/0.77 inference(quant_inst,[status(thm)],[])).
% 0.57/0.77 tff(484,plain,
% 0.57/0.77 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, not1(X)), in(n2, and1(X))))) | (~type(h1(f), halfadder)) | connection(out(n1, not1(h1(f))), in(n2, and1(h1(f))))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[483, 482])).
% 0.57/0.77 tff(485,plain,
% 0.57/0.77 (connection(out(n1, not1(h1(f))), in(n2, and1(h1(f))))),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[484, 481, 91])).
% 0.57/0.77 tff(486,assumption,(value(out(n1, not1(h1(f))), n0)), introduced(assumption)).
% 0.57/0.77 tff(487,plain,
% 0.57/0.77 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(out(n1, not1(h1(f))), n0)) | value(in(n2, and1(h1(f))), n0) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(n1, not1(h1(f))), n0)) | value(in(n2, and1(h1(f))), n0) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f))))))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(488,plain,
% 0.57/0.77 ((value(in(n2, and1(h1(f))), n0) | (~value(out(n1, not1(h1(f))), n0)) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f)))))) <=> ((~value(out(n1, not1(h1(f))), n0)) | value(in(n2, and1(h1(f))), n0) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f))))))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(489,plain,
% 0.57/0.77 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n2, and1(h1(f))), n0) | (~value(out(n1, not1(h1(f))), n0)) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~value(out(n1, not1(h1(f))), n0)) | value(in(n2, and1(h1(f))), n0) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f)))))))),
% 0.57/0.77 inference(monotonicity,[status(thm)],[488])).
% 0.57/0.77 tff(490,plain,
% 0.57/0.77 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n2, and1(h1(f))), n0) | (~value(out(n1, not1(h1(f))), n0)) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(n1, not1(h1(f))), n0)) | value(in(n2, and1(h1(f))), n0) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f))))))),
% 0.57/0.77 inference(transitivity,[status(thm)],[489, 487])).
% 0.57/0.77 tff(491,plain,
% 0.57/0.77 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(in(n2, and1(h1(f))), n0) | (~value(out(n1, not1(h1(f))), n0)) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f))))))),
% 0.57/0.77 inference(quant_inst,[status(thm)],[])).
% 0.57/0.77 tff(492,plain,
% 0.57/0.77 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~value(out(n1, not1(h1(f))), n0)) | value(in(n2, and1(h1(f))), n0) | (~connection(out(n1, not1(h1(f))), in(n2, and1(h1(f)))))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[491, 490])).
% 0.57/0.77 tff(493,plain,
% 0.57/0.77 ($false),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[492, 27, 486, 485, 474])).
% 0.57/0.77 tff(494,plain,(value(in(n2, and1(h1(f))), n0) | (~value(out(n1, not1(h1(f))), n0))), inference(lemma,lemma(discharge,[]))).
% 0.57/0.77 tff(495,plain,
% 0.57/0.77 (value(in(n2, and1(h1(f))), n0)),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[494, 473])).
% 0.57/0.77 tff(496,plain,
% 0.57/0.77 (^[Any: $i, K: $i] : refl(((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and))) <=> ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and))))),
% 0.57/0.77 inference(bind,[status(th)],[])).
% 0.57/0.77 tff(497,plain,
% 0.57/0.77 (![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and))) <=> ![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))),
% 0.57/0.77 inference(quant_intro,[status(thm)],[496])).
% 0.57/0.77 tff(498,plain,
% 0.57/0.77 (![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and))) <=> ![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(499,plain,
% 0.57/0.77 (^[Any: $i, K: $i] : trans(monotonicity(rewrite((((~mode(K, ok)) | (~type(K, and))) | (~value(in(Any, K), n0))) <=> ((~mode(K, ok)) | (~value(in(Any, K), n0)) | (~type(K, and)))), (((((~mode(K, ok)) | (~type(K, and))) | (~value(in(Any, K), n0))) | value(out(n1, K), n0)) <=> (((~mode(K, ok)) | (~value(in(Any, K), n0)) | (~type(K, and))) | value(out(n1, K), n0)))), rewrite((((~mode(K, ok)) | (~value(in(Any, K), n0)) | (~type(K, and))) | value(out(n1, K), n0)) <=> ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))), (((((~mode(K, ok)) | (~type(K, and))) | (~value(in(Any, K), n0))) | value(out(n1, K), n0)) <=> ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))))),
% 0.57/0.77 inference(bind,[status(th)],[])).
% 0.57/0.77 tff(500,plain,
% 0.57/0.77 (![Any: $i, K: $i] : ((((~mode(K, ok)) | (~type(K, and))) | (~value(in(Any, K), n0))) | value(out(n1, K), n0)) <=> ![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))),
% 0.57/0.77 inference(quant_intro,[status(thm)],[499])).
% 0.57/0.77 tff(501,axiom,(![Any: $i, K: $i] : ((((~mode(K, ok)) | (~type(K, and))) | (~value(in(Any, K), n0))) | value(out(n1, K), n0))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','and_0x_0')).
% 0.57/0.77 tff(502,plain,
% 0.57/0.77 (![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[501, 500])).
% 0.57/0.77 tff(503,plain,
% 0.57/0.77 (![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[502, 498])).
% 0.57/0.77 tff(504,plain,(
% 0.57/0.77 ![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))),
% 0.57/0.77 inference(skolemize,[status(sab)],[503])).
% 0.57/0.77 tff(505,plain,
% 0.57/0.77 (![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[504, 497])).
% 0.57/0.77 tff(506,plain,
% 0.57/0.77 (((~![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))) | ((~mode(and1(h1(f)), ok)) | value(out(n1, and1(h1(f))), n0) | (~value(in(n2, and1(h1(f))), n0)) | (~type(and1(h1(f)), and)))) <=> ((~![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))) | (~mode(and1(h1(f)), ok)) | value(out(n1, and1(h1(f))), n0) | (~value(in(n2, and1(h1(f))), n0)) | (~type(and1(h1(f)), and)))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(507,plain,
% 0.57/0.77 ((~![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))) | ((~mode(and1(h1(f)), ok)) | value(out(n1, and1(h1(f))), n0) | (~value(in(n2, and1(h1(f))), n0)) | (~type(and1(h1(f)), and)))),
% 0.57/0.77 inference(quant_inst,[status(thm)],[])).
% 0.57/0.77 tff(508,plain,
% 0.57/0.77 ((~![Any: $i, K: $i] : ((~mode(K, ok)) | value(out(n1, K), n0) | (~value(in(Any, K), n0)) | (~type(K, and)))) | (~mode(and1(h1(f)), ok)) | value(out(n1, and1(h1(f))), n0) | (~value(in(n2, and1(h1(f))), n0)) | (~type(and1(h1(f)), and))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[507, 506])).
% 0.57/0.77 tff(509,plain,
% 0.57/0.77 ((~mode(and1(h1(f)), ok)) | value(out(n1, and1(h1(f))), n0) | (~value(in(n2, and1(h1(f))), n0))),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[508, 505, 358])).
% 0.57/0.77 tff(510,plain,
% 0.57/0.77 (value(out(n1, and1(h1(f))), n0)),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[509, 495, 363])).
% 0.57/0.77 tff(511,plain,
% 0.57/0.77 (^[X: $i] : refl(((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X)))) <=> ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X)))))),
% 0.57/0.77 inference(bind,[status(th)],[])).
% 0.57/0.77 tff(512,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))),
% 0.57/0.77 inference(quant_intro,[status(thm)],[511])).
% 0.57/0.77 tff(513,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(514,axiom,(![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_connection_outs_out1and1')).
% 0.57/0.77 tff(515,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[514, 513])).
% 0.57/0.77 tff(516,plain,(
% 0.57/0.77 ![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))),
% 0.57/0.77 inference(skolemize,[status(sab)],[515])).
% 0.57/0.77 tff(517,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[516, 512])).
% 0.57/0.77 tff(518,plain,
% 0.57/0.77 (((~![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))) | ((~type(h1(f), halfadder)) | connection(out(s, h1(f)), out(n1, and1(h1(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))) | (~type(h1(f), halfadder)) | connection(out(s, h1(f)), out(n1, and1(h1(f)))))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(519,plain,
% 0.57/0.77 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))) | ((~type(h1(f), halfadder)) | connection(out(s, h1(f)), out(n1, and1(h1(f)))))),
% 0.57/0.77 inference(quant_inst,[status(thm)],[])).
% 0.57/0.77 tff(520,plain,
% 0.57/0.77 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))) | (~type(h1(f), halfadder)) | connection(out(s, h1(f)), out(n1, and1(h1(f))))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[519, 518])).
% 0.57/0.77 tff(521,plain,
% 0.57/0.77 (connection(out(s, h1(f)), out(n1, and1(h1(f))))),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[520, 517, 91])).
% 0.57/0.77 tff(522,plain,
% 0.57/0.77 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | ((~value(out(n1, and1(h1(f))), n0)) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | value(out(s, h1(f)), n0))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(out(n1, and1(h1(f))), n0)) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | value(out(s, h1(f)), n0))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(523,plain,
% 0.57/0.77 ((value(out(s, h1(f)), n0) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | (~value(out(n1, and1(h1(f))), n0))) <=> ((~value(out(n1, and1(h1(f))), n0)) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | value(out(s, h1(f)), n0))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(524,plain,
% 0.57/0.77 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(s, h1(f)), n0) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | (~value(out(n1, and1(h1(f))), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | ((~value(out(n1, and1(h1(f))), n0)) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | value(out(s, h1(f)), n0)))),
% 0.57/0.77 inference(monotonicity,[status(thm)],[523])).
% 0.57/0.77 tff(525,plain,
% 0.57/0.77 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(s, h1(f)), n0) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | (~value(out(n1, and1(h1(f))), n0)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(out(n1, and1(h1(f))), n0)) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | value(out(s, h1(f)), n0))),
% 0.57/0.77 inference(transitivity,[status(thm)],[524, 522])).
% 0.57/0.77 tff(526,plain,
% 0.57/0.77 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(s, h1(f)), n0) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | (~value(out(n1, and1(h1(f))), n0)))),
% 0.57/0.77 inference(quant_inst,[status(thm)],[])).
% 0.57/0.77 tff(527,plain,
% 0.57/0.77 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(out(n1, and1(h1(f))), n0)) | (~connection(out(s, h1(f)), out(n1, and1(h1(f))))) | value(out(s, h1(f)), n0)),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[526, 525])).
% 0.57/0.77 tff(528,plain,
% 0.57/0.77 (value(out(s, h1(f)), n0)),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[527, 76, 521, 510])).
% 0.57/0.77 tff(529,plain,
% 0.57/0.77 ((~equal_value(n1, n0)) <=> (~equal_value(n1, n0))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(530,axiom,(~equal_value(n1, n0)), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','equal_value2')).
% 0.57/0.77 tff(531,plain,
% 0.57/0.77 (~equal_value(n1, n0)),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[530, 529])).
% 0.57/0.77 tff(532,plain,
% 0.57/0.77 (((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n1, n0) | (~value(out(s, h1(f)), n1)) | (~value(out(s, h1(f)), n0)))) <=> ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | equal_value(n1, n0) | (~value(out(s, h1(f)), n1)) | (~value(out(s, h1(f)), n0)))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(533,plain,
% 0.57/0.77 ((equal_value(n1, n0) | (~value(out(s, h1(f)), n0)) | (~value(out(s, h1(f)), n1))) <=> (equal_value(n1, n0) | (~value(out(s, h1(f)), n1)) | (~value(out(s, h1(f)), n0)))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(534,plain,
% 0.57/0.77 (((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n1, n0) | (~value(out(s, h1(f)), n0)) | (~value(out(s, h1(f)), n1)))) <=> ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n1, n0) | (~value(out(s, h1(f)), n1)) | (~value(out(s, h1(f)), n0))))),
% 0.57/0.77 inference(monotonicity,[status(thm)],[533])).
% 0.57/0.77 tff(535,plain,
% 0.57/0.77 (((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n1, n0) | (~value(out(s, h1(f)), n0)) | (~value(out(s, h1(f)), n1)))) <=> ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | equal_value(n1, n0) | (~value(out(s, h1(f)), n1)) | (~value(out(s, h1(f)), n0)))),
% 0.57/0.77 inference(transitivity,[status(thm)],[534, 532])).
% 0.57/0.77 tff(536,plain,
% 0.57/0.77 ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n1, n0) | (~value(out(s, h1(f)), n0)) | (~value(out(s, h1(f)), n1)))),
% 0.57/0.77 inference(quant_inst,[status(thm)],[])).
% 0.57/0.77 tff(537,plain,
% 0.57/0.77 ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | equal_value(n1, n0) | (~value(out(s, h1(f)), n1)) | (~value(out(s, h1(f)), n0))),
% 0.57/0.77 inference(modus_ponens,[status(thm)],[536, 535])).
% 0.57/0.77 tff(538,plain,
% 0.57/0.77 (~value(out(s, h1(f)), n1)),
% 0.57/0.77 inference(unit_resolution,[status(thm)],[537, 62, 531, 528])).
% 0.57/0.77 tff(539,plain,
% 0.57/0.77 (^[X: $i] : refl(((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X)))) <=> ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X)))))),
% 0.57/0.77 inference(bind,[status(th)],[])).
% 0.57/0.77 tff(540,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))),
% 0.57/0.77 inference(quant_intro,[status(thm)],[539])).
% 0.57/0.77 tff(541,plain,
% 0.57/0.77 (![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))),
% 0.57/0.77 inference(rewrite,[status(thm)],[])).
% 0.57/0.77 tff(542,axiom,(![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_connection_outsh1_in2h2')).
% 0.57/0.78 tff(543,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[542, 541])).
% 0.57/0.78 tff(544,plain,(
% 0.57/0.78 ![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))),
% 0.57/0.78 inference(skolemize,[status(sab)],[543])).
% 0.57/0.78 tff(545,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[544, 540])).
% 0.57/0.78 tff(546,plain,
% 0.57/0.78 (((~![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))) | ((~type(f, fulladder)) | connection(out(s, h1(f)), in(n2, h2(f))))) <=> ((~![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))) | (~type(f, fulladder)) | connection(out(s, h1(f)), in(n2, h2(f))))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(547,plain,
% 0.57/0.78 ((~![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))) | ((~type(f, fulladder)) | connection(out(s, h1(f)), in(n2, h2(f))))),
% 0.57/0.78 inference(quant_inst,[status(thm)],[])).
% 0.57/0.78 tff(548,plain,
% 0.57/0.78 ((~![X: $i] : ((~type(X, fulladder)) | connection(out(s, h1(X)), in(n2, h2(X))))) | (~type(f, fulladder)) | connection(out(s, h1(f)), in(n2, h2(f)))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[547, 546])).
% 0.57/0.78 tff(549,plain,
% 0.57/0.78 (connection(out(s, h1(f)), in(n2, h2(f)))),
% 0.57/0.78 inference(unit_resolution,[status(thm)],[548, 545, 3])).
% 0.57/0.78 tff(550,plain,
% 0.57/0.78 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | ((~value(in(n2, h2(f)), n1)) | value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f)))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(in(n2, h2(f)), n1)) | value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f)))))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(551,plain,
% 0.57/0.78 ((value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f)))) | (~value(in(n2, h2(f)), n1))) <=> ((~value(in(n2, h2(f)), n1)) | value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f)))))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(552,plain,
% 0.57/0.78 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f)))) | (~value(in(n2, h2(f)), n1)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | ((~value(in(n2, h2(f)), n1)) | value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f))))))),
% 0.57/0.78 inference(monotonicity,[status(thm)],[551])).
% 0.57/0.78 tff(553,plain,
% 0.57/0.78 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f)))) | (~value(in(n2, h2(f)), n1)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(in(n2, h2(f)), n1)) | value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f)))))),
% 0.57/0.78 inference(transitivity,[status(thm)],[552, 550])).
% 0.57/0.78 tff(554,plain,
% 0.57/0.78 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f)))) | (~value(in(n2, h2(f)), n1)))),
% 0.57/0.78 inference(quant_inst,[status(thm)],[])).
% 0.57/0.78 tff(555,plain,
% 0.57/0.78 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(in(n2, h2(f)), n1)) | value(out(s, h1(f)), n1) | (~connection(out(s, h1(f)), in(n2, h2(f))))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[554, 553])).
% 0.57/0.78 tff(556,plain,
% 0.57/0.78 (~value(in(n2, h2(f)), n1)),
% 0.57/0.78 inference(unit_resolution,[status(thm)],[555, 76, 549, 538])).
% 0.57/0.78 tff(557,plain,
% 0.57/0.78 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h2(f)), n1) | (~value(in(n2, or1(h2(f))), n1)) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n2, h2(f)), n1) | (~value(in(n2, or1(h2(f))), n1)) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f))))))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(558,plain,
% 0.57/0.78 ((value(in(n2, h2(f)), n1) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f))))) | (~value(in(n2, or1(h2(f))), n1))) <=> (value(in(n2, h2(f)), n1) | (~value(in(n2, or1(h2(f))), n1)) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f))))))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(559,plain,
% 0.57/0.78 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h2(f)), n1) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f))))) | (~value(in(n2, or1(h2(f))), n1)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h2(f)), n1) | (~value(in(n2, or1(h2(f))), n1)) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f)))))))),
% 0.57/0.78 inference(monotonicity,[status(thm)],[558])).
% 0.57/0.78 tff(560,plain,
% 0.57/0.78 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h2(f)), n1) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f))))) | (~value(in(n2, or1(h2(f))), n1)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n2, h2(f)), n1) | (~value(in(n2, or1(h2(f))), n1)) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f))))))),
% 0.57/0.78 inference(transitivity,[status(thm)],[559, 557])).
% 0.57/0.78 tff(561,plain,
% 0.57/0.78 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n2, h2(f)), n1) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f))))) | (~value(in(n2, or1(h2(f))), n1)))),
% 0.57/0.78 inference(quant_inst,[status(thm)],[])).
% 0.57/0.78 tff(562,plain,
% 0.57/0.78 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n2, h2(f)), n1) | (~value(in(n2, or1(h2(f))), n1)) | (~connection(in(n2, h2(f)), in(n2, or1(h2(f)))))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[561, 560])).
% 0.57/0.78 tff(563,plain,
% 0.57/0.78 (~value(in(n2, or1(h2(f))), n1)),
% 0.57/0.78 inference(unit_resolution,[status(thm)],[562, 76, 556, 350])).
% 0.57/0.78 tff(564,plain,
% 0.57/0.78 (^[X: $i] : refl(((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X)))) <=> ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X)))))),
% 0.57/0.78 inference(bind,[status(th)],[])).
% 0.57/0.78 tff(565,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))),
% 0.57/0.78 inference(quant_intro,[status(thm)],[564])).
% 0.57/0.78 tff(566,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(567,axiom,(![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_connection_in1_in1or1')).
% 0.57/0.78 tff(568,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[567, 566])).
% 0.57/0.78 tff(569,plain,(
% 0.57/0.78 ![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))),
% 0.57/0.78 inference(skolemize,[status(sab)],[568])).
% 0.57/0.78 tff(570,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[569, 565])).
% 0.57/0.78 tff(571,plain,
% 0.57/0.78 (((~![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))) | ((~type(h2(f), halfadder)) | connection(in(n1, h2(f)), in(n1, or1(h2(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))) | (~type(h2(f), halfadder)) | connection(in(n1, h2(f)), in(n1, or1(h2(f)))))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(572,plain,
% 0.57/0.78 ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))) | ((~type(h2(f), halfadder)) | connection(in(n1, h2(f)), in(n1, or1(h2(f)))))),
% 0.57/0.78 inference(quant_inst,[status(thm)],[])).
% 0.57/0.78 tff(573,plain,
% 0.57/0.78 ((~![X: $i] : ((~type(X, halfadder)) | connection(in(n1, X), in(n1, or1(X))))) | (~type(h2(f), halfadder)) | connection(in(n1, h2(f)), in(n1, or1(h2(f))))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[572, 571])).
% 0.57/0.78 tff(574,plain,
% 0.57/0.78 (connection(in(n1, h2(f)), in(n1, or1(h2(f))))),
% 0.57/0.78 inference(unit_resolution,[status(thm)],[573, 570, 303])).
% 0.57/0.78 tff(575,plain,
% 0.57/0.78 (^[X: $i] : refl(((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X)))) <=> ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X)))))),
% 0.57/0.78 inference(bind,[status(th)],[])).
% 0.57/0.78 tff(576,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))),
% 0.57/0.78 inference(quant_intro,[status(thm)],[575])).
% 0.57/0.78 tff(577,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X)))) <=> ![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(578,axiom,(![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax','fulladder_connection_in1_in1h2')).
% 0.57/0.78 tff(579,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[578, 577])).
% 0.57/0.78 tff(580,plain,(
% 0.57/0.78 ![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))),
% 0.57/0.78 inference(skolemize,[status(sab)],[579])).
% 0.57/0.78 tff(581,plain,
% 0.57/0.78 (![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[580, 576])).
% 0.57/0.78 tff(582,plain,
% 0.57/0.78 (((~![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))) | ((~type(f, fulladder)) | connection(in(n1, f), in(n1, h2(f))))) <=> ((~![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))) | (~type(f, fulladder)) | connection(in(n1, f), in(n1, h2(f))))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(583,plain,
% 0.57/0.78 ((~![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))) | ((~type(f, fulladder)) | connection(in(n1, f), in(n1, h2(f))))),
% 0.57/0.78 inference(quant_inst,[status(thm)],[])).
% 0.57/0.78 tff(584,plain,
% 0.57/0.78 ((~![X: $i] : ((~type(X, fulladder)) | connection(in(n1, X), in(n1, h2(X))))) | (~type(f, fulladder)) | connection(in(n1, f), in(n1, h2(f)))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[583, 582])).
% 0.57/0.78 tff(585,plain,
% 0.57/0.78 (connection(in(n1, f), in(n1, h2(f)))),
% 0.57/0.78 inference(unit_resolution,[status(thm)],[584, 581, 3])).
% 0.57/0.78 tff(586,plain,
% 0.57/0.78 (value(in(n1, f), n0) <=> value(in(n1, f), n0)),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(587,axiom,(value(in(n1, f), n0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','in1_1')).
% 0.57/0.78 tff(588,plain,
% 0.57/0.78 (value(in(n1, f), n0)),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[587, 586])).
% 0.57/0.78 tff(589,plain,
% 0.57/0.78 (((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n1, n0) | (~value(in(n1, f), n0)) | (~value(in(n1, f), n1)))) <=> ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | equal_value(n1, n0) | (~value(in(n1, f), n0)) | (~value(in(n1, f), n1)))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(590,plain,
% 0.57/0.78 ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | (equal_value(n1, n0) | (~value(in(n1, f), n0)) | (~value(in(n1, f), n1)))),
% 0.57/0.78 inference(quant_inst,[status(thm)],[])).
% 0.57/0.78 tff(591,plain,
% 0.57/0.78 ((~![P: $i, V1: $i, V2: $i] : (equal_value(V1, V2) | (~value(P, V2)) | (~value(P, V1)))) | equal_value(n1, n0) | (~value(in(n1, f), n0)) | (~value(in(n1, f), n1))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[590, 589])).
% 0.57/0.78 tff(592,plain,
% 0.57/0.78 (~value(in(n1, f), n1)),
% 0.57/0.78 inference(unit_resolution,[status(thm)],[591, 62, 531, 588])).
% 0.57/0.78 tff(593,plain,
% 0.57/0.78 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n1, f), n1) | (~connection(in(n1, f), in(n1, h2(f)))) | (~value(in(n1, h2(f)), n1)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n1, f), n1) | (~connection(in(n1, f), in(n1, h2(f)))) | (~value(in(n1, h2(f)), n1)))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(594,plain,
% 0.57/0.78 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n1, f), n1) | (~connection(in(n1, f), in(n1, h2(f)))) | (~value(in(n1, h2(f)), n1)))),
% 0.57/0.78 inference(quant_inst,[status(thm)],[])).
% 0.57/0.78 tff(595,plain,
% 0.57/0.78 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n1, f), n1) | (~connection(in(n1, f), in(n1, h2(f)))) | (~value(in(n1, h2(f)), n1))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[594, 593])).
% 0.57/0.78 tff(596,plain,
% 0.57/0.78 (~value(in(n1, h2(f)), n1)),
% 0.57/0.78 inference(unit_resolution,[status(thm)],[595, 76, 592, 585])).
% 0.57/0.78 tff(597,plain,
% 0.57/0.78 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n1, h2(f)), n1) | (~connection(in(n1, h2(f)), in(n1, or1(h2(f))))) | (~value(in(n1, or1(h2(f))), n1)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n1, h2(f)), n1) | (~connection(in(n1, h2(f)), in(n1, or1(h2(f))))) | (~value(in(n1, or1(h2(f))), n1)))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(598,plain,
% 0.57/0.78 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(in(n1, h2(f)), n1) | (~connection(in(n1, h2(f)), in(n1, or1(h2(f))))) | (~value(in(n1, or1(h2(f))), n1)))),
% 0.57/0.78 inference(quant_inst,[status(thm)],[])).
% 0.57/0.78 tff(599,plain,
% 0.57/0.78 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | value(in(n1, h2(f)), n1) | (~connection(in(n1, h2(f)), in(n1, or1(h2(f))))) | (~value(in(n1, or1(h2(f))), n1))),
% 0.57/0.78 inference(modus_ponens,[status(thm)],[598, 597])).
% 0.57/0.78 tff(600,plain,
% 0.57/0.78 (~value(in(n1, or1(h2(f))), n1)),
% 0.57/0.78 inference(unit_resolution,[status(thm)],[599, 76, 596, 574])).
% 0.57/0.78 tff(601,plain,
% 0.57/0.78 (^[K: $i] : refl(((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or))) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or))))),
% 0.57/0.78 inference(bind,[status(th)],[])).
% 0.57/0.78 tff(602,plain,
% 0.57/0.78 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or))) <=> ![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))),
% 0.57/0.78 inference(quant_intro,[status(thm)],[601])).
% 0.57/0.78 tff(603,plain,
% 0.57/0.78 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or))) <=> ![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))),
% 0.57/0.78 inference(rewrite,[status(thm)],[])).
% 0.57/0.78 tff(604,plain,
% 0.57/0.78 (^[K: $i] : trans(monotonicity(trans(monotonicity(rewrite((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n1))) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, or)))), (((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1)) <=> (((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, or))) | value(in(n1, K), n1)))), rewrite((((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, or))) | value(in(n1, K), n1)) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n1, K), n1) | (~type(K, or)))), (((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1)) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n1, K), n1) | (~type(K, or))))), ((((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1)) | value(in(n2, K), n1)) <=> (((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n1, K), n1) | (~type(K, or))) | value(in(n2, K), n1)))), rewrite((((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n1, K), n1) | (~type(K, or))) | value(in(n2, K), n1)) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))), ((((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1)) | value(in(n2, K), n1)) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))))),
% 0.63/0.79 inference(bind,[status(th)],[])).
% 0.63/0.79 tff(605,plain,
% 0.63/0.79 (![K: $i] : (((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1)) | value(in(n2, K), n1)) <=> ![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))),
% 0.63/0.79 inference(quant_intro,[status(thm)],[604])).
% 0.63/0.79 tff(606,axiom,(![K: $i] : (((((~mode(K, ok)) | (~type(K, or))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1)) | value(in(n2, K), n1))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','or_1_11')).
% 0.63/0.79 tff(607,plain,
% 0.63/0.79 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[606, 605])).
% 0.63/0.79 tff(608,plain,
% 0.63/0.79 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[607, 603])).
% 0.63/0.79 tff(609,plain,(
% 0.63/0.79 ![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))),
% 0.63/0.79 inference(skolemize,[status(sab)],[608])).
% 0.63/0.79 tff(610,plain,
% 0.63/0.79 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[609, 602])).
% 0.63/0.79 tff(611,plain,
% 0.63/0.79 (((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))) | (value(in(n1, or1(h2(f))), n1) | (~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | (~type(or1(h2(f)), or)) | value(in(n2, or1(h2(f))), n1))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))) | value(in(n1, or1(h2(f))), n1) | (~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | (~type(or1(h2(f)), or)) | value(in(n2, or1(h2(f))), n1))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(612,plain,
% 0.63/0.79 (((~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | value(in(n2, or1(h2(f))), n1) | value(in(n1, or1(h2(f))), n1) | (~type(or1(h2(f)), or))) <=> (value(in(n1, or1(h2(f))), n1) | (~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | (~type(or1(h2(f)), or)) | value(in(n2, or1(h2(f))), n1))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(613,plain,
% 0.63/0.79 (((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))) | ((~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | value(in(n2, or1(h2(f))), n1) | value(in(n1, or1(h2(f))), n1) | (~type(or1(h2(f)), or)))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))) | (value(in(n1, or1(h2(f))), n1) | (~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | (~type(or1(h2(f)), or)) | value(in(n2, or1(h2(f))), n1)))),
% 0.63/0.79 inference(monotonicity,[status(thm)],[612])).
% 0.63/0.79 tff(614,plain,
% 0.63/0.79 (((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))) | ((~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | value(in(n2, or1(h2(f))), n1) | value(in(n1, or1(h2(f))), n1) | (~type(or1(h2(f)), or)))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))) | value(in(n1, or1(h2(f))), n1) | (~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | (~type(or1(h2(f)), or)) | value(in(n2, or1(h2(f))), n1))),
% 0.63/0.79 inference(transitivity,[status(thm)],[613, 611])).
% 0.63/0.79 tff(615,plain,
% 0.63/0.79 ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))) | ((~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | value(in(n2, or1(h2(f))), n1) | value(in(n1, or1(h2(f))), n1) | (~type(or1(h2(f)), or)))),
% 0.63/0.79 inference(quant_inst,[status(thm)],[])).
% 0.63/0.79 tff(616,plain,
% 0.63/0.79 ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | value(in(n2, K), n1) | value(in(n1, K), n1) | (~type(K, or)))) | value(in(n1, or1(h2(f))), n1) | (~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | (~type(or1(h2(f)), or)) | value(in(n2, or1(h2(f))), n1)),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[615, 614])).
% 0.63/0.79 tff(617,plain,
% 0.63/0.79 ((~mode(or1(h2(f)), ok)) | (~value(out(n1, or1(h2(f))), n1)) | value(in(n2, or1(h2(f))), n1)),
% 0.63/0.79 inference(unit_resolution,[status(thm)],[616, 610, 334, 600])).
% 0.63/0.79 tff(618,plain,
% 0.63/0.79 (~value(out(n1, or1(h2(f))), n1)),
% 0.63/0.79 inference(unit_resolution,[status(thm)],[617, 563, 339])).
% 0.63/0.79 tff(619,plain,
% 0.63/0.79 (^[X: $i] : refl(((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X)))) <=> ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X)))))),
% 0.63/0.79 inference(bind,[status(th)],[])).
% 0.63/0.79 tff(620,plain,
% 0.63/0.79 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))),
% 0.63/0.79 inference(quant_intro,[status(thm)],[619])).
% 0.63/0.79 tff(621,plain,
% 0.63/0.79 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X)))) <=> ![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(622,axiom,(![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax','halfadder_connection_out1or1_in1_and1')).
% 0.63/0.79 tff(623,plain,
% 0.63/0.79 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[622, 621])).
% 0.63/0.79 tff(624,plain,(
% 0.63/0.79 ![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))),
% 0.63/0.79 inference(skolemize,[status(sab)],[623])).
% 0.63/0.79 tff(625,plain,
% 0.63/0.79 (![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[624, 620])).
% 0.63/0.79 tff(626,plain,
% 0.63/0.79 (((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))) | ((~type(h2(f), halfadder)) | connection(out(n1, or1(h2(f))), in(n1, and1(h2(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))) | (~type(h2(f), halfadder)) | connection(out(n1, or1(h2(f))), in(n1, and1(h2(f)))))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(627,plain,
% 0.63/0.79 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))) | ((~type(h2(f), halfadder)) | connection(out(n1, or1(h2(f))), in(n1, and1(h2(f)))))),
% 0.63/0.79 inference(quant_inst,[status(thm)],[])).
% 0.63/0.79 tff(628,plain,
% 0.63/0.79 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(n1, or1(X)), in(n1, and1(X))))) | (~type(h2(f), halfadder)) | connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[627, 626])).
% 0.63/0.79 tff(629,plain,
% 0.63/0.79 (connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))),
% 0.63/0.79 inference(unit_resolution,[status(thm)],[628, 625, 303])).
% 0.63/0.79 tff(630,plain,
% 0.63/0.79 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | ((~value(in(n1, and1(h2(f))), n1)) | value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(in(n1, and1(h2(f))), n1)) | value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(631,plain,
% 0.63/0.79 ((value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))) | (~value(in(n1, and1(h2(f))), n1))) <=> ((~value(in(n1, and1(h2(f))), n1)) | value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(632,plain,
% 0.63/0.79 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))) | (~value(in(n1, and1(h2(f))), n1)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | ((~value(in(n1, and1(h2(f))), n1)) | value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f)))))))),
% 0.63/0.79 inference(monotonicity,[status(thm)],[631])).
% 0.63/0.79 tff(633,plain,
% 0.63/0.79 (((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))) | (~value(in(n1, and1(h2(f))), n1)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(in(n1, and1(h2(f))), n1)) | value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))))),
% 0.63/0.79 inference(transitivity,[status(thm)],[632, 630])).
% 0.63/0.79 tff(634,plain,
% 0.63/0.79 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f))))) | (~value(in(n1, and1(h2(f))), n1)))),
% 0.63/0.79 inference(quant_inst,[status(thm)],[])).
% 0.63/0.79 tff(635,plain,
% 0.63/0.79 ((~![V: $i, P2: $i, P1: $i] : (value(P1, V) | (~connection(P1, P2)) | (~value(P2, V)))) | (~value(in(n1, and1(h2(f))), n1)) | value(out(n1, or1(h2(f))), n1) | (~connection(out(n1, or1(h2(f))), in(n1, and1(h2(f)))))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[634, 633])).
% 0.63/0.79 tff(636,plain,
% 0.63/0.79 (~value(in(n1, and1(h2(f))), n1)),
% 0.63/0.79 inference(unit_resolution,[status(thm)],[635, 76, 629, 618])).
% 0.63/0.79 tff(637,plain,
% 0.63/0.79 (^[K: $i] : refl(((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1)) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1)))),
% 0.63/0.79 inference(bind,[status(th)],[])).
% 0.63/0.79 tff(638,plain,
% 0.63/0.79 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1)) <=> ![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))),
% 0.63/0.79 inference(quant_intro,[status(thm)],[637])).
% 0.63/0.79 tff(639,plain,
% 0.63/0.79 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1)) <=> ![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(640,plain,
% 0.63/0.79 (^[K: $i] : trans(monotonicity(rewrite((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n1))) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)))), (((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1)) <=> (((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and))) | value(in(n1, K), n1)))), rewrite((((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and))) | value(in(n1, K), n1)) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))), (((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1)) <=> ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))))),
% 0.63/0.79 inference(bind,[status(th)],[])).
% 0.63/0.79 tff(641,plain,
% 0.63/0.79 (![K: $i] : ((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1)) <=> ![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))),
% 0.63/0.79 inference(quant_intro,[status(thm)],[640])).
% 0.63/0.79 tff(642,axiom,(![K: $i] : ((((~mode(K, ok)) | (~type(K, and))) | (~value(out(n1, K), n1))) | value(in(n1, K), n1))), file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax','and_1_1x')).
% 0.63/0.79 tff(643,plain,
% 0.63/0.79 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[642, 641])).
% 0.63/0.79 tff(644,plain,
% 0.63/0.79 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[643, 639])).
% 0.63/0.79 tff(645,plain,(
% 0.63/0.79 ![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))),
% 0.63/0.79 inference(skolemize,[status(sab)],[644])).
% 0.63/0.79 tff(646,plain,
% 0.63/0.79 (![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[645, 638])).
% 0.63/0.79 tff(647,plain,
% 0.63/0.79 (((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))) | ((~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | value(in(n1, and1(h2(f))), n1) | (~type(and1(h2(f)), and)))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))) | (~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | value(in(n1, and1(h2(f))), n1) | (~type(and1(h2(f)), and)))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(648,plain,
% 0.63/0.79 (((~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | (~type(and1(h2(f)), and)) | value(in(n1, and1(h2(f))), n1)) <=> ((~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | value(in(n1, and1(h2(f))), n1) | (~type(and1(h2(f)), and)))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(649,plain,
% 0.63/0.79 (((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))) | ((~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | (~type(and1(h2(f)), and)) | value(in(n1, and1(h2(f))), n1))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))) | ((~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | value(in(n1, and1(h2(f))), n1) | (~type(and1(h2(f)), and))))),
% 0.63/0.79 inference(monotonicity,[status(thm)],[648])).
% 0.63/0.79 tff(650,plain,
% 0.63/0.79 (((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))) | ((~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | (~type(and1(h2(f)), and)) | value(in(n1, and1(h2(f))), n1))) <=> ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))) | (~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | value(in(n1, and1(h2(f))), n1) | (~type(and1(h2(f)), and)))),
% 0.63/0.79 inference(transitivity,[status(thm)],[649, 647])).
% 0.63/0.79 tff(651,plain,
% 0.63/0.79 ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))) | ((~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | (~type(and1(h2(f)), and)) | value(in(n1, and1(h2(f))), n1))),
% 0.63/0.79 inference(quant_inst,[status(thm)],[])).
% 0.63/0.79 tff(652,plain,
% 0.63/0.79 ((~![K: $i] : ((~mode(K, ok)) | (~value(out(n1, K), n1)) | (~type(K, and)) | value(in(n1, K), n1))) | (~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | value(in(n1, and1(h2(f))), n1) | (~type(and1(h2(f)), and))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[651, 650])).
% 0.63/0.79 tff(653,plain,
% 0.63/0.79 ((~mode(and1(h2(f)), ok)) | (~value(out(n1, and1(h2(f))), n1)) | value(in(n1, and1(h2(f))), n1)),
% 0.63/0.79 inference(unit_resolution,[status(thm)],[652, 646, 314])).
% 0.63/0.79 tff(654,plain,
% 0.63/0.79 (~value(out(n1, and1(h2(f))), n1)),
% 0.63/0.79 inference(unit_resolution,[status(thm)],[653, 636, 319])).
% 0.63/0.79 tff(655,plain,
% 0.63/0.79 (((~![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))) | ((~type(h2(f), halfadder)) | connection(out(s, h2(f)), out(n1, and1(h2(f)))))) <=> ((~![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))) | (~type(h2(f), halfadder)) | connection(out(s, h2(f)), out(n1, and1(h2(f)))))),
% 0.63/0.79 inference(rewrite,[status(thm)],[])).
% 0.63/0.79 tff(656,plain,
% 0.63/0.79 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))) | ((~type(h2(f), halfadder)) | connection(out(s, h2(f)), out(n1, and1(h2(f)))))),
% 0.63/0.79 inference(quant_inst,[status(thm)],[])).
% 0.63/0.79 tff(657,plain,
% 0.63/0.79 ((~![X: $i] : ((~type(X, halfadder)) | connection(out(s, X), out(n1, and1(X))))) | (~type(h2(f), halfadder)) | connection(out(s, h2(f)), out(n1, and1(h2(f))))),
% 0.63/0.79 inference(modus_ponens,[status(thm)],[656, 655])).
% 0.63/0.79 tff(658,plain,
% 0.63/0.79 (connection(out(s, h2(f)), out(n1, and1(h2(f))))),
% 0.63/0.79 inference(unit_resolution,[status(thm)],[657, 517, 303])).
% 0.63/0.79 tff(659,plain,
% 0.63/0.79 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~connection(out(s, h2(f)), out(n1, and1(h2(f))))) | value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1)))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~connection(out(s, h2(f)), out(n1, and1(h2(f))))) | value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1)))),
% 0.63/0.80 inference(rewrite,[status(thm)],[])).
% 0.63/0.80 tff(660,plain,
% 0.63/0.80 ((value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1)) | (~connection(out(s, h2(f)), out(n1, and1(h2(f)))))) <=> ((~connection(out(s, h2(f)), out(n1, and1(h2(f))))) | value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1)))),
% 0.63/0.80 inference(rewrite,[status(thm)],[])).
% 0.63/0.80 tff(661,plain,
% 0.63/0.80 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1)) | (~connection(out(s, h2(f)), out(n1, and1(h2(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | ((~connection(out(s, h2(f)), out(n1, and1(h2(f))))) | value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1))))),
% 0.63/0.80 inference(monotonicity,[status(thm)],[660])).
% 0.63/0.80 tff(662,plain,
% 0.63/0.80 (((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1)) | (~connection(out(s, h2(f)), out(n1, and1(h2(f))))))) <=> ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~connection(out(s, h2(f)), out(n1, and1(h2(f))))) | value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1)))),
% 0.63/0.80 inference(transitivity,[status(thm)],[661, 659])).
% 0.63/0.80 tff(663,plain,
% 0.63/0.80 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1)) | (~connection(out(s, h2(f)), out(n1, and1(h2(f))))))),
% 0.63/0.80 inference(quant_inst,[status(thm)],[])).
% 0.63/0.80 tff(664,plain,
% 0.63/0.80 ((~![V: $i, P2: $i, P1: $i] : (value(P2, V) | (~value(P1, V)) | (~connection(P1, P2)))) | (~connection(out(s, h2(f)), out(n1, and1(h2(f))))) | value(out(n1, and1(h2(f))), n1) | (~value(out(s, h2(f)), n1))),
% 0.63/0.80 inference(modus_ponens,[status(thm)],[663, 662])).
% 0.63/0.80 tff(665,plain,
% 0.63/0.80 ($false),
% 0.63/0.80 inference(unit_resolution,[status(thm)],[664, 27, 658, 654, 34])).
% 0.63/0.80 % SZS output end Proof
% 0.63/0.80 % E exiting
%------------------------------------------------------------------------------