%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ITP322_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n010.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:12:42 AM UTC 2025
% Result : Theorem 0.37s 0.55s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : ITP322_1 : TPTP v9.0.0. Released v8.0.0.
% 0.04/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n010.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 18:47:26 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.37/0.55 % SZS status Theorem
% 0.37/0.55 % SZS output start Proof
% 0.37/0.55 tff(tptp_fun__fun_app_b__type, type, (
% 0.37/0.55 tptp_fun__fun_app_b_: ( |'B_set_b_set_fun$'| * |'B_set$'| ) > |'B_set$'|)).
% 0.37/0.55 tff(tptp_fun__bot___type, type, (
% 0.37/0.55 tptp_fun__bot__: |'B_set$'|)).
% 0.37/0.55 tff(tptp_fun__insert___type, type, (
% 0.37/0.55 tptp_fun__insert__: |'B$'| > |'B_set_b_set_fun$'|)).
% 0.37/0.55 tff(tptp_fun__a___type, type, (
% 0.37/0.55 tptp_fun__a__: |'B$'|)).
% 0.37/0.55 tff(tptp_fun__fun_app_c__type, type, (
% 0.37/0.55 tptp_fun__fun_app_c_: ( |'B_set_b_set_b_set_fun_fun$'| * |'B_set$'| ) > |'B_set_b_set_fun$'|)).
% 0.37/0.55 tff(tptp_fun__top___type, type, (
% 0.37/0.55 tptp_fun__top__: |'B_set$'|)).
% 0.37/0.55 tff(tptp_fun__minus___type, type, (
% 0.37/0.55 tptp_fun__minus__: |'B_set_b_set_b_set_fun_fun$'|)).
% 0.37/0.55 tff(tptp_fun__sup___type, type, (
% 0.37/0.55 tptp_fun__sup__: |'B_set_b_set_b_set_fun_fun$'|)).
% 0.37/0.55 tff(tptp_fun__fun_app_d__type, type, (
% 0.37/0.55 tptp_fun__fun_app_d_: ( |'B_bool_fun_b_set_fun$'| * |'B_bool_fun$'| ) > |'B_set$'|)).
% 0.37/0.55 tff(tptp_fun__bot_b__type, type, (
% 0.37/0.55 tptp_fun__bot_b_: |'B_bool_fun$'|)).
% 0.37/0.55 tff(tptp_fun__collect___type, type, (
% 0.37/0.55 tptp_fun__collect__: |'B_bool_fun_b_set_fun$'|)).
% 0.37/0.55 tff(tptp_fun__b___type, type, (
% 0.37/0.55 tptp_fun__b__: |'B$'|)).
% 0.37/0.55 tff(tptp_fun__top_b__type, type, (
% 0.37/0.55 tptp_fun__top_b_: |'B_bool_fun$'|)).
% 0.37/0.55 tff(1,plain,
% 0.37/0.55 ((|'bot$'| = tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)) <=> (|'bot$'| = tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))),
% 0.37/0.55 inference(rewrite,[status(thm)],[])).
% 0.37/0.55 tff(2,axiom,(|'bot$'| = tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom128')).
% 0.37/0.55 tff(3,plain,
% 0.37/0.55 (|'bot$'| = tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.37/0.55 tff(4,plain,
% 0.37/0.55 (tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|) = |'bot$'|),
% 0.37/0.55 inference(symmetry,[status(thm)],[3])).
% 0.37/0.55 tff(5,plain,
% 0.37/0.55 ((|'a$'| = |'b$'|) <=> (|'a$'| = |'b$'|)),
% 0.37/0.55 inference(rewrite,[status(thm)],[])).
% 0.37/0.55 tff(6,axiom,(|'a$'| = |'b$'|), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom2')).
% 0.37/0.55 tff(7,plain,
% 0.37/0.55 (|'a$'| = |'b$'|),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.37/0.55 tff(8,plain,
% 0.37/0.55 (|'b$'| = |'a$'|),
% 0.37/0.55 inference(symmetry,[status(thm)],[7])).
% 0.37/0.55 tff(9,plain,
% 0.37/0.55 (tptp_fun__insert__(|'b$'|) = tptp_fun__insert__(|'a$'|)),
% 0.37/0.55 inference(monotonicity,[status(thm)],[8])).
% 0.37/0.55 tff(10,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|)),
% 0.37/0.55 inference(monotonicity,[status(thm)],[9, 4])).
% 0.37/0.55 tff(11,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))),
% 0.37/0.55 inference(symmetry,[status(thm)],[10])).
% 0.37/0.55 tff(12,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|)) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)))),
% 0.37/0.55 inference(monotonicity,[status(thm)],[11])).
% 0.37/0.55 tff(13,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))),
% 0.37/0.55 inference(symmetry,[status(thm)],[12])).
% 0.37/0.55 tff(14,plain,
% 0.37/0.55 (^[A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : refl((tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2))) <=> (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2))))),
% 0.37/0.55 inference(bind,[status(th)],[])).
% 0.37/0.55 tff(15,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2))) <=> ![A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2)))),
% 0.37/0.55 inference(quant_intro,[status(thm)],[14])).
% 0.37/0.55 tff(16,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2))) <=> ![A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2)))),
% 0.37/0.55 inference(rewrite,[status(thm)],[])).
% 0.37/0.55 tff(17,axiom,(![A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom10')).
% 0.37/0.55 tff(18,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2)))),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[17, 16])).
% 0.37/0.55 tff(19,plain,(
% 0.37/0.55 ![A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2)))),
% 0.37/0.55 inference(skolemize,[status(sab)],[18])).
% 0.37/0.55 tff(20,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2)))),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[19, 15])).
% 0.37/0.55 tff(21,plain,
% 0.37/0.55 ((~![A__questionmark_v0: |'B_set$'|, A__questionmark_v1: |'B$'|, A__questionmark_v2: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), A__questionmark_v2)) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), A__questionmark_v2)))) | (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))))),
% 0.37/0.55 inference(quant_inst,[status(thm)],[])).
% 0.37/0.55 tff(22,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[21, 20])).
% 0.37/0.55 tff(23,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)))),
% 0.37/0.55 inference(symmetry,[status(thm)],[22])).
% 0.37/0.55 tff(24,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'bot$'|) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))),
% 0.37/0.55 inference(monotonicity,[status(thm)],[3])).
% 0.37/0.55 tff(25,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'bot$'|)) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)))),
% 0.37/0.55 inference(monotonicity,[status(thm)],[24])).
% 0.37/0.55 tff(26,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'bot$'|))),
% 0.37/0.55 inference(symmetry,[status(thm)],[25])).
% 0.37/0.55 tff(27,plain,
% 0.37/0.55 ((|'top$'| = tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)) <=> (|'top$'| = tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|))),
% 0.37/0.55 inference(rewrite,[status(thm)],[])).
% 0.37/0.55 tff(28,axiom,(|'top$'| = tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom129')).
% 0.37/0.55 tff(29,plain,
% 0.37/0.55 (|'top$'| = tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.37/0.55 tff(30,plain,
% 0.37/0.55 (tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|) = |'top$'|),
% 0.37/0.55 inference(symmetry,[status(thm)],[29])).
% 0.37/0.55 tff(31,plain,
% 0.37/0.55 (tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)) = tptp_fun__fun_app_c_(|'minus$'|, |'top$'|)),
% 0.37/0.55 inference(monotonicity,[status(thm)],[30])).
% 0.37/0.55 tff(32,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))),
% 0.37/0.55 inference(monotonicity,[status(thm)],[31, 10])).
% 0.37/0.55 tff(33,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|)) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)))),
% 0.37/0.55 inference(symmetry,[status(thm)],[32])).
% 0.37/0.55 tff(34,plain,
% 0.37/0.55 (^[A__questionmark_v0: |'B_set$'|] : refl((tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0) <=> (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0))),
% 0.37/0.55 inference(bind,[status(th)],[])).
% 0.37/0.55 tff(35,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0) <=> ![A__questionmark_v0: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0)),
% 0.37/0.55 inference(quant_intro,[status(thm)],[34])).
% 0.37/0.55 tff(36,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0) <=> ![A__questionmark_v0: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0)),
% 0.37/0.55 inference(rewrite,[status(thm)],[])).
% 0.37/0.55 tff(37,axiom,(![A__questionmark_v0: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom67')).
% 0.37/0.55 tff(38,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0)),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.37/0.55 tff(39,plain,(
% 0.37/0.55 ![A__questionmark_v0: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0)),
% 0.37/0.55 inference(skolemize,[status(sab)],[38])).
% 0.37/0.55 tff(40,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0)),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[39, 35])).
% 0.37/0.55 tff(41,plain,
% 0.37/0.55 ((~![A__questionmark_v0: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, A__questionmark_v0), |'bot$'|) = A__questionmark_v0)) | (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), |'bot$'|) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|)))),
% 0.37/0.55 inference(quant_inst,[status(thm)],[])).
% 0.37/0.55 tff(42,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), |'bot$'|) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[41, 40])).
% 0.37/0.55 tff(43,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), |'bot$'|)),
% 0.37/0.55 inference(monotonicity,[status(thm)],[4])).
% 0.37/0.55 tff(44,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)) = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'bot$'|))),
% 0.37/0.55 inference(transitivity,[status(thm)],[43, 42, 33, 26])).
% 0.37/0.55 tff(45,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'bot$'|)))),
% 0.37/0.55 inference(monotonicity,[status(thm)],[44])).
% 0.37/0.55 tff(46,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_d_(|'collect$'|, |'bot$b'|)))),
% 0.37/0.55 inference(symmetry,[status(thm)],[45])).
% 0.37/0.55 tff(47,plain,
% 0.37/0.55 (^[A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : refl((tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1)) <=> (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1)))),
% 0.37/0.55 inference(bind,[status(th)],[])).
% 0.37/0.55 tff(48,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1)) <=> ![A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1))),
% 0.37/0.55 inference(quant_intro,[status(thm)],[47])).
% 0.37/0.55 tff(49,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1)) <=> ![A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1))),
% 0.37/0.55 inference(rewrite,[status(thm)],[])).
% 0.37/0.55 tff(50,axiom,(![A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom3')).
% 0.37/0.55 tff(51,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1))),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.37/0.55 tff(52,plain,(
% 0.37/0.55 ![A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1))),
% 0.37/0.55 inference(skolemize,[status(sab)],[51])).
% 0.37/0.55 tff(53,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1))),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[52, 48])).
% 0.37/0.55 tff(54,plain,
% 0.37/0.55 ((~![A__questionmark_v0: |'B$'|, A__questionmark_v1: |'B_set$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, A__questionmark_v1), tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), A__questionmark_v1))) | (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)))),
% 0.37/0.55 inference(quant_inst,[status(thm)],[])).
% 0.37/0.55 tff(55,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'bot$'|))) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[54, 53])).
% 0.37/0.55 tff(56,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)), tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'bot$'|)))),
% 0.37/0.55 inference(symmetry,[status(thm)],[55])).
% 0.37/0.55 tff(57,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|)) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'top$'|)),
% 0.37/0.55 inference(monotonicity,[status(thm)],[30])).
% 0.37/0.55 tff(58,plain,
% 0.37/0.55 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'top$'|) = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), tptp_fun__fun_app_d_(|'collect$'|, |'top$b'|))),
% 0.37/0.55 inference(symmetry,[status(thm)],[57])).
% 0.37/0.55 tff(59,plain,
% 0.37/0.55 (^[A__questionmark_v0: |'B$'|] : refl((tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|) <=> (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|))),
% 0.37/0.55 inference(bind,[status(th)],[])).
% 0.37/0.55 tff(60,plain,
% 0.37/0.55 (![A__questionmark_v0: |'B$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|) <=> ![A__questionmark_v0: |'B$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|)),
% 0.39/0.59 inference(quant_intro,[status(thm)],[59])).
% 0.39/0.59 tff(61,plain,
% 0.39/0.59 (![A__questionmark_v0: |'B$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|) <=> ![A__questionmark_v0: |'B$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|)),
% 0.39/0.59 inference(rewrite,[status(thm)],[])).
% 0.39/0.59 tff(62,axiom,(![A__questionmark_v0: |'B$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom66')).
% 0.39/0.59 tff(63,plain,
% 0.39/0.59 (![A__questionmark_v0: |'B$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|)),
% 0.39/0.59 inference(modus_ponens,[status(thm)],[62, 61])).
% 0.39/0.59 tff(64,plain,(
% 0.39/0.59 ![A__questionmark_v0: |'B$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|)),
% 0.39/0.59 inference(skolemize,[status(sab)],[63])).
% 0.39/0.59 tff(65,plain,
% 0.39/0.59 (![A__questionmark_v0: |'B$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|)),
% 0.39/0.59 inference(modus_ponens,[status(thm)],[64, 60])).
% 0.39/0.59 tff(66,plain,
% 0.39/0.59 ((~![A__questionmark_v0: |'B$'|] : (tptp_fun__fun_app_b_(tptp_fun__insert__(A__questionmark_v0), |'top$'|) = |'top$'|)) | (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'top$'|) = |'top$'|)),
% 0.39/0.59 inference(quant_inst,[status(thm)],[])).
% 0.39/0.59 tff(67,plain,
% 0.39/0.59 (tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'top$'|) = |'top$'|),
% 0.39/0.59 inference(unit_resolution,[status(thm)],[66, 65])).
% 0.39/0.59 tff(68,plain,
% 0.39/0.59 (|'top$'| = tptp_fun__fun_app_b_(tptp_fun__insert__(|'b$'|), |'top$'|)),
% 0.39/0.59 inference(symmetry,[status(thm)],[67])).
% 0.39/0.59 tff(69,plain,
% 0.39/0.59 (|'top$'| = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))),
% 0.39/0.59 inference(transitivity,[status(thm)],[68, 58, 56, 46, 23, 13])).
% 0.39/0.59 tff(70,plain,
% 0.39/0.59 ((~(|'top$'| = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|)))) <=> (~(|'top$'| = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))))),
% 0.39/0.59 inference(rewrite,[status(thm)],[])).
% 0.39/0.59 tff(71,axiom,(~(|'top$'| = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','conjecture1')).
% 0.39/0.59 tff(72,plain,
% 0.39/0.59 (~(|'top$'| = tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'sup$'|, tptp_fun__fun_app_b_(tptp_fun__fun_app_c_(|'minus$'|, |'top$'|), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|))), tptp_fun__fun_app_b_(tptp_fun__insert__(|'a$'|), |'bot$'|)))),
% 0.39/0.59 inference(modus_ponens,[status(thm)],[71, 70])).
% 0.39/0.59 tff(73,plain,
% 0.39/0.59 ($false),
% 0.39/0.59 inference(unit_resolution,[status(thm)],[72, 69])).
% 0.39/0.59 % SZS output end Proof
% 0.39/0.59 % E exiting
%------------------------------------------------------------------------------