%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM280_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:06 PM UTC 2026
% Result : Theorem 0.97s 1.14s
% Output : Proof 0.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : COM280_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.11 % Command : run_E %s %d THM
% 0.12/0.32 % Computer : n009.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Mon May 4 20:14:27 EDT 2026
% 0.12/0.32 % CPUTime :
% 0.97/1.14 % SZS status Theorem
% 0.97/1.14 % SZS output start Proof
% 0.97/1.14 tff(vrcons_type, type, (
% 0.97/1.14 vrcons: ( vVal * vRow ) > vRow)).
% 0.97/1.14 tff(tptp_fun_Vr0_63_type, type, (
% 0.97/1.14 tptp_fun_Vr0_63: vRow > vRow)).
% 0.97/1.14 tff(vrempty_type, type, (
% 0.97/1.14 vrempty: vRow)).
% 0.97/1.14 tff(tptp_fun_Vv0_64_type, type, (
% 0.97/1.14 tptp_fun_Vv0_64: vRow > vVal)).
% 0.97/1.14 tff(vttcons_type, type, (
% 0.97/1.14 vttcons: ( vName * vFType * vTType ) > vTType)).
% 0.97/1.14 tff(tptp_fun_Vttr0_65_type, type, (
% 0.97/1.14 tptp_fun_Vttr0_65: vTType > vTType)).
% 0.97/1.14 tff(tptp_fun_Vttrest_307_type, type, (
% 0.97/1.14 tptp_fun_Vttrest_307: vTType)).
% 0.97/1.14 tff(tptp_fun_Vft_308_type, type, (
% 0.97/1.14 tptp_fun_Vft_308: vFType)).
% 0.97/1.14 tff(tptp_fun_Vn_309_type, type, (
% 0.97/1.14 tptp_fun_Vn_309: vName)).
% 0.97/1.14 tff(tptp_fun_Vft0_66_type, type, (
% 0.97/1.14 tptp_fun_Vft0_66: vTType > vFType)).
% 0.97/1.14 tff(tptp_fun_VwildcardName00_67_type, type, (
% 0.97/1.14 tptp_fun_VwildcardName00_67: vTType > vName)).
% 0.97/1.14 tff(vttempty_type, type, (
% 0.97/1.14 vttempty: vTType)).
% 0.97/1.14 tff(vwelltypedRow_type, type, (
% 0.97/1.14 vwelltypedRow: ( vTType * vRow ) > $o)).
% 0.97/1.14 tff(vwelltypedRawtable_type, type, (
% 0.97/1.14 vwelltypedRawtable: ( vTType * vRawTable ) > $o)).
% 0.97/1.14 tff(vrt2_type, type, (
% 0.97/1.14 vrt2: vRawTable)).
% 0.97/1.14 tff(vtcons_type, type, (
% 0.97/1.14 vtcons: ( vRow * vRawTable ) > vRawTable)).
% 0.97/1.14 tff(vdropFirstColRaw_type, type, (
% 0.97/1.14 vdropFirstColRaw: vRawTable > vRawTable)).
% 0.97/1.14 tff(1,plain,
% 0.97/1.14 ((vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) <=> (vttempty = vttcons(Vn!309, Vft!308, Vttrest!307))),
% 0.97/1.14 inference(commutativity,[status(thm)],[])).
% 0.97/1.14 tff(2,plain,
% 0.97/1.14 ((vttempty = vttcons(Vn!309, Vft!308, Vttrest!307)) <=> (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)),
% 0.97/1.14 inference(symmetry,[status(thm)],[1])).
% 0.97/1.14 tff(3,plain,
% 0.97/1.14 ((~(vttempty = vttcons(Vn!309, Vft!308, Vttrest!307))) <=> (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty))),
% 0.97/1.14 inference(monotonicity,[status(thm)],[2])).
% 0.97/1.14 tff(4,plain,
% 0.97/1.14 (^[VName0: vName, VFType0: vFType, VTType0: vTType] : refl((~(vttempty = vttcons(VName0, VFType0, VTType0))) <=> (~(vttempty = vttcons(VName0, VFType0, VTType0))))),
% 0.97/1.14 inference(bind,[status(th)],[])).
% 0.97/1.14 tff(5,plain,
% 0.97/1.14 (![VName0: vName, VFType0: vFType, VTType0: vTType] : (~(vttempty = vttcons(VName0, VFType0, VTType0))) <=> ![VName0: vName, VFType0: vFType, VTType0: vTType] : (~(vttempty = vttcons(VName0, VFType0, VTType0)))),
% 0.97/1.14 inference(quant_intro,[status(thm)],[4])).
% 0.97/1.14 tff(6,plain,
% 0.97/1.14 (![VName0: vName, VFType0: vFType, VTType0: vTType] : (~(vttempty = vttcons(VName0, VFType0, VTType0))) <=> ![VName0: vName, VFType0: vFType, VTType0: vTType] : (~(vttempty = vttcons(VName0, VFType0, VTType0)))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(7,axiom,(![VName0: vName, VFType0: vFType, VTType0: vTType] : (~(vttempty = vttcons(VName0, VFType0, VTType0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''DIFF-ttempty-ttcons'')).
% 0.97/1.14 tff(8,plain,
% 0.97/1.14 (![VName0: vName, VFType0: vFType, VTType0: vTType] : (~(vttempty = vttcons(VName0, VFType0, VTType0)))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[7, 6])).
% 0.97/1.14 tff(9,plain,(
% 0.97/1.14 ![VName0: vName, VFType0: vFType, VTType0: vTType] : (~(vttempty = vttcons(VName0, VFType0, VTType0)))),
% 0.97/1.14 inference(skolemize,[status(sab)],[8])).
% 0.97/1.14 tff(10,plain,
% 0.97/1.14 (![VName0: vName, VFType0: vFType, VTType0: vTType] : (~(vttempty = vttcons(VName0, VFType0, VTType0)))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.97/1.14 tff(11,plain,
% 0.97/1.14 ((~![VName0: vName, VFType0: vFType, VTType0: vTType] : (~(vttempty = vttcons(VName0, VFType0, VTType0)))) | (~(vttempty = vttcons(Vn!309, Vft!308, Vttrest!307)))),
% 0.97/1.14 inference(quant_inst,[status(thm)],[])).
% 0.97/1.14 tff(12,plain,
% 0.97/1.14 (~(vttempty = vttcons(Vn!309, Vft!308, Vttrest!307))),
% 0.97/1.14 inference(unit_resolution,[status(thm)],[11, 10])).
% 0.97/1.14 tff(13,plain,
% 0.97/1.14 (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[12, 3])).
% 0.97/1.14 tff(14,plain,
% 0.97/1.14 (^[Vtt: vTType, Vr: vRow, Vt1: vRawTable] : refl((~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))))),
% 0.97/1.14 inference(bind,[status(th)],[])).
% 0.97/1.14 tff(15,plain,
% 0.97/1.14 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))) <=> ![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))),
% 0.97/1.14 inference(quant_intro,[status(thm)],[14])).
% 0.97/1.14 tff(16,plain,
% 0.97/1.14 (^[Vtt: vTType, Vr: vRow, Vt1: vRawTable] : trans(trans(monotonicity(rewrite((vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)) <=> (~((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))))), ((vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (~((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))))))), rewrite((vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (~((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))), ((vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))))), rewrite((~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))), ((vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))))),
% 0.97/1.14 inference(bind,[status(th)],[])).
% 0.97/1.14 tff(17,plain,
% 0.97/1.14 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> ![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))),
% 0.97/1.14 inference(quant_intro,[status(thm)],[16])).
% 0.97/1.14 tff(18,plain,
% 0.97/1.14 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> ![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(19,axiom,(![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''welltypedRawtable-1'')).
% 0.97/1.14 tff(20,plain,
% 0.97/1.14 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[19, 18])).
% 0.97/1.14 tff(21,plain,(
% 0.97/1.14 ![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)))),
% 0.97/1.14 inference(skolemize,[status(sab)],[20])).
% 0.97/1.14 tff(22,plain,
% 0.97/1.14 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[21, 17])).
% 0.97/1.14 tff(23,plain,
% 0.97/1.14 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[22, 15])).
% 0.97/1.14 tff(24,plain,
% 0.97/1.14 (((~![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))) | (~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))))) <=> ((~![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))) | (~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2)))))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(25,plain,
% 0.97/1.14 ((~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2)))) <=> (~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(26,plain,
% 0.97/1.14 ((((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))) <=> (((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2)))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(27,plain,
% 0.97/1.14 ((~(((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2)))) <=> (~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(monotonicity,[status(thm)],[26])).
% 0.97/1.14 tff(28,plain,
% 0.97/1.14 ((~(((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2)))) <=> (~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(transitivity,[status(thm)],[27, 25])).
% 0.97/1.14 tff(29,plain,
% 0.97/1.14 (((~![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))) | (~(((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))))) <=> ((~![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))) | (~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2)))))),
% 0.97/1.14 inference(monotonicity,[status(thm)],[28])).
% 0.97/1.14 tff(30,plain,
% 0.97/1.14 (((~![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))) | (~(((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))))) <=> ((~![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))) | (~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2)))))),
% 0.97/1.14 inference(transitivity,[status(thm)],[29, 24])).
% 0.97/1.14 tff(31,plain,
% 0.97/1.14 ((~![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))) | (~(((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(quant_inst,[status(thm)],[])).
% 0.97/1.14 tff(32,plain,
% 0.97/1.14 ((~![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))) | (~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[31, 30])).
% 0.97/1.14 tff(33,plain,
% 0.97/1.14 (~(((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2)))),
% 0.97/1.14 inference(unit_resolution,[status(thm)],[32, 23])).
% 0.97/1.14 tff(34,plain,
% 0.97/1.14 ((~![Vn: vName, Vft: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), vtcons(vrempty, vrt2))) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(vtcons(vrempty, vrt2))))) <=> (~![Vn: vName, Vft: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), vtcons(vrempty, vrt2))) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(vtcons(vrempty, vrt2)))))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(35,plain,
% 0.97/1.14 ((~![Vn: vName, Vft: vFType, Vttrest: vTType] : (vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), vtcons(vrempty, vrt2)) => vwelltypedRawtable(Vttrest, vdropFirstColRaw(vtcons(vrempty, vrt2))))) <=> (~![Vn: vName, Vft: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), vtcons(vrempty, vrt2))) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(vtcons(vrempty, vrt2)))))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(36,axiom,(~![Vn: vName, Vft: vFType, Vttrest: vTType] : (vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), vtcons(vrempty, vrt2)) => vwelltypedRawtable(Vttrest, vdropFirstColRaw(vtcons(vrempty, vrt2))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''dropFirstColRawPreservesWelltypedRaw-tcons-rempty'')).
% 0.97/1.14 tff(37,plain,
% 0.97/1.14 (~![Vn: vName, Vft: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), vtcons(vrempty, vrt2))) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[36, 35])).
% 0.97/1.14 tff(38,plain,
% 0.97/1.14 (~![Vn: vName, Vft: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), vtcons(vrempty, vrt2))) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[37, 34])).
% 0.97/1.14 tff(39,plain,
% 0.97/1.14 (~![Vn: vName, Vft: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), vtcons(vrempty, vrt2))) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[38, 34])).
% 0.97/1.14 tff(40,plain,
% 0.97/1.14 (~![Vn: vName, Vft: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), vtcons(vrempty, vrt2))) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[39, 34])).
% 0.97/1.14 tff(41,plain,(
% 0.97/1.14 ~((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))) | vwelltypedRawtable(Vttrest!307, vdropFirstColRaw(vtcons(vrempty, vrt2))))),
% 0.97/1.14 inference(skolemize,[status(sab)],[40])).
% 0.97/1.14 tff(42,plain,
% 0.97/1.14 (vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))),
% 0.97/1.14 inference(or_elim,[status(thm)],[41])).
% 0.97/1.14 tff(43,plain,
% 0.97/1.14 ((((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))) | (~((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)))) | (~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2)))),
% 0.97/1.14 inference(tautology,[status(thm)],[])).
% 0.97/1.14 tff(44,plain,
% 0.97/1.14 ((((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) <=> vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vtcons(vrempty, vrt2))) | (~((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))))),
% 0.97/1.14 inference(unit_resolution,[status(thm)],[43, 42])).
% 0.97/1.14 tff(45,plain,
% 0.97/1.14 (~((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)))),
% 0.97/1.14 inference(unit_resolution,[status(thm)],[44, 33])).
% 0.97/1.14 tff(46,plain,
% 0.97/1.14 (((~vwelltypedRawtable(vttcons(Vn!309, Vft!308, Vttrest!307), vrt2)) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty))) | vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)),
% 0.97/1.14 inference(tautology,[status(thm)],[])).
% 0.97/1.14 tff(47,plain,
% 0.97/1.14 (vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)),
% 0.97/1.14 inference(unit_resolution,[status(thm)],[46, 45])).
% 0.97/1.14 tff(48,plain,
% 0.97/1.14 (^[VwildcardName0: vTType, VwildcardName1: vRow] : refl(((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0))))))) <=> ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0))))))))),
% 0.97/1.14 inference(bind,[status(th)],[])).
% 0.97/1.14 tff(49,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0))))))) <=> ![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))),
% 0.97/1.14 inference(quant_intro,[status(thm)],[48])).
% 0.97/1.14 tff(50,plain,
% 0.97/1.14 (^[VwildcardName0: vTType, VwildcardName1: vRow] : rewrite(((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0))))) <=> ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0))))))))),
% 0.97/1.14 inference(bind,[status(th)],[])).
% 0.97/1.14 tff(51,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0))))) <=> ![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))),
% 0.97/1.14 inference(quant_intro,[status(thm)],[50])).
% 0.97/1.14 tff(52,plain,
% 0.97/1.14 (^[VwildcardName0: vTType, VwildcardName1: vRow] : trans(monotonicity(monotonicity(rewrite((~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) <=> (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))))), (((~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0))))) <=> ((~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0))))))), (((~vwelltypedRow(VwildcardName0, VwildcardName1)) | ((~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))) <=> ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | ((~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))), rewrite(((~vwelltypedRow(VwildcardName0, VwildcardName1)) | ((~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))) <=> ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))), (((~vwelltypedRow(VwildcardName0, VwildcardName1)) | ((~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))) <=> ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))),
% 0.97/1.14 inference(bind,[status(th)],[])).
% 0.97/1.14 tff(53,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | ((~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))) <=> ![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))),
% 0.97/1.14 inference(quant_intro,[status(thm)],[52])).
% 0.97/1.14 tff(54,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0))))))) <=> ![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0)))))))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(55,plain,
% 0.97/1.14 (^[VwildcardName0: vTType, VwildcardName1: vRow] : trans(monotonicity(rewrite((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0))) | ![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))))) <=> (((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0)))))), (((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0))) | ![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))))) => (~vwelltypedRow(VwildcardName0, VwildcardName1))) <=> ((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0))))) => (~vwelltypedRow(VwildcardName0, VwildcardName1))))), rewrite(((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0))))) => (~vwelltypedRow(VwildcardName0, VwildcardName1))) <=> ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0)))))))), (((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0))) | ![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))))) => (~vwelltypedRow(VwildcardName0, VwildcardName1))) <=> ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0)))))))))),
% 0.97/1.14 inference(bind,[status(th)],[])).
% 0.97/1.14 tff(56,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0))) | ![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))))) => (~vwelltypedRow(VwildcardName0, VwildcardName1))) <=> ![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0)))))))),
% 0.97/1.14 inference(quant_intro,[status(thm)],[55])).
% 0.97/1.14 tff(57,axiom,(![VwildcardName0: vTType, VwildcardName1: vRow] : ((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0))) | ![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))))) => (~vwelltypedRow(VwildcardName0, VwildcardName1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''welltypedRow-2'')).
% 0.97/1.14 tff(58,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0)))))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[57, 56])).
% 0.97/1.14 tff(59,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty))) & (![Vv0: vVal, Vr0: vRow] : (~(VwildcardName1 = vrcons(Vv0, Vr0))) | ![VwildcardName00: vName, Vft0: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(VwildcardName00, Vft0, Vttr0)))))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[58, 54])).
% 0.97/1.14 tff(60,plain,(
% 0.97/1.14 ![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | ((~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0))))))),
% 0.97/1.14 inference(skolemize,[status(sab)],[59])).
% 0.97/1.14 tff(61,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | ((VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[60, 53])).
% 0.97/1.14 tff(62,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[61, 51])).
% 0.97/1.14 tff(63,plain,
% 0.97/1.14 (![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[62, 49])).
% 0.97/1.14 tff(64,plain,
% 0.97/1.14 (((~![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))) | ((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))))) <=> ((~![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(65,plain,
% 0.97/1.14 (((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307)))))))) <=> ((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(66,plain,
% 0.97/1.14 ((~(~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty))) <=> (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(67,plain,
% 0.97/1.14 (((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | $false) <=> (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty))),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(68,plain,
% 0.97/1.14 ((~$true) <=> $false),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(69,plain,
% 0.97/1.14 ((vrempty = vrempty) <=> $true),
% 0.97/1.14 inference(rewrite,[status(thm)],[])).
% 0.97/1.14 tff(70,plain,
% 0.97/1.14 ((~(vrempty = vrempty)) <=> (~$true)),
% 0.97/1.14 inference(monotonicity,[status(thm)],[69])).
% 0.97/1.14 tff(71,plain,
% 0.97/1.14 ((~(vrempty = vrempty)) <=> $false),
% 0.97/1.14 inference(transitivity,[status(thm)],[70, 68])).
% 0.97/1.14 tff(72,plain,
% 0.97/1.14 (((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | (~(vrempty = vrempty))) <=> ((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | $false)),
% 0.97/1.14 inference(monotonicity,[status(thm)],[71])).
% 0.97/1.14 tff(73,plain,
% 0.97/1.14 (((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | (~(vrempty = vrempty))) <=> (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty))),
% 0.97/1.14 inference(transitivity,[status(thm)],[72, 67])).
% 0.97/1.14 tff(74,plain,
% 0.97/1.14 ((~((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | (~(vrempty = vrempty)))) <=> (~(~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)))),
% 0.97/1.14 inference(monotonicity,[status(thm)],[73])).
% 0.97/1.14 tff(75,plain,
% 0.97/1.14 ((~((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | (~(vrempty = vrempty)))) <=> (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)),
% 0.97/1.14 inference(transitivity,[status(thm)],[74, 66])).
% 0.97/1.14 tff(76,plain,
% 0.97/1.14 (((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | (~(vrempty = vrempty)))) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307)))))))) <=> ((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))))),
% 0.97/1.14 inference(monotonicity,[status(thm)],[75])).
% 0.97/1.14 tff(77,plain,
% 0.97/1.14 (((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | (~(vrempty = vrempty)))) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307)))))))) <=> ((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))))),
% 0.97/1.14 inference(transitivity,[status(thm)],[76, 65])).
% 0.97/1.14 tff(78,plain,
% 0.97/1.14 (((~![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))) | ((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | (~(vrempty = vrempty)))) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))))) <=> ((~![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))) | ((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307)))))))))),
% 0.97/1.14 inference(monotonicity,[status(thm)],[77])).
% 0.97/1.14 tff(79,plain,
% 0.97/1.14 (((~![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))) | ((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | (~(vrempty = vrempty)))) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))))) <=> ((~![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))))),
% 0.97/1.14 inference(transitivity,[status(thm)],[78, 64])).
% 0.97/1.14 tff(80,plain,
% 0.97/1.14 ((~![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))) | ((~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (~((~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty)) | (~(vrempty = vrempty)))) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))))),
% 0.97/1.14 inference(quant_inst,[status(thm)],[])).
% 0.97/1.14 tff(81,plain,
% 0.97/1.14 ((~![VwildcardName0: vTType, VwildcardName1: vRow] : ((~vwelltypedRow(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vrempty)))) | (~((~(VwildcardName1 = vrcons(tptp_fun_Vv0_64(VwildcardName1), tptp_fun_Vr0_63(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_VwildcardName00_67(VwildcardName0), tptp_fun_Vft0_66(VwildcardName0), tptp_fun_Vttr0_65(VwildcardName0)))))))) | (~vwelltypedRow(vttcons(Vn!309, Vft!308, Vttrest!307), vrempty)) | (vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307)))))))),
% 0.97/1.14 inference(modus_ponens,[status(thm)],[80, 79])).
% 0.97/1.14 tff(82,plain,
% 0.97/1.14 ((vttcons(Vn!309, Vft!308, Vttrest!307) = vttempty) | (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307)))))))),
% 0.97/1.14 inference(unit_resolution,[status(thm)],[81, 63, 47])).
% 0.97/1.16 tff(83,plain,
% 0.97/1.16 (~((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307))))))),
% 0.97/1.16 inference(unit_resolution,[status(thm)],[82, 13])).
% 0.97/1.16 tff(84,plain,
% 0.97/1.16 (((~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))) | (~(vttcons(Vn!309, Vft!308, Vttrest!307) = vttcons(tptp_fun_VwildcardName00_67(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vft0_66(vttcons(Vn!309, Vft!308, Vttrest!307)), tptp_fun_Vttr0_65(vttcons(Vn!309, Vft!308, Vttrest!307)))))) | (vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty)))),
% 0.97/1.16 inference(tautology,[status(thm)],[])).
% 0.97/1.16 tff(85,plain,
% 0.97/1.16 (vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty))),
% 0.97/1.16 inference(unit_resolution,[status(thm)],[84, 83])).
% 0.97/1.16 tff(86,plain,
% 0.97/1.16 (^[VVal0: vVal, VRow0: vRow] : refl((~(vrempty = vrcons(VVal0, VRow0))) <=> (~(vrempty = vrcons(VVal0, VRow0))))),
% 0.97/1.16 inference(bind,[status(th)],[])).
% 0.97/1.16 tff(87,plain,
% 0.97/1.16 (![VVal0: vVal, VRow0: vRow] : (~(vrempty = vrcons(VVal0, VRow0))) <=> ![VVal0: vVal, VRow0: vRow] : (~(vrempty = vrcons(VVal0, VRow0)))),
% 0.97/1.16 inference(quant_intro,[status(thm)],[86])).
% 0.97/1.16 tff(88,plain,
% 0.97/1.16 (![VVal0: vVal, VRow0: vRow] : (~(vrempty = vrcons(VVal0, VRow0))) <=> ![VVal0: vVal, VRow0: vRow] : (~(vrempty = vrcons(VVal0, VRow0)))),
% 0.97/1.16 inference(rewrite,[status(thm)],[])).
% 0.97/1.16 tff(89,axiom,(![VVal0: vVal, VRow0: vRow] : (~(vrempty = vrcons(VVal0, VRow0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''DIFF-rempty-rcons'')).
% 0.97/1.16 tff(90,plain,
% 0.97/1.16 (![VVal0: vVal, VRow0: vRow] : (~(vrempty = vrcons(VVal0, VRow0)))),
% 0.97/1.16 inference(modus_ponens,[status(thm)],[89, 88])).
% 0.97/1.16 tff(91,plain,(
% 0.97/1.16 ![VVal0: vVal, VRow0: vRow] : (~(vrempty = vrcons(VVal0, VRow0)))),
% 0.97/1.16 inference(skolemize,[status(sab)],[90])).
% 0.97/1.16 tff(92,plain,
% 0.97/1.16 (![VVal0: vVal, VRow0: vRow] : (~(vrempty = vrcons(VVal0, VRow0)))),
% 0.97/1.16 inference(modus_ponens,[status(thm)],[91, 87])).
% 0.97/1.16 tff(93,plain,
% 0.97/1.16 ((~![VVal0: vVal, VRow0: vRow] : (~(vrempty = vrcons(VVal0, VRow0)))) | (~(vrempty = vrcons(tptp_fun_Vv0_64(vrempty), tptp_fun_Vr0_63(vrempty))))),
% 0.97/1.16 inference(quant_inst,[status(thm)],[])).
% 0.97/1.16 tff(94,plain,
% 0.97/1.16 ($false),
% 0.97/1.16 inference(unit_resolution,[status(thm)],[93, 92, 85])).
% 0.97/1.16 % SZS output end Proof
% 0.97/1.16 % E exiting
%------------------------------------------------------------------------------