%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ITP367_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n008.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:45 AM UTC 2025
% Result : Theorem 0.19s 0.56s
% Output : Proof 0.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : ITP367_1 : TPTP v9.0.0. Released v8.0.0.
% 0.10/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n008.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:33 EDT 2025
% 0.18/0.33 % CPUTime :
% 0.19/0.56 % SZS status Theorem
% 0.19/0.56 % SZS output start Proof
% 0.19/0.56 tff(tptp_fun__fun_app_a__type, type, (
% 0.19/0.56 tptp_fun__fun_app_a_: ( |'A_ltln_set_bool_fun$'| * |'A_ltln_set$'| ) > $o)).
% 0.19/0.56 tff(tptp_fun__y___type, type, (
% 0.19/0.56 tptp_fun__y__: |'A_ltln_set$'|)).
% 0.19/0.56 tff(tptp_fun__finite___type, type, (
% 0.19/0.56 tptp_fun__finite__: |'A_ltln_set_bool_fun$'|)).
% 0.19/0.56 tff(tptp_fun__x___type, type, (
% 0.19/0.56 tptp_fun__x__: |'A_ltln_set$'|)).
% 0.19/0.56 tff(tptp_fun__fun_app_c__type, type, (
% 0.19/0.56 tptp_fun__fun_app_c_: ( |'A_ltln_set_a_ltln_set_fun$'| * |'A_ltln_set$'| ) > |'A_ltln_set$'|)).
% 0.19/0.56 tff(tptp_fun__fun_app_d__type, type, (
% 0.19/0.56 tptp_fun__fun_app_d_: ( |'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$'| * |'A_ltln_set$'| ) > |'A_ltln_set_a_ltln_set_fun$'|)).
% 0.19/0.56 tff(tptp_fun__sup___type, type, (
% 0.19/0.56 tptp_fun__sup__: |'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$'|)).
% 0.19/0.56 tff(tptp_fun__fun_app_h__type, type, (
% 0.19/0.56 tptp_fun__fun_app_h_: ( |'A_ltln_a_ltln_set_fun$'| * |'A_ltln$'| ) > |'A_ltln_set$'|)).
% 0.19/0.56 tff(tptp_fun__phi___type, type, (
% 0.19/0.56 tptp_fun__phi__: |'A_ltln$'|)).
% 0.19/0.56 tff(tptp_fun__subformulas_nu___type, type, (
% 0.19/0.56 tptp_fun__subformulas_nu__: |'A_ltln_a_ltln_set_fun$'|)).
% 0.19/0.56 tff(tptp_fun__fun_app_g__type, type, (
% 0.19/0.56 tptp_fun__fun_app_g_: ( |'A_ltln_set_a_ltln_set_bool_fun_fun$'| * |'A_ltln_set$'| ) > |'A_ltln_set_bool_fun$'|)).
% 0.19/0.56 tff(tptp_fun__less_eq___type, type, (
% 0.19/0.56 tptp_fun__less_eq__: |'A_ltln_set_a_ltln_set_bool_fun_fun$'|)).
% 0.19/0.56 tff(tptp_fun__subformulas_mu___type, type, (
% 0.19/0.56 tptp_fun__subformulas_mu__: |'A_ltln_a_ltln_set_fun$'|)).
% 0.19/0.56 tff(1,plain,
% 0.19/0.56 (^[A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : refl((~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))))) <=> (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))))))),
% 0.19/0.56 inference(bind,[status(th)],[])).
% 0.19/0.56 tff(2,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))))) <=> ![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))),
% 0.19/0.56 inference(quant_intro,[status(thm)],[1])).
% 0.19/0.56 tff(3,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))))) <=> ![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))),
% 0.19/0.56 inference(rewrite,[status(thm)],[])).
% 0.19/0.56 tff(4,plain,
% 0.19/0.56 (^[A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : trans(trans(monotonicity(rewrite(((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))), (((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))), rewrite(((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))) <=> (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))), (((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))) <=> (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))))))), rewrite((~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))))) <=> (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))), (((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))) <=> (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))))),
% 0.19/0.56 inference(bind,[status(th)],[])).
% 0.19/0.56 tff(5,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))) <=> ![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))),
% 0.19/0.56 inference(quant_intro,[status(thm)],[4])).
% 0.19/0.56 tff(6,axiom,(![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom64')).
% 0.19/0.56 tff(7,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))),
% 0.19/0.56 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.19/0.56 tff(8,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))),
% 0.19/0.56 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.19/0.56 tff(9,plain,(
% 0.19/0.56 ![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))),
% 0.19/0.56 inference(skolemize,[status(sab)],[8])).
% 0.19/0.56 tff(10,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))),
% 0.19/0.56 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.19/0.56 tff(11,plain,
% 0.19/0.56 ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, A__questionmark_v0), A__questionmark_v1)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))))) | (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, |'x$'|), |'y$'|)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)) | (~tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)))))),
% 0.19/0.56 inference(quant_inst,[status(thm)],[])).
% 0.19/0.56 tff(12,plain,
% 0.19/0.56 (~(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, |'x$'|), |'y$'|)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)) | (~tptp_fun__fun_app_a_(|'finite$'|, |'y$'|))))),
% 0.19/0.56 inference(unit_resolution,[status(thm)],[11, 10])).
% 0.19/0.56 tff(13,plain,
% 0.19/0.56 ((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, |'x$'|), |'y$'|))) <=> (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, |'x$'|), |'y$'|)))),
% 0.19/0.56 inference(rewrite,[status(thm)],[])).
% 0.19/0.56 tff(14,axiom,(~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, |'x$'|), |'y$'|))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','conjecture2')).
% 0.19/0.56 tff(15,plain,
% 0.19/0.56 (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, |'x$'|), |'y$'|))),
% 0.19/0.56 inference(modus_ponens,[status(thm)],[14, 13])).
% 0.19/0.56 tff(16,plain,
% 0.19/0.56 ((tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, |'x$'|), |'y$'|)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)) | (~tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)))) | tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, |'x$'|), |'y$'|)) | ((~tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)) | (~tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)))),
% 0.19/0.56 inference(tautology,[status(thm)],[])).
% 0.19/0.56 tff(17,plain,
% 0.19/0.56 ((tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_c_(tptp_fun__fun_app_d_(|'sup$'|, |'x$'|), |'y$'|)) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)) | (~tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)))) | ((~tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)) | (~tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)))),
% 0.19/0.56 inference(unit_resolution,[status(thm)],[16, 15])).
% 0.19/0.56 tff(18,plain,
% 0.19/0.56 ((~tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)) | (~tptp_fun__fun_app_a_(|'finite$'|, |'y$'|))),
% 0.19/0.56 inference(unit_resolution,[status(thm)],[17, 12])).
% 0.19/0.56 tff(19,plain,
% 0.19/0.56 (^[A__questionmark_v0: |'A_ltln$'|] : refl(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0)) <=> tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0)))),
% 0.19/0.56 inference(bind,[status(th)],[])).
% 0.19/0.56 tff(20,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0)) <=> ![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0))),
% 0.19/0.56 inference(quant_intro,[status(thm)],[19])).
% 0.19/0.56 tff(21,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0)) <=> ![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0))),
% 0.19/0.56 inference(rewrite,[status(thm)],[])).
% 0.19/0.56 tff(22,axiom,(![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom288')).
% 0.19/0.56 tff(23,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0))),
% 0.19/0.56 inference(modus_ponens,[status(thm)],[22, 21])).
% 0.19/0.56 tff(24,plain,(
% 0.19/0.56 ![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0))),
% 0.19/0.56 inference(skolemize,[status(sab)],[23])).
% 0.19/0.56 tff(25,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0))),
% 0.19/0.56 inference(modus_ponens,[status(thm)],[24, 20])).
% 0.19/0.56 tff(26,plain,
% 0.19/0.56 ((~![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))),
% 0.19/0.56 inference(quant_inst,[status(thm)],[])).
% 0.19/0.56 tff(27,plain,
% 0.19/0.56 (tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))),
% 0.19/0.56 inference(unit_resolution,[status(thm)],[26, 25])).
% 0.19/0.56 tff(28,plain,
% 0.19/0.56 (^[A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : refl((tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) <=> (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))))),
% 0.19/0.56 inference(bind,[status(th)],[])).
% 0.19/0.56 tff(29,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) <=> ![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))),
% 0.19/0.56 inference(quant_intro,[status(thm)],[28])).
% 0.19/0.56 tff(30,plain,
% 0.19/0.56 (^[A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : trans(monotonicity(trans(monotonicity(rewrite((tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)) <=> (~((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))))), ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) <=> (~(~((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))))))), rewrite((~(~((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))), ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) <=> ((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))))), (((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)) <=> (((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))), rewrite((((~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)) <=> (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))), (((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)) <=> (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))))),
% 0.19/0.56 inference(bind,[status(th)],[])).
% 0.19/0.56 tff(31,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)) <=> ![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))),
% 0.19/0.56 inference(quant_intro,[status(thm)],[30])).
% 0.19/0.56 tff(32,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)) <=> ![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))),
% 0.19/0.56 inference(rewrite,[status(thm)],[])).
% 0.19/0.56 tff(33,plain,
% 0.19/0.56 (^[A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : rewrite(((tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)) => tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)) <=> ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)))),
% 0.19/0.56 inference(bind,[status(th)],[])).
% 0.19/0.56 tff(34,plain,
% 0.19/0.56 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)) => tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1)) <=> ![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))),
% 0.19/0.57 inference(quant_intro,[status(thm)],[33])).
% 0.19/0.57 tff(35,axiom,(![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)) => tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom262')).
% 0.19/0.57 tff(36,plain,
% 0.19/0.57 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))),
% 0.19/0.57 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.19/0.57 tff(37,plain,
% 0.19/0.57 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))),
% 0.19/0.57 inference(modus_ponens,[status(thm)],[36, 32])).
% 0.19/0.57 tff(38,plain,(
% 0.19/0.57 ![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : ((~(tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0) & tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1))),
% 0.19/0.57 inference(skolemize,[status(sab)],[37])).
% 0.19/0.57 tff(39,plain,
% 0.19/0.57 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))),
% 0.19/0.57 inference(modus_ponens,[status(thm)],[38, 31])).
% 0.19/0.57 tff(40,plain,
% 0.19/0.57 (![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))),
% 0.19/0.57 inference(modus_ponens,[status(thm)],[39, 29])).
% 0.19/0.57 tff(41,plain,
% 0.19/0.57 (tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|)) <=> tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))),
% 0.19/0.57 inference(rewrite,[status(thm)],[])).
% 0.19/0.57 tff(42,axiom,(tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom69')).
% 0.19/0.57 tff(43,plain,
% 0.19/0.57 (tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))),
% 0.19/0.57 inference(modus_ponens,[status(thm)],[42, 41])).
% 0.19/0.57 tff(44,plain,
% 0.19/0.57 (((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | ((~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'y$'|))) <=> ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'y$'|))),
% 0.19/0.57 inference(rewrite,[status(thm)],[])).
% 0.19/0.57 tff(45,plain,
% 0.19/0.57 ((tptp_fun__fun_app_a_(|'finite$'|, |'y$'|) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|)))) <=> ((~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'y$'|))),
% 0.19/0.57 inference(rewrite,[status(thm)],[])).
% 0.19/0.57 tff(46,plain,
% 0.19/0.57 (((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (tptp_fun__fun_app_a_(|'finite$'|, |'y$'|) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))))) <=> ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | ((~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)))),
% 0.19/0.57 inference(monotonicity,[status(thm)],[45])).
% 0.19/0.57 tff(47,plain,
% 0.19/0.57 (((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (tptp_fun__fun_app_a_(|'finite$'|, |'y$'|) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))))) <=> ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'y$'|))),
% 0.19/0.57 inference(transitivity,[status(thm)],[46, 44])).
% 0.19/0.57 tff(48,plain,
% 0.19/0.57 ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (tptp_fun__fun_app_a_(|'finite$'|, |'y$'|) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))))),
% 0.19/0.57 inference(quant_inst,[status(thm)],[])).
% 0.19/0.57 tff(49,plain,
% 0.19/0.57 ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'y$'|), tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)),
% 0.19/0.57 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.19/0.57 tff(50,plain,
% 0.19/0.57 ((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_nu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)),
% 0.19/0.57 inference(unit_resolution,[status(thm)],[49, 43, 40])).
% 0.19/0.57 tff(51,plain,
% 0.19/0.57 (tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)),
% 0.19/0.57 inference(unit_resolution,[status(thm)],[50, 27])).
% 0.19/0.57 tff(52,plain,
% 0.19/0.57 (^[A__questionmark_v0: |'A_ltln$'|] : refl(tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0)) <=> tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0)))),
% 0.19/0.57 inference(bind,[status(th)],[])).
% 0.19/0.57 tff(53,plain,
% 0.19/0.57 (![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0)) <=> ![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0))),
% 0.19/0.57 inference(quant_intro,[status(thm)],[52])).
% 0.19/0.57 tff(54,plain,
% 0.19/0.57 (![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0)) <=> ![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0))),
% 0.19/0.57 inference(rewrite,[status(thm)],[])).
% 0.19/0.57 tff(55,axiom,(![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom287')).
% 0.19/0.57 tff(56,plain,
% 0.19/0.57 (![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0))),
% 0.19/0.57 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.19/0.57 tff(57,plain,(
% 0.19/0.57 ![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0))),
% 0.19/0.57 inference(skolemize,[status(sab)],[56])).
% 0.19/0.57 tff(58,plain,
% 0.19/0.57 (![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0))),
% 0.19/0.57 inference(modus_ponens,[status(thm)],[57, 53])).
% 0.19/0.57 tff(59,plain,
% 0.19/0.57 ((~![A__questionmark_v0: |'A_ltln$'|] : tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, A__questionmark_v0))) | tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))),
% 0.19/0.57 inference(quant_inst,[status(thm)],[])).
% 0.19/0.57 tff(60,plain,
% 0.19/0.57 (tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))),
% 0.19/0.57 inference(unit_resolution,[status(thm)],[59, 58])).
% 0.19/0.57 tff(61,plain,
% 0.19/0.57 (tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|)) <=> tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))),
% 0.19/0.57 inference(rewrite,[status(thm)],[])).
% 0.19/0.57 tff(62,axiom,(tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom70')).
% 0.19/0.57 tff(63,plain,
% 0.19/0.57 (tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))),
% 0.19/0.57 inference(modus_ponens,[status(thm)],[62, 61])).
% 0.19/0.57 tff(64,plain,
% 0.19/0.57 (((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | ((~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'x$'|))) <=> ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'x$'|))),
% 0.19/0.57 inference(rewrite,[status(thm)],[])).
% 0.19/0.57 tff(65,plain,
% 0.19/0.57 ((tptp_fun__fun_app_a_(|'finite$'|, |'x$'|) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|)))) <=> ((~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'x$'|))),
% 0.19/0.57 inference(rewrite,[status(thm)],[])).
% 0.19/0.57 tff(66,plain,
% 0.19/0.57 (((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (tptp_fun__fun_app_a_(|'finite$'|, |'x$'|) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))))) <=> ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | ((~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)))),
% 0.19/0.57 inference(monotonicity,[status(thm)],[65])).
% 0.19/0.57 tff(67,plain,
% 0.19/0.57 (((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (tptp_fun__fun_app_a_(|'finite$'|, |'x$'|) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))))) <=> ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'x$'|))),
% 0.19/0.57 inference(transitivity,[status(thm)],[66, 64])).
% 0.19/0.57 tff(68,plain,
% 0.19/0.57 ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (tptp_fun__fun_app_a_(|'finite$'|, |'x$'|) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))))),
% 0.44/0.60 inference(quant_inst,[status(thm)],[])).
% 0.44/0.60 tff(69,plain,
% 0.44/0.60 ((~![A__questionmark_v0: |'A_ltln_set$'|, A__questionmark_v1: |'A_ltln_set$'|] : (tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v1) | (~tptp_fun__fun_app_a_(|'finite$'|, A__questionmark_v0)) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, A__questionmark_v1), A__questionmark_v0)))) | (~tptp_fun__fun_app_a_(tptp_fun__fun_app_g_(|'less_eq$'|, |'x$'|), tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | (~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[68, 67])).
% 0.44/0.60 tff(70,plain,
% 0.44/0.60 ((~tptp_fun__fun_app_a_(|'finite$'|, tptp_fun__fun_app_h_(|'subformulas_mu$'|, |'phi$'|))) | tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[69, 63, 40])).
% 0.44/0.60 tff(71,plain,
% 0.44/0.60 (tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[70, 60])).
% 0.44/0.60 tff(72,plain,
% 0.44/0.60 ((~((~tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)) | (~tptp_fun__fun_app_a_(|'finite$'|, |'y$'|)))) | (~tptp_fun__fun_app_a_(|'finite$'|, |'x$'|)) | (~tptp_fun__fun_app_a_(|'finite$'|, |'y$'|))),
% 0.44/0.60 inference(tautology,[status(thm)],[])).
% 0.44/0.60 tff(73,plain,
% 0.44/0.60 ($false),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[72, 71, 51, 18])).
% 0.44/0.60 % SZS output end Proof
% 0.44/0.61 % E exiting
%------------------------------------------------------------------------------