%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS138+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n005.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:13:28 AM UTC 2025
% Result : Theorem 0.12s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : KRS138+1 : TPTP v9.0.0. Released v3.1.0.
% 0.04/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n005.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 19:11:35 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.37 % SZS status Theorem
% 0.12/0.37 % SZS output start Proof
% 0.12/0.37 tff(xsd_string_type, type, (
% 0.12/0.37 xsd_string: $i > $o)).
% 0.12/0.37 tff(tptp_fun_X_1_type, type, (
% 0.12/0.37 tptp_fun_X_1: $i)).
% 0.12/0.37 tff(xsd_integer_type, type, (
% 0.12/0.37 xsd_integer: $i > $o)).
% 0.12/0.37 tff(cowlNothing_type, type, (
% 0.12/0.37 cowlNothing: $i > $o)).
% 0.12/0.37 tff(tptp_fun_X_0_type, type, (
% 0.12/0.37 tptp_fun_X_0: $i)).
% 0.12/0.37 tff(cowlThing_type, type, (
% 0.12/0.37 cowlThing: $i > $o)).
% 0.12/0.37 tff(requalityOnA_type, type, (
% 0.12/0.37 requalityOnA: ( $i * $i ) > $o)).
% 0.12/0.37 tff(tptp_fun_X_5_type, type, (
% 0.12/0.37 tptp_fun_X_5: $i)).
% 0.12/0.37 tff(tptp_fun_Y_4_type, type, (
% 0.12/0.37 tptp_fun_Y_4: $i)).
% 0.12/0.37 tff(ia_type, type, (
% 0.12/0.37 ia: $i)).
% 0.12/0.37 tff(ib_type, type, (
% 0.12/0.37 ib: $i)).
% 0.12/0.37 tff(cA_type, type, (
% 0.12/0.37 cA: $i > $o)).
% 0.12/0.37 tff(tptp_fun_Y_2_type, type, (
% 0.12/0.37 tptp_fun_Y_2: $i)).
% 0.12/0.37 tff(tptp_fun_X_3_type, type, (
% 0.12/0.37 tptp_fun_X_3: $i)).
% 0.12/0.37 tff(ic_type, type, (
% 0.12/0.37 ic: $i)).
% 0.12/0.37 tff(1,assumption,(xsd_integer(X!1) <=> xsd_string(X!1)), introduced(assumption)).
% 0.12/0.37 tff(2,plain,
% 0.12/0.37 (^[X: $i] : refl((~(xsd_integer(X) <=> xsd_string(X))) <=> (~(xsd_integer(X) <=> xsd_string(X))))),
% 0.12/0.37 inference(bind,[status(th)],[])).
% 0.12/0.37 tff(3,plain,
% 0.12/0.37 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) <=> ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.12/0.37 inference(quant_intro,[status(thm)],[2])).
% 0.12/0.37 tff(4,plain,
% 0.12/0.37 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) <=> ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(5,plain,
% 0.12/0.37 (^[X: $i] : trans(rewrite((xsd_string(X) <=> (~xsd_integer(X))) <=> (~(xsd_integer(X) <=> xsd_string(X)))), rewrite((~(xsd_integer(X) <=> xsd_string(X))) <=> (~(xsd_integer(X) <=> xsd_string(X)))), ((xsd_string(X) <=> (~xsd_integer(X))) <=> (~(xsd_integer(X) <=> xsd_string(X)))))),
% 0.12/0.37 inference(bind,[status(th)],[])).
% 0.12/0.37 tff(6,plain,
% 0.12/0.37 (![X: $i] : (xsd_string(X) <=> (~xsd_integer(X))) <=> ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.12/0.37 inference(quant_intro,[status(thm)],[5])).
% 0.12/0.37 tff(7,axiom,(![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_1')).
% 0.12/0.37 tff(8,plain,
% 0.12/0.37 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[7, 6])).
% 0.12/0.37 tff(9,plain,
% 0.12/0.37 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[8, 4])).
% 0.12/0.37 tff(10,plain,(
% 0.12/0.37 ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.12/0.37 inference(skolemize,[status(sab)],[9])).
% 0.12/0.37 tff(11,plain,
% 0.12/0.37 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[10, 3])).
% 0.12/0.37 tff(12,plain,
% 0.12/0.37 ((~![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))) | (~(xsd_integer(X!1) <=> xsd_string(X!1)))),
% 0.12/0.37 inference(quant_inst,[status(thm)],[])).
% 0.12/0.37 tff(13,plain,
% 0.12/0.37 ($false),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[12, 11, 1])).
% 0.12/0.37 tff(14,plain,(~(xsd_integer(X!1) <=> xsd_string(X!1))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.37 tff(15,assumption,(cowlNothing(X!0) | (~cowlThing(X!0))), introduced(assumption)).
% 0.12/0.37 tff(16,plain,
% 0.12/0.37 (^[X: $i] : refl((~(cowlNothing(X) | (~cowlThing(X)))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.12/0.37 inference(bind,[status(th)],[])).
% 0.12/0.37 tff(17,plain,
% 0.12/0.37 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X)))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.12/0.37 inference(quant_intro,[status(thm)],[16])).
% 0.12/0.37 tff(18,plain,
% 0.12/0.37 (^[X: $i] : rewrite((cowlThing(X) & (~cowlNothing(X))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.12/0.37 inference(bind,[status(th)],[])).
% 0.12/0.37 tff(19,plain,
% 0.12/0.37 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.12/0.37 inference(quant_intro,[status(thm)],[18])).
% 0.12/0.37 tff(20,plain,
% 0.12/0.37 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(21,axiom,(![X: $i] : (cowlThing(X) & (~cowlNothing(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_0')).
% 0.12/0.37 tff(22,plain,
% 0.12/0.37 (![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.12/0.37 tff(23,plain,(
% 0.12/0.37 ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.12/0.37 inference(skolemize,[status(sab)],[22])).
% 0.12/0.37 tff(24,plain,
% 0.19/0.37 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[23, 19])).
% 0.19/0.37 tff(25,plain,
% 0.19/0.37 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[24, 17])).
% 0.19/0.37 tff(26,plain,
% 0.19/0.37 ((~![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))) | (~(cowlNothing(X!0) | (~cowlThing(X!0))))),
% 0.19/0.37 inference(quant_inst,[status(thm)],[])).
% 0.19/0.37 tff(27,plain,
% 0.19/0.37 ($false),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[26, 25, 15])).
% 0.19/0.37 tff(28,plain,(~(cowlNothing(X!0) | (~cowlThing(X!0)))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.37 tff(29,plain,
% 0.19/0.37 ((cowlNothing(X!0) | (~cowlThing(X!0))) | (~cowlNothing(X!0))),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(30,plain,
% 0.19/0.37 (~cowlNothing(X!0)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[29, 28])).
% 0.19/0.37 tff(31,plain,
% 0.19/0.37 ((cowlNothing(X!0) | (~cowlThing(X!0))) | cowlThing(X!0)),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(32,plain,
% 0.19/0.37 (cowlThing(X!0)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[31, 28])).
% 0.19/0.37 tff(33,plain,
% 0.19/0.37 (^[X: $i] : refl((cA(X) <=> ((X = ia) | (X = ib))) <=> (cA(X) <=> ((X = ia) | (X = ib))))),
% 0.19/0.37 inference(bind,[status(th)],[])).
% 0.19/0.37 tff(34,plain,
% 0.19/0.37 (![X: $i] : (cA(X) <=> ((X = ia) | (X = ib))) <=> ![X: $i] : (cA(X) <=> ((X = ia) | (X = ib)))),
% 0.19/0.37 inference(quant_intro,[status(thm)],[33])).
% 0.19/0.37 tff(35,plain,
% 0.19/0.37 (![X: $i] : (cA(X) <=> ((X = ia) | (X = ib))) <=> ![X: $i] : (cA(X) <=> ((X = ia) | (X = ib)))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(36,plain,
% 0.19/0.37 (^[X: $i] : rewrite((cA(X) <=> ((X = ib) | (X = ia))) <=> (cA(X) <=> ((X = ia) | (X = ib))))),
% 0.19/0.37 inference(bind,[status(th)],[])).
% 0.19/0.37 tff(37,plain,
% 0.19/0.37 (![X: $i] : (cA(X) <=> ((X = ib) | (X = ia))) <=> ![X: $i] : (cA(X) <=> ((X = ia) | (X = ib)))),
% 0.19/0.37 inference(quant_intro,[status(thm)],[36])).
% 0.19/0.37 tff(38,axiom,(![X: $i] : (cA(X) <=> ((X = ib) | (X = ia)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_2')).
% 0.19/0.37 tff(39,plain,
% 0.19/0.37 (![X: $i] : (cA(X) <=> ((X = ia) | (X = ib)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[38, 37])).
% 0.19/0.37 tff(40,plain,
% 0.19/0.37 (![X: $i] : (cA(X) <=> ((X = ia) | (X = ib)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[39, 35])).
% 0.19/0.37 tff(41,plain,(
% 0.19/0.37 ![X: $i] : (cA(X) <=> ((X = ia) | (X = ib)))),
% 0.19/0.37 inference(skolemize,[status(sab)],[40])).
% 0.19/0.37 tff(42,plain,
% 0.19/0.37 (![X: $i] : (cA(X) <=> ((X = ia) | (X = ib)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[41, 34])).
% 0.19/0.37 tff(43,plain,
% 0.19/0.37 ((~![X: $i] : (cA(X) <=> ((X = ia) | (X = ib)))) | (cA(Y!4) <=> ((Y!4 = ia) | (Y!4 = ib)))),
% 0.19/0.37 inference(quant_inst,[status(thm)],[])).
% 0.19/0.37 tff(44,plain,
% 0.19/0.37 (cA(Y!4) <=> ((Y!4 = ia) | (Y!4 = ib))),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[43, 42])).
% 0.19/0.37 tff(45,assumption,(~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))), introduced(assumption)).
% 0.19/0.37 tff(46,plain,
% 0.19/0.37 (((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5)) | requalityOnA(X!5, Y!4)),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(47,plain,
% 0.19/0.37 (requalityOnA(X!5, Y!4)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[46, 45])).
% 0.19/0.37 tff(48,plain,
% 0.19/0.37 (^[X: $i, Y: $i] : refl((cA(Y) | (~requalityOnA(X, Y))) <=> (cA(Y) | (~requalityOnA(X, Y))))),
% 0.19/0.37 inference(bind,[status(th)],[])).
% 0.19/0.37 tff(49,plain,
% 0.19/0.37 (![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y))) <=> ![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))),
% 0.19/0.37 inference(quant_intro,[status(thm)],[48])).
% 0.19/0.37 tff(50,plain,
% 0.19/0.37 (![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y))) <=> ![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(51,plain,
% 0.19/0.37 (^[X: $i, Y: $i] : rewrite((requalityOnA(X, Y) => cA(Y)) <=> (cA(Y) | (~requalityOnA(X, Y))))),
% 0.19/0.37 inference(bind,[status(th)],[])).
% 0.19/0.37 tff(52,plain,
% 0.19/0.37 (![X: $i, Y: $i] : (requalityOnA(X, Y) => cA(Y)) <=> ![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))),
% 0.19/0.37 inference(quant_intro,[status(thm)],[51])).
% 0.19/0.37 tff(53,axiom,(![X: $i, Y: $i] : (requalityOnA(X, Y) => cA(Y))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_4')).
% 0.19/0.37 tff(54,plain,
% 0.19/0.37 (![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[53, 52])).
% 0.19/0.37 tff(55,plain,
% 0.19/0.37 (![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[54, 50])).
% 0.19/0.37 tff(56,plain,(
% 0.19/0.37 ![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))),
% 0.19/0.37 inference(skolemize,[status(sab)],[55])).
% 0.19/0.37 tff(57,plain,
% 0.19/0.37 (![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[56, 49])).
% 0.19/0.37 tff(58,plain,
% 0.19/0.37 (((~![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))) | (cA(Y!4) | (~requalityOnA(X!5, Y!4)))) <=> ((~![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))) | cA(Y!4) | (~requalityOnA(X!5, Y!4)))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(59,plain,
% 0.19/0.37 ((~![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))) | (cA(Y!4) | (~requalityOnA(X!5, Y!4)))),
% 0.19/0.37 inference(quant_inst,[status(thm)],[])).
% 0.19/0.37 tff(60,plain,
% 0.19/0.37 ((~![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))) | cA(Y!4) | (~requalityOnA(X!5, Y!4))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[59, 58])).
% 0.19/0.37 tff(61,plain,
% 0.19/0.37 (cA(Y!4)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[60, 57, 47])).
% 0.19/0.37 tff(62,plain,
% 0.19/0.37 ((~(cA(Y!4) <=> ((Y!4 = ia) | (Y!4 = ib)))) | (~cA(Y!4)) | ((Y!4 = ia) | (Y!4 = ib))),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(63,plain,
% 0.19/0.37 ((~(cA(Y!4) <=> ((Y!4 = ia) | (Y!4 = ib)))) | ((Y!4 = ia) | (Y!4 = ib))),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[62, 61])).
% 0.19/0.37 tff(64,plain,
% 0.19/0.37 ((Y!4 = ia) | (Y!4 = ib)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[63, 44])).
% 0.19/0.37 tff(65,plain,
% 0.19/0.37 (((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5)) | (~requalityOnA(Y!4, X!5))),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(66,plain,
% 0.19/0.37 (~requalityOnA(Y!4, X!5)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[65, 45])).
% 0.19/0.37 tff(67,assumption,(Y!4 = ib), introduced(assumption)).
% 0.19/0.37 tff(68,plain,
% 0.19/0.37 (ib = Y!4),
% 0.19/0.37 inference(symmetry,[status(thm)],[67])).
% 0.19/0.37 tff(69,plain,
% 0.19/0.37 (requalityOnA(X!5, ib) <=> requalityOnA(X!5, Y!4)),
% 0.19/0.37 inference(monotonicity,[status(thm)],[68])).
% 0.19/0.37 tff(70,plain,
% 0.19/0.37 (requalityOnA(X!5, Y!4) <=> requalityOnA(X!5, ib)),
% 0.19/0.37 inference(symmetry,[status(thm)],[69])).
% 0.19/0.37 tff(71,assumption,(requalityOnA(X!5, Y!4)), introduced(assumption)).
% 0.19/0.37 tff(72,plain,
% 0.19/0.37 (requalityOnA(X!5, ib)),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[71, 70])).
% 0.19/0.37 tff(73,plain,
% 0.19/0.37 (requalityOnA(ib, ib) <=> requalityOnA(ib, ib)),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(74,axiom,(requalityOnA(ib, ib)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_8')).
% 0.19/0.37 tff(75,plain,
% 0.19/0.37 (requalityOnA(ib, ib)),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[74, 73])).
% 0.19/0.37 tff(76,plain,
% 0.19/0.37 (^[X: $i, Y: $i, Z: $i] : refl(((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X))) <=> ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X))))),
% 0.19/0.37 inference(bind,[status(th)],[])).
% 0.19/0.37 tff(77,plain,
% 0.19/0.37 (![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X))) <=> ![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))),
% 0.19/0.37 inference(quant_intro,[status(thm)],[76])).
% 0.19/0.37 tff(78,plain,
% 0.19/0.37 (^[X: $i, Y: $i, Z: $i] : trans(monotonicity(trans(monotonicity(rewrite((requalityOnA(Y, X) & requalityOnA(Z, X)) <=> (~((~requalityOnA(Y, X)) | (~requalityOnA(Z, X))))), ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) <=> (~(~((~requalityOnA(Y, X)) | (~requalityOnA(Z, X))))))), rewrite((~(~((~requalityOnA(Y, X)) | (~requalityOnA(Z, X))))) <=> ((~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))), ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) <=> ((~requalityOnA(Y, X)) | (~requalityOnA(Z, X))))), (((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z)) <=> (((~requalityOnA(Y, X)) | (~requalityOnA(Z, X))) | (Y = Z)))), rewrite((((~requalityOnA(Y, X)) | (~requalityOnA(Z, X))) | (Y = Z)) <=> ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))), (((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z)) <=> ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))))),
% 0.19/0.37 inference(bind,[status(th)],[])).
% 0.19/0.37 tff(79,plain,
% 0.19/0.37 (![X: $i, Y: $i, Z: $i] : ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z)) <=> ![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))),
% 0.19/0.37 inference(quant_intro,[status(thm)],[78])).
% 0.19/0.38 tff(80,plain,
% 0.19/0.38 (![X: $i, Y: $i, Z: $i] : ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(81,plain,
% 0.19/0.38 (^[X: $i, Y: $i, Z: $i] : rewrite(((requalityOnA(Y, X) & requalityOnA(Z, X)) => (Y = Z)) <=> ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z)))),
% 0.19/0.38 inference(bind,[status(th)],[])).
% 0.19/0.38 tff(82,plain,
% 0.19/0.38 (![X: $i, Y: $i, Z: $i] : ((requalityOnA(Y, X) & requalityOnA(Z, X)) => (Y = Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z))),
% 0.19/0.38 inference(quant_intro,[status(thm)],[81])).
% 0.19/0.38 tff(83,axiom,(![X: $i, Y: $i, Z: $i] : ((requalityOnA(Y, X) & requalityOnA(Z, X)) => (Y = Z))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_3')).
% 0.19/0.38 tff(84,plain,
% 0.19/0.38 (![X: $i, Y: $i, Z: $i] : ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.19/0.38 tff(85,plain,
% 0.19/0.38 (![X: $i, Y: $i, Z: $i] : ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[84, 80])).
% 0.19/0.38 tff(86,plain,(
% 0.19/0.38 ![X: $i, Y: $i, Z: $i] : ((~(requalityOnA(Y, X) & requalityOnA(Z, X))) | (Y = Z))),
% 0.19/0.38 inference(skolemize,[status(sab)],[85])).
% 0.19/0.38 tff(87,plain,
% 0.19/0.38 (![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[86, 79])).
% 0.19/0.38 tff(88,plain,
% 0.19/0.38 (![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[87, 77])).
% 0.19/0.38 tff(89,plain,
% 0.19/0.38 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((~requalityOnA(ib, ib)) | (X!5 = ib) | (~requalityOnA(X!5, ib)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (~requalityOnA(ib, ib)) | (X!5 = ib) | (~requalityOnA(X!5, ib)))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(90,plain,
% 0.19/0.38 (((X!5 = ib) | (~requalityOnA(X!5, ib)) | (~requalityOnA(ib, ib))) <=> ((~requalityOnA(ib, ib)) | (X!5 = ib) | (~requalityOnA(X!5, ib)))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(91,plain,
% 0.19/0.38 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!5 = ib) | (~requalityOnA(X!5, ib)) | (~requalityOnA(ib, ib)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((~requalityOnA(ib, ib)) | (X!5 = ib) | (~requalityOnA(X!5, ib))))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[90])).
% 0.19/0.38 tff(92,plain,
% 0.19/0.38 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!5 = ib) | (~requalityOnA(X!5, ib)) | (~requalityOnA(ib, ib)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (~requalityOnA(ib, ib)) | (X!5 = ib) | (~requalityOnA(X!5, ib)))),
% 0.19/0.38 inference(transitivity,[status(thm)],[91, 89])).
% 0.19/0.38 tff(93,plain,
% 0.19/0.38 ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!5 = ib) | (~requalityOnA(X!5, ib)) | (~requalityOnA(ib, ib)))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(94,plain,
% 0.19/0.38 ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (~requalityOnA(ib, ib)) | (X!5 = ib) | (~requalityOnA(X!5, ib))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[93, 92])).
% 0.19/0.38 tff(95,plain,
% 0.19/0.38 ((X!5 = ib) | (~requalityOnA(X!5, ib))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[94, 88, 75])).
% 0.19/0.38 tff(96,plain,
% 0.19/0.38 (X!5 = ib),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[95, 72])).
% 0.19/0.38 tff(97,plain,
% 0.19/0.38 (requalityOnA(Y!4, X!5) <=> requalityOnA(ib, ib)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[67, 96])).
% 0.19/0.38 tff(98,plain,
% 0.19/0.38 (requalityOnA(ib, ib) <=> requalityOnA(Y!4, X!5)),
% 0.19/0.38 inference(symmetry,[status(thm)],[97])).
% 0.19/0.38 tff(99,plain,
% 0.19/0.38 (requalityOnA(Y!4, X!5)),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[75, 98])).
% 0.19/0.38 tff(100,assumption,(~requalityOnA(Y!4, X!5)), introduced(assumption)).
% 0.19/0.38 tff(101,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[100, 99])).
% 0.19/0.38 tff(102,plain,((~(Y!4 = ib)) | requalityOnA(Y!4, X!5) | (~requalityOnA(X!5, Y!4))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(103,plain,
% 0.19/0.38 (~(Y!4 = ib)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[102, 66, 47])).
% 0.19/0.38 tff(104,plain,
% 0.19/0.38 ((~((Y!4 = ia) | (Y!4 = ib))) | (Y!4 = ia) | (Y!4 = ib)),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(105,plain,
% 0.19/0.38 (Y!4 = ia),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[104, 103, 64])).
% 0.19/0.38 tff(106,plain,
% 0.19/0.38 (ia = Y!4),
% 0.19/0.38 inference(symmetry,[status(thm)],[105])).
% 0.19/0.38 tff(107,plain,
% 0.19/0.38 (requalityOnA(X!5, ia) <=> requalityOnA(X!5, Y!4)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[106])).
% 0.19/0.38 tff(108,plain,
% 0.19/0.38 (requalityOnA(X!5, Y!4) <=> requalityOnA(X!5, ia)),
% 0.19/0.38 inference(symmetry,[status(thm)],[107])).
% 0.19/0.38 tff(109,plain,
% 0.19/0.38 (requalityOnA(X!5, ia)),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[47, 108])).
% 0.19/0.38 tff(110,plain,
% 0.19/0.38 (requalityOnA(ia, ia) <=> requalityOnA(ia, ia)),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(111,axiom,(requalityOnA(ia, ia)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_6')).
% 0.19/0.38 tff(112,plain,
% 0.19/0.38 (requalityOnA(ia, ia)),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[111, 110])).
% 0.19/0.38 tff(113,plain,
% 0.19/0.38 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((~requalityOnA(ia, ia)) | (~requalityOnA(X!5, ia)) | (X!5 = ia))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (~requalityOnA(ia, ia)) | (~requalityOnA(X!5, ia)) | (X!5 = ia))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(114,plain,
% 0.19/0.38 (((X!5 = ia) | (~requalityOnA(X!5, ia)) | (~requalityOnA(ia, ia))) <=> ((~requalityOnA(ia, ia)) | (~requalityOnA(X!5, ia)) | (X!5 = ia))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(115,plain,
% 0.19/0.38 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!5 = ia) | (~requalityOnA(X!5, ia)) | (~requalityOnA(ia, ia)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((~requalityOnA(ia, ia)) | (~requalityOnA(X!5, ia)) | (X!5 = ia)))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[114])).
% 0.19/0.38 tff(116,plain,
% 0.19/0.38 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!5 = ia) | (~requalityOnA(X!5, ia)) | (~requalityOnA(ia, ia)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (~requalityOnA(ia, ia)) | (~requalityOnA(X!5, ia)) | (X!5 = ia))),
% 0.19/0.38 inference(transitivity,[status(thm)],[115, 113])).
% 0.19/0.38 tff(117,plain,
% 0.19/0.38 ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!5 = ia) | (~requalityOnA(X!5, ia)) | (~requalityOnA(ia, ia)))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(118,plain,
% 0.19/0.38 ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (~requalityOnA(ia, ia)) | (~requalityOnA(X!5, ia)) | (X!5 = ia)),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[117, 116])).
% 0.19/0.38 tff(119,plain,
% 0.19/0.38 ((~requalityOnA(X!5, ia)) | (X!5 = ia)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[118, 88, 112])).
% 0.19/0.38 tff(120,plain,
% 0.19/0.38 (X!5 = ia),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[119, 109])).
% 0.19/0.38 tff(121,plain,
% 0.19/0.38 (requalityOnA(Y!4, X!5) <=> requalityOnA(ia, ia)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[105, 120])).
% 0.19/0.38 tff(122,plain,
% 0.19/0.38 (requalityOnA(ia, ia) <=> requalityOnA(Y!4, X!5)),
% 0.19/0.38 inference(symmetry,[status(thm)],[121])).
% 0.19/0.38 tff(123,plain,
% 0.19/0.38 (requalityOnA(Y!4, X!5)),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[112, 122])).
% 0.19/0.38 tff(124,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[66, 123])).
% 0.19/0.38 tff(125,plain,((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(126,plain,
% 0.19/0.38 ((~![X: $i] : (cA(X) <=> ((X = ia) | (X = ib)))) | (cA(Y!2) <=> ((Y!2 = ia) | (Y!2 = ib)))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(127,plain,
% 0.19/0.38 (cA(Y!2) <=> ((Y!2 = ia) | (Y!2 = ib))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[126, 42])).
% 0.19/0.38 tff(128,assumption,(~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))), introduced(assumption)).
% 0.19/0.38 tff(129,plain,
% 0.19/0.38 (((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2))) | requalityOnA(X!3, Y!2)),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(130,plain,
% 0.19/0.38 (requalityOnA(X!3, Y!2)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[129, 128])).
% 0.19/0.38 tff(131,plain,
% 0.19/0.38 (((~![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))) | (cA(Y!2) | (~requalityOnA(X!3, Y!2)))) <=> ((~![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))) | cA(Y!2) | (~requalityOnA(X!3, Y!2)))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(132,plain,
% 0.19/0.38 ((~![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))) | (cA(Y!2) | (~requalityOnA(X!3, Y!2)))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(133,plain,
% 0.19/0.38 ((~![X: $i, Y: $i] : (cA(Y) | (~requalityOnA(X, Y)))) | cA(Y!2) | (~requalityOnA(X!3, Y!2))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[132, 131])).
% 0.19/0.38 tff(134,plain,
% 0.19/0.38 (cA(Y!2)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[133, 57, 130])).
% 0.19/0.38 tff(135,plain,
% 0.19/0.38 ((~(cA(Y!2) <=> ((Y!2 = ia) | (Y!2 = ib)))) | (~cA(Y!2)) | ((Y!2 = ia) | (Y!2 = ib))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(136,plain,
% 0.19/0.38 ((~(cA(Y!2) <=> ((Y!2 = ia) | (Y!2 = ib)))) | ((Y!2 = ia) | (Y!2 = ib))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[135, 134])).
% 0.19/0.38 tff(137,plain,
% 0.19/0.38 ((Y!2 = ia) | (Y!2 = ib)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[136, 127])).
% 0.19/0.38 tff(138,plain,
% 0.19/0.38 (((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2))) | (~(X!3 = ib))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(139,plain,
% 0.19/0.38 (~(X!3 = ib)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[138, 128])).
% 0.19/0.38 tff(140,assumption,(Y!2 = ib), introduced(assumption)).
% 0.19/0.38 tff(141,plain,
% 0.19/0.38 (ib = Y!2),
% 0.19/0.38 inference(symmetry,[status(thm)],[140])).
% 0.19/0.38 tff(142,plain,
% 0.19/0.38 (requalityOnA(X!3, ib) <=> requalityOnA(X!3, Y!2)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[141])).
% 0.19/0.38 tff(143,plain,
% 0.19/0.38 (requalityOnA(X!3, Y!2) <=> requalityOnA(X!3, ib)),
% 0.19/0.38 inference(symmetry,[status(thm)],[142])).
% 0.19/0.38 tff(144,assumption,(requalityOnA(X!3, Y!2)), introduced(assumption)).
% 0.19/0.38 tff(145,plain,
% 0.19/0.38 (requalityOnA(X!3, ib)),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[144, 143])).
% 0.19/0.38 tff(146,assumption,(~(X!3 = ib)), introduced(assumption)).
% 0.19/0.38 tff(147,plain,
% 0.19/0.38 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!3 = ib) | (~requalityOnA(ib, ib)) | (~requalityOnA(X!3, ib)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (X!3 = ib) | (~requalityOnA(ib, ib)) | (~requalityOnA(X!3, ib)))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(148,plain,
% 0.19/0.38 (((X!3 = ib) | (~requalityOnA(X!3, ib)) | (~requalityOnA(ib, ib))) <=> ((X!3 = ib) | (~requalityOnA(ib, ib)) | (~requalityOnA(X!3, ib)))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(149,plain,
% 0.19/0.38 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!3 = ib) | (~requalityOnA(X!3, ib)) | (~requalityOnA(ib, ib)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!3 = ib) | (~requalityOnA(ib, ib)) | (~requalityOnA(X!3, ib))))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[148])).
% 0.19/0.38 tff(150,plain,
% 0.19/0.38 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!3 = ib) | (~requalityOnA(X!3, ib)) | (~requalityOnA(ib, ib)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (X!3 = ib) | (~requalityOnA(ib, ib)) | (~requalityOnA(X!3, ib)))),
% 0.19/0.38 inference(transitivity,[status(thm)],[149, 147])).
% 0.19/0.38 tff(151,plain,
% 0.19/0.38 ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!3 = ib) | (~requalityOnA(X!3, ib)) | (~requalityOnA(ib, ib)))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(152,plain,
% 0.19/0.38 ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (X!3 = ib) | (~requalityOnA(ib, ib)) | (~requalityOnA(X!3, ib))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[151, 150])).
% 0.19/0.38 tff(153,plain,
% 0.19/0.38 (~requalityOnA(X!3, ib)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[152, 88, 75, 146])).
% 0.19/0.39 tff(154,plain,
% 0.19/0.39 ($false),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[153, 145])).
% 0.19/0.39 tff(155,plain,((~(Y!2 = ib)) | (~requalityOnA(X!3, Y!2)) | (X!3 = ib)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.39 tff(156,plain,
% 0.19/0.39 (~(Y!2 = ib)),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[155, 130, 139])).
% 0.19/0.39 tff(157,plain,
% 0.19/0.39 ((~((Y!2 = ia) | (Y!2 = ib))) | (Y!2 = ia) | (Y!2 = ib)),
% 0.19/0.39 inference(tautology,[status(thm)],[])).
% 0.19/0.39 tff(158,plain,
% 0.19/0.39 (Y!2 = ia),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[157, 156, 137])).
% 0.19/0.39 tff(159,plain,
% 0.19/0.39 (ia = Y!2),
% 0.19/0.39 inference(symmetry,[status(thm)],[158])).
% 0.19/0.39 tff(160,plain,
% 0.19/0.39 (requalityOnA(X!3, ia) <=> requalityOnA(X!3, Y!2)),
% 0.19/0.39 inference(monotonicity,[status(thm)],[159])).
% 0.19/0.39 tff(161,plain,
% 0.19/0.39 (requalityOnA(X!3, Y!2) <=> requalityOnA(X!3, ia)),
% 0.19/0.39 inference(symmetry,[status(thm)],[160])).
% 0.19/0.39 tff(162,plain,
% 0.19/0.39 (requalityOnA(X!3, ia)),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[130, 161])).
% 0.19/0.39 tff(163,plain,
% 0.19/0.39 (((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2))) | (~(X!3 = ia))),
% 0.19/0.39 inference(tautology,[status(thm)],[])).
% 0.19/0.39 tff(164,plain,
% 0.19/0.39 (~(X!3 = ia)),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[163, 128])).
% 0.19/0.39 tff(165,plain,
% 0.19/0.39 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((~requalityOnA(ia, ia)) | (X!3 = ia) | (~requalityOnA(X!3, ia)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (~requalityOnA(ia, ia)) | (X!3 = ia) | (~requalityOnA(X!3, ia)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(166,plain,
% 0.19/0.39 (((X!3 = ia) | (~requalityOnA(X!3, ia)) | (~requalityOnA(ia, ia))) <=> ((~requalityOnA(ia, ia)) | (X!3 = ia) | (~requalityOnA(X!3, ia)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(167,plain,
% 0.19/0.39 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!3 = ia) | (~requalityOnA(X!3, ia)) | (~requalityOnA(ia, ia)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((~requalityOnA(ia, ia)) | (X!3 = ia) | (~requalityOnA(X!3, ia))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[166])).
% 0.19/0.39 tff(168,plain,
% 0.19/0.39 (((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!3 = ia) | (~requalityOnA(X!3, ia)) | (~requalityOnA(ia, ia)))) <=> ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (~requalityOnA(ia, ia)) | (X!3 = ia) | (~requalityOnA(X!3, ia)))),
% 0.19/0.39 inference(transitivity,[status(thm)],[167, 165])).
% 0.19/0.39 tff(169,plain,
% 0.19/0.39 ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | ((X!3 = ia) | (~requalityOnA(X!3, ia)) | (~requalityOnA(ia, ia)))),
% 0.19/0.39 inference(quant_inst,[status(thm)],[])).
% 0.19/0.39 tff(170,plain,
% 0.19/0.39 ((~![X: $i, Y: $i, Z: $i] : ((Y = Z) | (~requalityOnA(Y, X)) | (~requalityOnA(Z, X)))) | (~requalityOnA(ia, ia)) | (X!3 = ia) | (~requalityOnA(X!3, ia))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[169, 168])).
% 0.19/0.39 tff(171,plain,
% 0.19/0.39 (~requalityOnA(X!3, ia)),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[170, 88, 112, 164])).
% 0.19/0.39 tff(172,plain,
% 0.19/0.39 ($false),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[171, 162])).
% 0.19/0.39 tff(173,plain,((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.39 tff(174,plain,
% 0.19/0.39 (cowlThing(ic) <=> cowlThing(ic)),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(175,axiom,(cowlThing(ic)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_9')).
% 0.19/0.39 tff(176,plain,
% 0.19/0.39 (cowlThing(ic)),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[175, 174])).
% 0.19/0.39 tff(177,plain,
% 0.19/0.39 (cowlThing(ib) <=> cowlThing(ib)),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(178,axiom,(cowlThing(ib)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_7')).
% 0.19/0.39 tff(179,plain,
% 0.19/0.39 (cowlThing(ib)),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[178, 177])).
% 0.19/0.39 tff(180,plain,
% 0.19/0.39 (cowlThing(ia) <=> cowlThing(ia)),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(181,axiom,(cowlThing(ia)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_5')).
% 0.19/0.39 tff(182,plain,
% 0.19/0.39 (cowlThing(ia)),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[181, 180])).
% 0.19/0.39 tff(183,plain,
% 0.19/0.39 (((~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | ((~cowlThing(X!0)) | cowlNothing(X!0)) | (xsd_integer(X!1) <=> xsd_string(X!1))) <=> ((~cowlThing(X!0)) | (~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | cowlNothing(X!0) | (xsd_integer(X!1) <=> xsd_string(X!1)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(184,plain,
% 0.19/0.39 ((~(~((~cowlThing(X!0)) | cowlNothing(X!0)))) <=> ((~cowlThing(X!0)) | cowlNothing(X!0))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(185,plain,
% 0.19/0.39 ((cowlThing(X!0) & (~cowlNothing(X!0))) <=> (~((~cowlThing(X!0)) | cowlNothing(X!0)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(186,plain,
% 0.19/0.39 ((~(cowlThing(X!0) & (~cowlNothing(X!0)))) <=> (~(~((~cowlThing(X!0)) | cowlNothing(X!0))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[185])).
% 0.19/0.39 tff(187,plain,
% 0.19/0.39 ((~(cowlThing(X!0) & (~cowlNothing(X!0)))) <=> ((~cowlThing(X!0)) | cowlNothing(X!0))),
% 0.19/0.39 inference(transitivity,[status(thm)],[186, 184])).
% 0.19/0.39 tff(188,plain,
% 0.19/0.39 ((~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) <=> (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(189,plain,
% 0.19/0.39 (((~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | (~(cowlThing(X!0) & (~cowlNothing(X!0)))) | (xsd_integer(X!1) <=> xsd_string(X!1))) <=> ((~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | ((~cowlThing(X!0)) | cowlNothing(X!0)) | (xsd_integer(X!1) <=> xsd_string(X!1)))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[188, 187])).
% 0.19/0.39 tff(190,plain,
% 0.19/0.39 (((~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | (~(cowlThing(X!0) & (~cowlNothing(X!0)))) | (xsd_integer(X!1) <=> xsd_string(X!1))) <=> ((~cowlThing(X!0)) | (~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | cowlNothing(X!0) | (xsd_integer(X!1) <=> xsd_string(X!1)))),
% 0.19/0.39 inference(transitivity,[status(thm)],[189, 183])).
% 0.19/0.39 tff(191,plain,
% 0.19/0.39 (((~(cowlThing(X!0) & (~cowlNothing(X!0)))) | (xsd_integer(X!1) <=> xsd_string(X!1)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | (~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic))) <=> ((~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | (~(cowlThing(X!0) & (~cowlNothing(X!0)))) | (xsd_integer(X!1) <=> xsd_string(X!1)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(192,plain,
% 0.19/0.39 ((~((X!3 = ic) | (X!3 = ib) | (X!3 = ia) | (~requalityOnA(X!3, Y!2)))) <=> (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(193,plain,
% 0.19/0.39 (((~(cowlThing(X!0) & (~cowlNothing(X!0)))) | (xsd_integer(X!1) <=> xsd_string(X!1)) | (~((X!3 = ic) | (X!3 = ib) | (X!3 = ia) | (~requalityOnA(X!3, Y!2)))) | (~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic))) <=> ((~(cowlThing(X!0) & (~cowlNothing(X!0)))) | (xsd_integer(X!1) <=> xsd_string(X!1)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | (~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic)))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[192])).
% 0.19/0.39 tff(194,plain,
% 0.19/0.39 (((~(cowlThing(X!0) & (~cowlNothing(X!0)))) | (xsd_integer(X!1) <=> xsd_string(X!1)) | (~((X!3 = ic) | (X!3 = ib) | (X!3 = ia) | (~requalityOnA(X!3, Y!2)))) | (~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic))) <=> ((~((~requalityOnA(X!5, Y!4)) | requalityOnA(Y!4, X!5))) | (~cowlThing(ia)) | (~requalityOnA(ia, ia)) | (~cowlThing(ib)) | (~cowlThing(ic)) | (~((X!3 = ia) | (X!3 = ic) | (X!3 = ib) | (~requalityOnA(X!3, Y!2)))) | (~(cowlThing(X!0) & (~cowlNothing(X!0)))) | (xsd_integer(X!1) <=> xsd_string(X!1)))),
% 0.19/0.39 inference(transitivity,[status(thm)],[193, 191])).
% 0.19/0.39 tff(195,plain,
% 0.19/0.39 ((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic)) <=> (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(196,plain,
% 0.19/0.39 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic)))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[195])).
% 0.19/0.39 tff(197,plain,
% 0.19/0.39 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(198,plain,
% 0.19/0.39 ((~(((((((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & ![X: $i, Y: $i] : (requalityOnA(X, Y) => (((X = ia) | (X = ib)) | (X = ic)))) & ![X: $i, Y: $i] : (requalityOnA(X, Y) => requalityOnA(Y, X))) & cowlThing(ia)) & requalityOnA(ia, ia)) & cowlThing(ib)) & cowlThing(ic))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(199,axiom,(~(((((((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & ![X: $i, Y: $i] : (requalityOnA(X, Y) => (((X = ia) | (X = ib)) | (X = ic)))) & ![X: $i, Y: $i] : (requalityOnA(X, Y) => requalityOnA(Y, X))) & cowlThing(ia)) & requalityOnA(ia, ia)) & cowlThing(ib)) & cowlThing(ic))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','the_axiom')).
% 0.19/0.40 tff(200,plain,
% 0.19/0.40 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[199, 198])).
% 0.19/0.40 tff(201,plain,
% 0.19/0.40 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[200, 196])).
% 0.19/0.40 tff(202,plain,
% 0.19/0.40 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[201, 197])).
% 0.19/0.40 tff(203,plain,
% 0.19/0.40 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i, Y: $i] : ((X = ic) | (X = ib) | (X = ia) | (~requalityOnA(X, Y))) & ![X: $i, Y: $i] : ((~requalityOnA(X, Y)) | requalityOnA(Y, X)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[202, 196])).
% 0.19/0.40 unexpected number of arguments: (let ((a!1 (forall ((X $i)) (and (cowlThing X) (not (cowlNothing X)))))
% 0.19/0.40 (a!2 (not (and (cowlThing X!0) (not (cowlNothing X!0)))))
% 0.19/0.40 (a!3 (forall ((X $i)) (not (= (xsd_integer X) (xsd_string X)))))
% 0.19/0.40 (a!5 (forall ((X $i) (Y $i))
% 0.19/0.40 (or (= X ic) (= X ib) (= X ia) (not (requalityOnA X Y)))))
% 0.19/0.40 (a!6 (not (or (= X!3 ic)
% 0.19/0.40 (= X!3 ib)
% 0.19/0.40 (= X!3 ia)
% 0.19/0.40 (not (requalityOnA X!3 Y!2)))))
% 0.19/0.40 (a!7 (forall ((X $i) (Y $i))
% 0.19/0.40 (or (not (requalityOnA X Y)) (requalityOnA Y X))))
% 0.19/0.40 (a!8 (not (or (not (requalityOnA X!5 Y!4)) (requalityOnA Y!4 X!5))))
% 0.19/0.40 (a!9 (refl (~ (not (cowlThing ia)) (not (cowlThing ia)))))
% 0.19/0.40 (a!10 (refl (~ (not (requalityOnA ia ia)) (not (requalityOnA ia ia)))))
% 0.19/0.40 (a!11 (refl (~ (not (cowlThing ib)) (not (cowlThing ib)))))
% 0.19/0.40 (a!12 (refl (~ (not (cowlThing ic)) (not (cowlThing ic))))))
% 0.19/0.40 (let ((a!4 (sk (~ (not a!3) (= (xsd_integer X!1) (xsd_string X!1)))))
% 0.19/0.40 (a!13 (~ (not (and a!1
% 0.19/0.40 a!3
% 0.19/0.40 a!5
% 0.19/0.40 a!7
% 0.19/0.40 (cowlThing ia)
% 0.19/0.40 (requalityOnA ia ia)
% 0.19/0.40 (cowlThing ib)
% 0.19/0.40 (cowlThing ic)))
% 0.19/0.40 (or a!2
% 0.19/0.40 (= (xsd_integer X!1) (xsd_string X!1))
% 0.19/0.40 a!6
% 0.19/0.40 a!8
% 0.19/0.40 (not (cowlThing ia))
% 0.19/0.40 (not (requalityOnA ia ia))
% 0.19/0.40 (not (cowlThing ib))
% 0.19/0.40 (not (cowlThing ic))))))
% 0.19/0.40 (nnf-neg (sk (~ (not a!1) a!2))
% 0.19/0.40 a!4
% 0.19/0.40 (sk (~ (not a!5) a!6))
% 0.19/0.40 (sk (~ (not a!7) a!8))
% 0.19/0.40 a!9
% 0.19/0.40 a!10
% 0.19/0.40 a!11
% 0.19/0.40 a!12
% 0.19/0.40 a!13)))
% 0.19/0.40 Proof display could not be completed: unexpected number of arguments
% 0.19/0.40 % E exiting
%------------------------------------------------------------------------------