%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM218_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.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 : Tue May 5 06:23:01 PM UTC 2026
% Result : Theorem 0.27s 0.46s
% Output : Proof 0.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : COM218_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : run_E %s %d THM
% 0.13/0.33 % Computer : n009.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon May 4 19:00:28 EDT 2026
% 0.13/0.34 % CPUTime :
% 0.27/0.46 % SZS status Theorem
% 0.27/0.46 % SZS output start Proof
% 0.27/0.46 tff(vptchecksimple_type, type, (
% 0.27/0.46 vptchecksimple: ( vTerm * vTy ) > $o)).
% 0.27/0.46 tff(vB_type, type, (
% 0.27/0.46 vB: vTy)).
% 0.27/0.46 tff(tptp_fun_VwildcardName0_12_type, type, (
% 0.27/0.46 tptp_fun_VwildcardName0_12: vOptTerm > vTerm)).
% 0.27/0.46 tff(vreduce_type, type, (
% 0.27/0.46 vreduce: vTerm > vOptTerm)).
% 0.27/0.46 tff(vt1_type, type, (
% 0.27/0.46 vt1: vTerm)).
% 0.27/0.46 tff(tptp_fun_VT_63_type, type, (
% 0.27/0.46 tptp_fun_VT_63: vTy)).
% 0.27/0.46 tff(vIfelse_type, type, (
% 0.27/0.46 vIfelse: ( vTerm * vTerm * vTerm ) > vTerm)).
% 0.27/0.46 tff(vt3_type, type, (
% 0.27/0.46 vt3: vTerm)).
% 0.27/0.46 tff(vt2_type, type, (
% 0.27/0.46 vt2: vTerm)).
% 0.27/0.46 tff(tptp_fun_Vtres_62_type, type, (
% 0.27/0.46 tptp_fun_Vtres_62: vTerm)).
% 0.27/0.46 tff(vgetTerm_type, type, (
% 0.27/0.46 vgetTerm: vOptTerm > vTerm)).
% 0.27/0.46 tff(vsomeTerm_type, type, (
% 0.27/0.46 vsomeTerm: vTerm > vOptTerm)).
% 0.27/0.46 tff(vFalse_type, type, (
% 0.27/0.46 vFalse: vTerm)).
% 0.27/0.46 tff(vTrue_type, type, (
% 0.27/0.46 vTrue: vTerm)).
% 0.27/0.46 tff(visSomeTerm_type, type, (
% 0.27/0.46 visSomeTerm: vOptTerm > $o)).
% 0.27/0.46 tff(1,plain,
% 0.27/0.46 (![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt) <=> ![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt)),
% 0.27/0.46 inference(rewrite,[status(thm)],[])).
% 0.27/0.46 tff(2,plain,
% 0.27/0.46 (![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt) <=> ![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt)),
% 0.27/0.46 inference(rewrite,[status(thm)],[])).
% 0.27/0.46 tff(3,axiom,(![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''getTerm-0'')).
% 0.27/0.46 tff(4,plain,
% 0.27/0.46 (![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt)),
% 0.27/0.46 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.27/0.46 tff(5,plain,(
% 0.27/0.46 ![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt)),
% 0.27/0.46 inference(skolemize,[status(sab)],[4])).
% 0.27/0.46 tff(6,plain,
% 0.27/0.46 (![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt)),
% 0.27/0.46 inference(modus_ponens,[status(thm)],[5, 1])).
% 0.27/0.46 tff(7,plain,
% 0.27/0.46 ((~![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt)) | (vgetTerm(vsomeTerm(Vtres!62)) = Vtres!62)),
% 0.27/0.46 inference(quant_inst,[status(thm)],[])).
% 0.27/0.46 tff(8,plain,
% 0.27/0.46 (vgetTerm(vsomeTerm(Vtres!62)) = Vtres!62),
% 0.27/0.46 inference(unit_resolution,[status(thm)],[7, 6])).
% 0.27/0.46 tff(9,plain,
% 0.27/0.46 ((~![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue)) & (~(vt1 = vFalse)) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))) <=> (~![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue)) & (~(vt1 = vFalse)) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)))),
% 0.27/0.46 inference(rewrite,[status(thm)],[])).
% 0.27/0.46 tff(10,plain,
% 0.27/0.46 ((~![VT: vTy, Vtres: vTerm] : (((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue))) & (~(vt1 = vFalse))) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT)) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT))) <=> (~![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue)) & (~(vt1 = vFalse)) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)))),
% 0.27/0.46 inference(rewrite,[status(thm)],[])).
% 0.27/0.46 tff(11,axiom,(~![VT: vTy, Vtres: vTerm] : (((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue))) & (~(vt1 = vFalse))) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT)) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''Preservation-Ifelse-t1-isSomeTerm-True'')).
% 0.27/0.46 tff(12,plain,
% 0.27/0.46 (~![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue)) & (~(vt1 = vFalse)) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 0.27/0.46 inference(modus_ponens,[status(thm)],[11, 10])).
% 0.27/0.46 tff(13,plain,
% 0.27/0.46 (~![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue)) & (~(vt1 = vFalse)) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 0.27/0.46 inference(modus_ponens,[status(thm)],[12, 9])).
% 0.27/0.46 tff(14,plain,
% 0.27/0.46 (~![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue)) & (~(vt1 = vFalse)) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[13, 9])).
% 0.27/0.47 tff(15,plain,
% 0.27/0.47 (~![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue)) & (~(vt1 = vFalse)) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[14, 9])).
% 0.27/0.47 tff(16,plain,(
% 0.27/0.47 ~((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue)) & (~(vt1 = vFalse)) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres!62)))) | vptchecksimple(Vtres!62, VT!63))),
% 0.27/0.47 inference(skolemize,[status(sab)],[15])).
% 0.27/0.47 tff(17,plain,
% 0.27/0.47 (visSomeTerm(vreduce(vt1)) & (~(vt1 = vTrue)) & (~(vt1 = vFalse)) & vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63) & (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres!62))),
% 0.27/0.47 inference(or_elim,[status(thm)],[16])).
% 0.27/0.47 tff(18,plain,
% 0.27/0.47 (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(Vtres!62)),
% 0.27/0.47 inference(and_elim,[status(thm)],[17])).
% 0.27/0.47 tff(19,plain,
% 0.27/0.47 (~(vt1 = vFalse)),
% 0.27/0.47 inference(and_elim,[status(thm)],[17])).
% 0.27/0.47 tff(20,plain,
% 0.27/0.47 (~(vt1 = vTrue)),
% 0.27/0.47 inference(and_elim,[status(thm)],[17])).
% 0.27/0.47 tff(21,plain,
% 0.27/0.47 (visSomeTerm(vreduce(vt1))),
% 0.27/0.47 inference(and_elim,[status(thm)],[17])).
% 0.27/0.47 tff(22,plain,
% 0.27/0.47 (^[Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : refl(((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse)) <=> ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse)))),
% 0.27/0.47 inference(bind,[status(th)],[])).
% 0.27/0.47 tff(23,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))),
% 0.27/0.47 inference(quant_intro,[status(thm)],[22])).
% 0.27/0.47 tff(24,plain,
% 0.27/0.47 (^[Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : trans(monotonicity(trans(monotonicity(rewrite(((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1))) <=> (~((~visSomeTerm(vreduce(Vt1))) | (Vt1 = vTrue) | (Vt1 = vFalse)))), ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) <=> (~(~((~visSomeTerm(vreduce(Vt1))) | (Vt1 = vTrue) | (Vt1 = vFalse)))))), rewrite((~(~((~visSomeTerm(vreduce(Vt1))) | (Vt1 = vTrue) | (Vt1 = vFalse)))) <=> ((~visSomeTerm(vreduce(Vt1))) | (Vt1 = vTrue) | (Vt1 = vFalse))), ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) <=> ((~visSomeTerm(vreduce(Vt1))) | (Vt1 = vTrue) | (Vt1 = vFalse)))), (((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))) <=> (((~visSomeTerm(vreduce(Vt1))) | (Vt1 = vTrue) | (Vt1 = vFalse)) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))))), rewrite((((~visSomeTerm(vreduce(Vt1))) | (Vt1 = vTrue) | (Vt1 = vFalse)) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))) <=> ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))), (((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))) <=> ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))))),
% 0.27/0.47 inference(bind,[status(th)],[])).
% 0.27/0.47 tff(25,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))),
% 0.27/0.47 inference(quant_intro,[status(thm)],[24])).
% 0.27/0.47 tff(26,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))))),
% 0.27/0.47 inference(rewrite,[status(thm)],[])).
% 0.27/0.47 tff(27,plain,
% 0.27/0.47 (^[Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : trans(monotonicity(trans(monotonicity(rewrite((![Vt200: vTerm, Vt300: vTerm] : (((~(Vt1 = vTrue)) | (~(Vt2 = Vt200))) | (~(Vt3 = Vt300))) & ![Vt201: vTerm, Vt301: vTerm] : (((~(Vt1 = vFalse)) | (~(Vt2 = Vt201))) | (~(Vt3 = Vt301)))) <=> ((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)))), (((![Vt200: vTerm, Vt300: vTerm] : (((~(Vt1 = vTrue)) | (~(Vt2 = Vt200))) | (~(Vt3 = Vt300))) & ![Vt201: vTerm, Vt301: vTerm] : (((~(Vt1 = vFalse)) | (~(Vt2 = Vt201))) | (~(Vt3 = Vt301)))) & visSomeTerm(vreduce(Vt1))) <=> (((~(Vt1 = vTrue)) & (~(Vt1 = vFalse))) & visSomeTerm(vreduce(Vt1))))), rewrite((((~(Vt1 = vTrue)) & (~(Vt1 = vFalse))) & visSomeTerm(vreduce(Vt1))) <=> ((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))), (((![Vt200: vTerm, Vt300: vTerm] : (((~(Vt1 = vTrue)) | (~(Vt2 = Vt200))) | (~(Vt3 = Vt300))) & ![Vt201: vTerm, Vt301: vTerm] : (((~(Vt1 = vFalse)) | (~(Vt2 = Vt201))) | (~(Vt3 = Vt301)))) & visSomeTerm(vreduce(Vt1))) <=> ((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1))))), ((((![Vt200: vTerm, Vt300: vTerm] : (((~(Vt1 = vTrue)) | (~(Vt2 = Vt200))) | (~(Vt3 = Vt300))) & ![Vt201: vTerm, Vt301: vTerm] : (((~(Vt1 = vFalse)) | (~(Vt2 = Vt201))) | (~(Vt3 = Vt301)))) & visSomeTerm(vreduce(Vt1))) => (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))) <=> (((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1))) => (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))))), rewrite((((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1))) => (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))) <=> ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))))), ((((![Vt200: vTerm, Vt300: vTerm] : (((~(Vt1 = vTrue)) | (~(Vt2 = Vt200))) | (~(Vt3 = Vt300))) & ![Vt201: vTerm, Vt301: vTerm] : (((~(Vt1 = vFalse)) | (~(Vt2 = Vt201))) | (~(Vt3 = Vt301)))) & visSomeTerm(vreduce(Vt1))) => (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))) <=> ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))))))),
% 0.27/0.47 inference(bind,[status(th)],[])).
% 0.27/0.47 tff(28,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : (((![Vt200: vTerm, Vt300: vTerm] : (((~(Vt1 = vTrue)) | (~(Vt2 = Vt200))) | (~(Vt3 = Vt300))) & ![Vt201: vTerm, Vt301: vTerm] : (((~(Vt1 = vFalse)) | (~(Vt2 = Vt201))) | (~(Vt3 = Vt301)))) & visSomeTerm(vreduce(Vt1))) => (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3)))) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))))),
% 0.27/0.47 inference(quant_intro,[status(thm)],[27])).
% 0.27/0.47 tff(29,axiom,(![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : (((![Vt200: vTerm, Vt300: vTerm] : (((~(Vt1 = vTrue)) | (~(Vt2 = Vt200))) | (~(Vt3 = Vt300))) & ![Vt201: vTerm, Vt301: vTerm] : (((~(Vt1 = vFalse)) | (~(Vt2 = Vt201))) | (~(Vt3 = Vt301)))) & visSomeTerm(vreduce(Vt1))) => (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''reduce-2'')).
% 0.27/0.47 tff(30,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[29, 28])).
% 0.27/0.47 tff(31,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[30, 26])).
% 0.27/0.47 tff(32,plain,(
% 0.27/0.47 ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~((~(Vt1 = vTrue)) & (~(Vt1 = vFalse)) & visSomeTerm(vreduce(Vt1)))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))))),
% 0.27/0.47 inference(skolemize,[status(sab)],[31])).
% 0.27/0.47 tff(33,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[32, 25])).
% 0.27/0.47 tff(34,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[33, 23])).
% 0.27/0.47 tff(35,plain,
% 0.27/0.47 (((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))) | ((vt1 = vFalse) | (vt1 = vTrue) | (~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))))) <=> ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))) | (vt1 = vFalse) | (vt1 = vTrue) | (~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))))),
% 0.27/0.47 inference(rewrite,[status(thm)],[])).
% 0.27/0.47 tff(36,plain,
% 0.27/0.47 (((~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))) | (vt1 = vTrue) | (vt1 = vFalse)) <=> ((vt1 = vFalse) | (vt1 = vTrue) | (~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))))),
% 0.27/0.47 inference(rewrite,[status(thm)],[])).
% 0.27/0.47 tff(37,plain,
% 0.27/0.47 (((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))) | ((~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))) | (vt1 = vTrue) | (vt1 = vFalse))) <=> ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))) | ((vt1 = vFalse) | (vt1 = vTrue) | (~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3)))))),
% 0.27/0.47 inference(monotonicity,[status(thm)],[36])).
% 0.27/0.47 tff(38,plain,
% 0.27/0.47 (((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))) | ((~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))) | (vt1 = vTrue) | (vt1 = vFalse))) <=> ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))) | (vt1 = vFalse) | (vt1 = vTrue) | (~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))))),
% 0.27/0.47 inference(transitivity,[status(thm)],[37, 35])).
% 0.27/0.47 tff(39,plain,
% 0.27/0.47 ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))) | ((~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))) | (vt1 = vTrue) | (vt1 = vFalse))),
% 0.27/0.47 inference(quant_inst,[status(thm)],[])).
% 0.27/0.47 tff(40,plain,
% 0.27/0.47 ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm] : ((~visSomeTerm(vreduce(Vt1))) | (vreduce(vIfelse(Vt1, Vt2, Vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(Vt1)), Vt2, Vt3))) | (Vt1 = vTrue) | (Vt1 = vFalse))) | (vt1 = vFalse) | (vt1 = vTrue) | (~visSomeTerm(vreduce(vt1))) | (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3)))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[39, 38])).
% 0.27/0.47 tff(41,plain,
% 0.27/0.47 (vreduce(vIfelse(vt1, vt2, vt3)) = vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))),
% 0.27/0.47 inference(unit_resolution,[status(thm)],[40, 34, 21, 20, 19])).
% 0.27/0.47 tff(42,plain,
% 0.27/0.47 (vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3)) = vreduce(vIfelse(vt1, vt2, vt3))),
% 0.27/0.47 inference(symmetry,[status(thm)],[41])).
% 0.27/0.47 tff(43,plain,
% 0.27/0.47 (vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3)) = vsomeTerm(Vtres!62)),
% 0.27/0.47 inference(transitivity,[status(thm)],[42, 18])).
% 0.27/0.47 tff(44,plain,
% 0.27/0.47 (vgetTerm(vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))) = vgetTerm(vsomeTerm(Vtres!62))),
% 0.27/0.47 inference(monotonicity,[status(thm)],[43])).
% 0.27/0.47 tff(45,plain,
% 0.27/0.47 ((~![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt)) | (vgetTerm(vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))) = vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))),
% 0.27/0.47 inference(quant_inst,[status(thm)],[])).
% 0.27/0.47 tff(46,plain,
% 0.27/0.47 (vgetTerm(vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3))) = vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3)),
% 0.27/0.47 inference(unit_resolution,[status(thm)],[45, 6])).
% 0.27/0.47 tff(47,plain,
% 0.27/0.47 (vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3) = vgetTerm(vsomeTerm(vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3)))),
% 0.27/0.47 inference(symmetry,[status(thm)],[46])).
% 0.27/0.47 tff(48,plain,
% 0.27/0.47 (^[VOptTerm0: vOptTerm] : refl(((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0)))) <=> ((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0)))))),
% 0.27/0.47 inference(bind,[status(th)],[])).
% 0.27/0.47 tff(49,plain,
% 0.27/0.47 (![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0)))) <=> ![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0))))),
% 0.27/0.47 inference(quant_intro,[status(thm)],[48])).
% 0.27/0.47 tff(50,plain,
% 0.27/0.47 (![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | ?[VwildcardName0: vTerm] : (VOptTerm0 = vsomeTerm(VwildcardName0))) <=> ![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | ?[VwildcardName0: vTerm] : (VOptTerm0 = vsomeTerm(VwildcardName0)))),
% 0.27/0.47 inference(rewrite,[status(thm)],[])).
% 0.27/0.47 tff(51,plain,
% 0.27/0.47 (^[VOptTerm0: vOptTerm] : rewrite((visSomeTerm(VOptTerm0) => ?[VwildcardName0: vTerm] : (VOptTerm0 = vsomeTerm(VwildcardName0))) <=> ((~visSomeTerm(VOptTerm0)) | ?[VwildcardName0: vTerm] : (VOptTerm0 = vsomeTerm(VwildcardName0))))),
% 0.27/0.47 inference(bind,[status(th)],[])).
% 0.27/0.47 tff(52,plain,
% 0.27/0.47 (![VOptTerm0: vOptTerm] : (visSomeTerm(VOptTerm0) => ?[VwildcardName0: vTerm] : (VOptTerm0 = vsomeTerm(VwildcardName0))) <=> ![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | ?[VwildcardName0: vTerm] : (VOptTerm0 = vsomeTerm(VwildcardName0)))),
% 0.27/0.47 inference(quant_intro,[status(thm)],[51])).
% 0.27/0.47 tff(53,axiom,(![VOptTerm0: vOptTerm] : (visSomeTerm(VOptTerm0) => ?[VwildcardName0: vTerm] : (VOptTerm0 = vsomeTerm(VwildcardName0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''isSomeTerm-true-INV'')).
% 0.27/0.47 tff(54,plain,
% 0.27/0.47 (![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | ?[VwildcardName0: vTerm] : (VOptTerm0 = vsomeTerm(VwildcardName0)))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[53, 52])).
% 0.27/0.47 tff(55,plain,
% 0.27/0.47 (![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | ?[VwildcardName0: vTerm] : (VOptTerm0 = vsomeTerm(VwildcardName0)))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[54, 50])).
% 0.27/0.47 tff(56,plain,(
% 0.27/0.47 ![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0))))),
% 0.27/0.47 inference(skolemize,[status(sab)],[55])).
% 0.27/0.47 tff(57,plain,
% 0.27/0.47 (![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0))))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[56, 49])).
% 0.27/0.47 tff(58,plain,
% 0.27/0.47 (((~![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0))))) | ((~visSomeTerm(vreduce(vt1))) | (vreduce(vt1) = vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1)))))) <=> ((~![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0))))) | (~visSomeTerm(vreduce(vt1))) | (vreduce(vt1) = vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1)))))),
% 0.27/0.47 inference(rewrite,[status(thm)],[])).
% 0.27/0.47 tff(59,plain,
% 0.27/0.47 ((~![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0))))) | ((~visSomeTerm(vreduce(vt1))) | (vreduce(vt1) = vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1)))))),
% 0.27/0.47 inference(quant_inst,[status(thm)],[])).
% 0.27/0.47 tff(60,plain,
% 0.27/0.47 ((~![VOptTerm0: vOptTerm] : ((~visSomeTerm(VOptTerm0)) | (VOptTerm0 = vsomeTerm(tptp_fun_VwildcardName0_12(VOptTerm0))))) | (~visSomeTerm(vreduce(vt1))) | (vreduce(vt1) = vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1))))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[59, 58])).
% 0.27/0.47 tff(61,plain,
% 0.27/0.47 (vreduce(vt1) = vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1)))),
% 0.27/0.47 inference(unit_resolution,[status(thm)],[60, 57, 21])).
% 0.27/0.47 tff(62,plain,
% 0.27/0.47 (vgetTerm(vreduce(vt1)) = vgetTerm(vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1))))),
% 0.27/0.47 inference(monotonicity,[status(thm)],[61])).
% 0.27/0.47 tff(63,plain,
% 0.27/0.47 (vgetTerm(vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1)))) = vgetTerm(vreduce(vt1))),
% 0.27/0.47 inference(symmetry,[status(thm)],[62])).
% 0.27/0.47 tff(64,plain,
% 0.27/0.47 ((~![Vt: vTerm] : (vgetTerm(vsomeTerm(Vt)) = Vt)) | (vgetTerm(vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1)))) = tptp_fun_VwildcardName0_12(vreduce(vt1)))),
% 0.27/0.47 inference(quant_inst,[status(thm)],[])).
% 0.27/0.47 tff(65,plain,
% 0.27/0.47 (vgetTerm(vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1)))) = tptp_fun_VwildcardName0_12(vreduce(vt1))),
% 0.27/0.47 inference(unit_resolution,[status(thm)],[64, 6])).
% 0.27/0.47 tff(66,plain,
% 0.27/0.47 (tptp_fun_VwildcardName0_12(vreduce(vt1)) = vgetTerm(vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1))))),
% 0.27/0.47 inference(symmetry,[status(thm)],[65])).
% 0.27/0.47 tff(67,plain,
% 0.27/0.47 (tptp_fun_VwildcardName0_12(vreduce(vt1)) = vgetTerm(vreduce(vt1))),
% 0.27/0.47 inference(transitivity,[status(thm)],[66, 63])).
% 0.27/0.47 tff(68,plain,
% 0.27/0.47 (vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3) = vIfelse(vgetTerm(vreduce(vt1)), vt2, vt3)),
% 0.27/0.47 inference(monotonicity,[status(thm)],[67])).
% 0.27/0.47 tff(69,plain,
% 0.27/0.47 (vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3) = Vtres!62),
% 0.27/0.47 inference(transitivity,[status(thm)],[68, 47, 44, 8])).
% 0.27/0.47 tff(70,plain,
% 0.27/0.47 (vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) <=> vptchecksimple(Vtres!62, VT!63)),
% 0.27/0.47 inference(monotonicity,[status(thm)],[69])).
% 0.27/0.47 tff(71,plain,
% 0.27/0.47 (vptchecksimple(Vtres!62, VT!63) <=> vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63)),
% 0.27/0.47 inference(symmetry,[status(thm)],[70])).
% 0.27/0.47 tff(72,plain,
% 0.27/0.47 ((~vptchecksimple(Vtres!62, VT!63)) <=> (~vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63))),
% 0.27/0.47 inference(monotonicity,[status(thm)],[71])).
% 0.27/0.47 tff(73,plain,
% 0.27/0.47 (~vptchecksimple(Vtres!62, VT!63)),
% 0.27/0.47 inference(or_elim,[status(thm)],[16])).
% 0.27/0.47 tff(74,plain,
% 0.27/0.47 (~vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63)),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[73, 72])).
% 0.27/0.47 tff(75,plain,
% 0.27/0.47 (vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)),
% 0.27/0.47 inference(and_elim,[status(thm)],[17])).
% 0.27/0.47 tff(76,plain,
% 0.27/0.47 (^[Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : refl(((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT)) <=> ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT)))),
% 0.27/0.47 inference(bind,[status(th)],[])).
% 0.27/0.47 tff(77,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))),
% 0.27/0.47 inference(quant_intro,[status(thm)],[76])).
% 0.27/0.47 tff(78,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))),
% 0.27/0.47 inference(rewrite,[status(thm)],[])).
% 0.27/0.47 tff(79,plain,
% 0.27/0.47 (^[Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : rewrite((vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) => vptchecksimple(Vt2, VT)) <=> ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT)))),
% 0.27/0.47 inference(bind,[status(th)],[])).
% 0.27/0.47 tff(80,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) => vptchecksimple(Vt2, VT)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))),
% 0.27/0.47 inference(quant_intro,[status(thm)],[79])).
% 0.27/0.47 tff(81,axiom,(![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) => vptchecksimple(Vt2, VT))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''Tif_inv2'')).
% 0.27/0.47 tff(82,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[81, 80])).
% 0.27/0.47 tff(83,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[82, 78])).
% 0.27/0.47 tff(84,plain,(
% 0.27/0.47 ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))),
% 0.27/0.47 inference(skolemize,[status(sab)],[83])).
% 0.27/0.47 tff(85,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[84, 77])).
% 0.27/0.47 tff(86,plain,
% 0.27/0.47 (((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))) | ((~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt2, VT!63))) <=> ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))) | (~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt2, VT!63))),
% 0.27/0.47 inference(rewrite,[status(thm)],[])).
% 0.27/0.47 tff(87,plain,
% 0.27/0.47 ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))) | ((~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt2, VT!63))),
% 0.27/0.47 inference(quant_inst,[status(thm)],[])).
% 0.27/0.47 tff(88,plain,
% 0.27/0.47 ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt2, VT))) | (~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt2, VT!63)),
% 0.27/0.47 inference(modus_ponens,[status(thm)],[87, 86])).
% 0.27/0.47 tff(89,plain,
% 0.27/0.47 (vptchecksimple(vt2, VT!63)),
% 0.27/0.47 inference(unit_resolution,[status(thm)],[88, 85, 75])).
% 0.27/0.47 tff(90,plain,
% 0.27/0.47 (^[Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : refl(((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT)) <=> ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT)))),
% 0.27/0.47 inference(bind,[status(th)],[])).
% 0.27/0.47 tff(91,plain,
% 0.27/0.47 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))),
% 0.27/0.48 inference(quant_intro,[status(thm)],[90])).
% 0.27/0.48 tff(92,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))),
% 0.27/0.48 inference(rewrite,[status(thm)],[])).
% 0.27/0.48 tff(93,plain,
% 0.27/0.48 (^[Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : rewrite((vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) => vptchecksimple(Vt3, VT)) <=> ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT)))),
% 0.27/0.48 inference(bind,[status(th)],[])).
% 0.27/0.48 tff(94,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) => vptchecksimple(Vt3, VT)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))),
% 0.27/0.48 inference(quant_intro,[status(thm)],[93])).
% 0.27/0.48 tff(95,axiom,(![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) => vptchecksimple(Vt3, VT))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''Tif_inv3'')).
% 0.27/0.48 tff(96,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[95, 94])).
% 0.27/0.48 tff(97,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[96, 92])).
% 0.27/0.48 tff(98,plain,(
% 0.27/0.48 ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))),
% 0.27/0.48 inference(skolemize,[status(sab)],[97])).
% 0.27/0.48 tff(99,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[98, 91])).
% 0.27/0.48 tff(100,plain,
% 0.27/0.48 (((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))) | ((~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt3, VT!63))) <=> ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))) | (~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt3, VT!63))),
% 0.27/0.48 inference(rewrite,[status(thm)],[])).
% 0.27/0.48 tff(101,plain,
% 0.27/0.48 ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))) | ((~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt3, VT!63))),
% 0.27/0.48 inference(quant_inst,[status(thm)],[])).
% 0.27/0.48 tff(102,plain,
% 0.27/0.48 ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt3, VT))) | (~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt3, VT!63)),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[101, 100])).
% 0.27/0.48 tff(103,plain,
% 0.27/0.48 (vptchecksimple(vt3, VT!63)),
% 0.27/0.48 inference(unit_resolution,[status(thm)],[102, 99, 75])).
% 0.27/0.48 tff(104,plain,
% 0.27/0.48 (^[Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : refl((vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT))) <=> (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT))))),
% 0.27/0.48 inference(bind,[status(th)],[])).
% 0.27/0.48 tff(105,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT))) <=> ![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))),
% 0.27/0.48 inference(quant_intro,[status(thm)],[104])).
% 0.27/0.48 tff(106,plain,
% 0.27/0.48 (^[Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : trans(monotonicity(trans(monotonicity(rewrite((vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT)) <=> (~((~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT))))), ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) <=> (~(~((~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT))))))), rewrite((~(~((~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT))))) <=> ((~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))), ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) <=> ((~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT))))), (((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) <=> (((~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)))), rewrite((((~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) <=> (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))), (((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) <=> (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))))),
% 0.27/0.48 inference(bind,[status(th)],[])).
% 0.27/0.48 tff(107,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) <=> ![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))),
% 0.27/0.48 inference(quant_intro,[status(thm)],[106])).
% 0.27/0.48 tff(108,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) <=> ![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT))),
% 0.27/0.48 inference(rewrite,[status(thm)],[])).
% 0.27/0.48 tff(109,plain,
% 0.27/0.48 (^[Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : trans(monotonicity(rewrite(((vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT)) & vptchecksimple(Vt3, VT)) <=> (vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))), ((((vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT)) & vptchecksimple(Vt3, VT)) => vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) <=> ((vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT)) => vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)))), rewrite(((vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT)) => vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) <=> ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT))), ((((vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT)) & vptchecksimple(Vt3, VT)) => vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) <=> ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT))))),
% 0.27/0.48 inference(bind,[status(th)],[])).
% 0.27/0.48 tff(110,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (((vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT)) & vptchecksimple(Vt3, VT)) => vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) <=> ![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT))),
% 0.27/0.48 inference(quant_intro,[status(thm)],[109])).
% 0.27/0.48 tff(111,axiom,(![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (((vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT)) & vptchecksimple(Vt3, VT)) => vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''Tif'')).
% 0.27/0.48 tff(112,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[111, 110])).
% 0.27/0.48 tff(113,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[112, 108])).
% 0.27/0.48 tff(114,plain,(
% 0.27/0.48 ![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : ((~(vptchecksimple(Vt1, vB) & vptchecksimple(Vt2, VT) & vptchecksimple(Vt3, VT))) | vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT))),
% 0.27/0.48 inference(skolemize,[status(sab)],[113])).
% 0.27/0.48 tff(115,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[114, 107])).
% 0.27/0.48 tff(116,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[115, 105])).
% 0.27/0.48 tff(117,plain,
% 0.27/0.48 (((~![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))) | ((~vptchecksimple(vt3, VT!63)) | (~vptchecksimple(vt2, VT!63)) | vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB)))) <=> ((~![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))) | (~vptchecksimple(vt3, VT!63)) | (~vptchecksimple(vt2, VT!63)) | vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB)))),
% 0.27/0.48 inference(rewrite,[status(thm)],[])).
% 0.27/0.48 tff(118,plain,
% 0.27/0.48 ((vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB)) | (~vptchecksimple(vt2, VT!63)) | (~vptchecksimple(vt3, VT!63))) <=> ((~vptchecksimple(vt3, VT!63)) | (~vptchecksimple(vt2, VT!63)) | vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB)))),
% 0.27/0.48 inference(rewrite,[status(thm)],[])).
% 0.27/0.48 tff(119,plain,
% 0.27/0.48 (((~![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))) | (vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB)) | (~vptchecksimple(vt2, VT!63)) | (~vptchecksimple(vt3, VT!63)))) <=> ((~![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))) | ((~vptchecksimple(vt3, VT!63)) | (~vptchecksimple(vt2, VT!63)) | vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB))))),
% 0.27/0.48 inference(monotonicity,[status(thm)],[118])).
% 0.27/0.48 tff(120,plain,
% 0.27/0.48 (((~![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))) | (vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB)) | (~vptchecksimple(vt2, VT!63)) | (~vptchecksimple(vt3, VT!63)))) <=> ((~![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))) | (~vptchecksimple(vt3, VT!63)) | (~vptchecksimple(vt2, VT!63)) | vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB)))),
% 0.27/0.48 inference(transitivity,[status(thm)],[119, 117])).
% 0.27/0.48 tff(121,plain,
% 0.27/0.48 ((~![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))) | (vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB)) | (~vptchecksimple(vt2, VT!63)) | (~vptchecksimple(vt3, VT!63)))),
% 0.27/0.48 inference(quant_inst,[status(thm)],[])).
% 0.27/0.48 tff(122,plain,
% 0.27/0.48 ((~![Vt1: vTerm, Vt2: vTerm, VT: vTy, Vt3: vTerm] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) | (~vptchecksimple(Vt1, vB)) | (~vptchecksimple(Vt2, VT)) | (~vptchecksimple(Vt3, VT)))) | (~vptchecksimple(vt3, VT!63)) | (~vptchecksimple(vt2, VT!63)) | vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[121, 120])).
% 0.27/0.48 tff(123,plain,
% 0.27/0.48 (vptchecksimple(vIfelse(tptp_fun_VwildcardName0_12(vreduce(vt1)), vt2, vt3), VT!63) | (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB))),
% 0.27/0.48 inference(unit_resolution,[status(thm)],[122, 116, 103, 89])).
% 0.27/0.48 tff(124,plain,
% 0.27/0.48 (~vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB)),
% 0.27/0.48 inference(unit_resolution,[status(thm)],[123, 74])).
% 0.27/0.48 tff(125,plain,
% 0.27/0.48 (^[Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : refl(((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB)) <=> ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB)))),
% 0.27/0.48 inference(bind,[status(th)],[])).
% 0.27/0.48 tff(126,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))),
% 0.27/0.48 inference(quant_intro,[status(thm)],[125])).
% 0.27/0.48 tff(127,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))),
% 0.27/0.48 inference(rewrite,[status(thm)],[])).
% 0.27/0.48 tff(128,plain,
% 0.27/0.48 (^[Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : rewrite((vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) => vptchecksimple(Vt1, vB)) <=> ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB)))),
% 0.27/0.48 inference(bind,[status(th)],[])).
% 0.27/0.48 tff(129,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) => vptchecksimple(Vt1, vB)) <=> ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))),
% 0.27/0.48 inference(quant_intro,[status(thm)],[128])).
% 0.27/0.48 tff(130,axiom,(![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : (vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT) => vptchecksimple(Vt1, vB))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''Tif_inv1'')).
% 0.27/0.48 tff(131,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[130, 129])).
% 0.27/0.48 tff(132,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[131, 127])).
% 0.27/0.48 tff(133,plain,(
% 0.27/0.48 ![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))),
% 0.27/0.48 inference(skolemize,[status(sab)],[132])).
% 0.27/0.48 tff(134,plain,
% 0.27/0.48 (![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[133, 126])).
% 0.27/0.48 tff(135,plain,
% 0.27/0.48 (((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))) | ((~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt1, vB))) <=> ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))) | (~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt1, vB))),
% 0.27/0.48 inference(rewrite,[status(thm)],[])).
% 0.27/0.48 tff(136,plain,
% 0.27/0.48 ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))) | ((~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt1, vB))),
% 0.27/0.48 inference(quant_inst,[status(thm)],[])).
% 0.27/0.48 tff(137,plain,
% 0.27/0.48 ((~![Vt1: vTerm, Vt2: vTerm, Vt3: vTerm, VT: vTy] : ((~vptchecksimple(vIfelse(Vt1, Vt2, Vt3), VT)) | vptchecksimple(Vt1, vB))) | (~vptchecksimple(vIfelse(vt1, vt2, vt3), VT!63)) | vptchecksimple(vt1, vB)),
% 0.27/0.48 inference(modus_ponens,[status(thm)],[136, 135])).
% 0.27/0.48 tff(138,plain,
% 0.27/0.48 (vptchecksimple(vt1, vB)),
% 0.27/0.48 inference(unit_resolution,[status(thm)],[137, 134, 75])).
% 0.27/0.48 tff(139,plain,
% 0.27/0.48 (^[VT: vTy, Vtres: vTerm] : refl((vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres)))) <=> (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres)))))),
% 0.27/0.48 inference(bind,[status(th)],[])).
% 0.27/0.48 tff(140,plain,
% 0.27/0.48 (![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres)))) <=> ![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))),
% 0.27/0.48 inference(quant_intro,[status(thm)],[139])).
% 0.27/0.48 tff(141,plain,
% 0.27/0.48 (^[VT: vTy, Vtres: vTerm] : trans(monotonicity(trans(monotonicity(rewrite((vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres))) <=> (~((~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres)))))), ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) <=> (~(~((~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres)))))))), rewrite((~(~((~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres)))))) <=> ((~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))), ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) <=> ((~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres)))))), (((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> (((~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)))), rewrite((((~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))), (((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))))),
% 0.27/0.48 inference(bind,[status(th)],[])).
% 0.27/0.48 tff(142,plain,
% 0.27/0.48 (![VT: vTy, Vtres: vTerm] : ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> ![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))),
% 0.27/0.48 inference(quant_intro,[status(thm)],[141])).
% 0.27/0.48 tff(143,plain,
% 0.27/0.48 (![VT: vTy, Vtres: vTerm] : ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> ![VT: vTy, Vtres: vTerm] : ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 0.27/0.48 inference(rewrite,[status(thm)],[])).
% 0.27/0.48 tff(144,plain,
% 0.27/0.48 (^[VT: vTy, Vtres: vTerm] : rewrite(((vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT)) <=> ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)))),
% 0.27/0.49 inference(bind,[status(th)],[])).
% 0.27/0.49 tff(145,plain,
% 0.27/0.49 (![VT: vTy, Vtres: vTerm] : ((vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT)) <=> ![VT: vTy, Vtres: vTerm] : ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 0.27/0.49 inference(quant_intro,[status(thm)],[144])).
% 0.27/0.49 tff(146,axiom,(![VT: vTy, Vtres: vTerm] : ((vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''Preservation-Ifelse-IH0'')).
% 0.27/0.49 tff(147,plain,
% 0.27/0.49 (![VT: vTy, Vtres: vTerm] : ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 0.27/0.49 inference(modus_ponens,[status(thm)],[146, 145])).
% 0.27/0.49 tff(148,plain,
% 0.27/0.49 (![VT: vTy, Vtres: vTerm] : ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 0.27/0.49 inference(modus_ponens,[status(thm)],[147, 143])).
% 0.27/0.49 tff(149,plain,(
% 0.27/0.49 ![VT: vTy, Vtres: vTerm] : ((~(vptchecksimple(vt1, VT) & (vreduce(vt1) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 0.27/0.49 inference(skolemize,[status(sab)],[148])).
% 0.27/0.49 tff(150,plain,
% 0.27/0.49 (![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))),
% 0.27/0.49 inference(modus_ponens,[status(thm)],[149, 142])).
% 0.27/0.49 tff(151,plain,
% 0.27/0.49 (![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))),
% 0.27/0.49 inference(modus_ponens,[status(thm)],[150, 140])).
% 0.27/0.49 tff(152,plain,
% 0.27/0.49 (((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))) | (vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB) | (~vptchecksimple(vt1, vB)) | (~(vreduce(vt1) = vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1))))))) <=> ((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))) | vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB) | (~vptchecksimple(vt1, vB)) | (~(vreduce(vt1) = vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1))))))),
% 0.27/0.49 inference(rewrite,[status(thm)],[])).
% 0.27/0.49 tff(153,plain,
% 0.27/0.49 ((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))) | (vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB) | (~vptchecksimple(vt1, vB)) | (~(vreduce(vt1) = vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1))))))),
% 0.27/0.49 inference(quant_inst,[status(thm)],[])).
% 0.27/0.49 tff(154,plain,
% 0.27/0.49 ((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (~vptchecksimple(vt1, VT)) | (~(vreduce(vt1) = vsomeTerm(Vtres))))) | vptchecksimple(tptp_fun_VwildcardName0_12(vreduce(vt1)), vB) | (~vptchecksimple(vt1, vB)) | (~(vreduce(vt1) = vsomeTerm(tptp_fun_VwildcardName0_12(vreduce(vt1)))))),
% 0.27/0.49 inference(modus_ponens,[status(thm)],[153, 152])).
% 0.27/0.49 tff(155,plain,
% 0.27/0.49 ($false),
% 0.27/0.49 inference(unit_resolution,[status(thm)],[154, 151, 61, 138, 124])).
% 0.27/0.49 % SZS output end Proof
% 0.27/0.49 % E exiting
%------------------------------------------------------------------------------