%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM305_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n007.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:07 PM UTC 2026
% Result : Theorem 0.29s 0.48s
% Output : Proof 0.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : COM305_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.11 % Command : run_E %s %d THM
% 0.13/0.31 % Computer : n007.cluster.edu
% 0.13/0.31 % Model : x86_64 x86_64
% 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.31 % Memory : 8042.1875MB
% 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.31 % CPULimit : 300
% 0.13/0.31 % WCLimit : 300
% 0.13/0.31 % DateTime : Mon May 4 20:39:55 EDT 2026
% 0.13/0.31 % CPUTime :
% 0.29/0.48 % SZS status Theorem
% 0.29/0.48 % SZS output start Proof
% 0.29/0.48 tff(vwelltypedRawtable_type, type, (
% 0.29/0.48 vwelltypedRawtable: ( vTType * vRawTable ) > $o)).
% 0.29/0.48 tff(vtempty_type, type, (
% 0.29/0.48 vtempty: vRawTable)).
% 0.29/0.48 tff(vttcons_type, type, (
% 0.29/0.48 vttcons: ( vName * vFType * vTType ) > vTType)).
% 0.29/0.48 tff(vttempty_type, type, (
% 0.29/0.48 vttempty: vTType)).
% 0.29/0.48 tff(tptp_fun_Vct_308_type, type, (
% 0.29/0.48 tptp_fun_Vct_308: vFType)).
% 0.29/0.48 tff(tptp_fun_Va_309_type, type, (
% 0.29/0.48 tptp_fun_Va_309: vName)).
% 0.29/0.48 tff(vprojectFirstRaw_type, type, (
% 0.29/0.48 vprojectFirstRaw: vRawTable > vRawTable)).
% 0.29/0.48 tff(tptp_fun_Vttrest_307_type, type, (
% 0.29/0.48 tptp_fun_Vttrest_307: vTType)).
% 0.29/0.48 tff(1,plain,
% 0.29/0.48 ((vprojectFirstRaw(vtempty) = vtempty) <=> (vprojectFirstRaw(vtempty) = vtempty)),
% 0.29/0.48 inference(rewrite,[status(thm)],[])).
% 0.29/0.48 tff(2,axiom,(vprojectFirstRaw(vtempty) = vtempty), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''projectFirstRaw-0'')).
% 0.29/0.48 tff(3,plain,
% 0.29/0.48 (vprojectFirstRaw(vtempty) = vtempty),
% 0.29/0.48 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.29/0.48 tff(4,plain,
% 0.29/0.48 (vtempty = vprojectFirstRaw(vtempty)),
% 0.29/0.48 inference(symmetry,[status(thm)],[3])).
% 0.29/0.48 tff(5,plain,
% 0.29/0.48 (vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vtempty) <=> vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vprojectFirstRaw(vtempty))),
% 0.29/0.48 inference(monotonicity,[status(thm)],[4])).
% 0.29/0.48 tff(6,plain,
% 0.29/0.48 (vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vprojectFirstRaw(vtempty)) <=> vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vtempty)),
% 0.29/0.48 inference(symmetry,[status(thm)],[5])).
% 0.29/0.48 tff(7,plain,
% 0.29/0.48 ((~vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vprojectFirstRaw(vtempty))) <=> (~vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vtempty))),
% 0.29/0.48 inference(monotonicity,[status(thm)],[6])).
% 0.29/0.48 tff(8,plain,
% 0.29/0.48 ((~![Va: vName, Vct: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Va, Vct, Vttrest), vtempty)) | vwelltypedRawtable(vttcons(Va, Vct, vttempty), vprojectFirstRaw(vtempty)))) <=> (~![Va: vName, Vct: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Va, Vct, Vttrest), vtempty)) | vwelltypedRawtable(vttcons(Va, Vct, vttempty), vprojectFirstRaw(vtempty))))),
% 0.29/0.48 inference(rewrite,[status(thm)],[])).
% 0.29/0.48 tff(9,plain,
% 0.29/0.48 ((~![Va: vName, Vct: vFType, Vttrest: vTType] : (vwelltypedRawtable(vttcons(Va, Vct, Vttrest), vtempty) => vwelltypedRawtable(vttcons(Va, Vct, vttempty), vprojectFirstRaw(vtempty)))) <=> (~![Va: vName, Vct: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Va, Vct, Vttrest), vtempty)) | vwelltypedRawtable(vttcons(Va, Vct, vttempty), vprojectFirstRaw(vtempty))))),
% 0.29/0.48 inference(rewrite,[status(thm)],[])).
% 0.29/0.48 tff(10,axiom,(~![Va: vName, Vct: vFType, Vttrest: vTType] : (vwelltypedRawtable(vttcons(Va, Vct, Vttrest), vtempty) => vwelltypedRawtable(vttcons(Va, Vct, vttempty), vprojectFirstRaw(vtempty)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''projectFirstRawPreservesWelltypedRaw-tempty'')).
% 0.29/0.48 tff(11,plain,
% 0.29/0.48 (~![Va: vName, Vct: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Va, Vct, Vttrest), vtempty)) | vwelltypedRawtable(vttcons(Va, Vct, vttempty), vprojectFirstRaw(vtempty)))),
% 0.29/0.48 inference(modus_ponens,[status(thm)],[10, 9])).
% 0.29/0.48 tff(12,plain,
% 0.29/0.48 (~![Va: vName, Vct: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Va, Vct, Vttrest), vtempty)) | vwelltypedRawtable(vttcons(Va, Vct, vttempty), vprojectFirstRaw(vtempty)))),
% 0.29/0.48 inference(modus_ponens,[status(thm)],[11, 8])).
% 0.29/0.48 tff(13,plain,
% 0.29/0.48 (~![Va: vName, Vct: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Va, Vct, Vttrest), vtempty)) | vwelltypedRawtable(vttcons(Va, Vct, vttempty), vprojectFirstRaw(vtempty)))),
% 0.29/0.48 inference(modus_ponens,[status(thm)],[12, 8])).
% 0.29/0.48 tff(14,plain,
% 0.29/0.48 (~![Va: vName, Vct: vFType, Vttrest: vTType] : ((~vwelltypedRawtable(vttcons(Va, Vct, Vttrest), vtempty)) | vwelltypedRawtable(vttcons(Va, Vct, vttempty), vprojectFirstRaw(vtempty)))),
% 0.29/0.48 inference(modus_ponens,[status(thm)],[13, 8])).
% 0.29/0.48 tff(15,plain,(
% 0.29/0.48 ~((~vwelltypedRawtable(vttcons(Va!309, Vct!308, Vttrest!307), vtempty)) | vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vprojectFirstRaw(vtempty)))),
% 0.29/0.50 inference(skolemize,[status(sab)],[14])).
% 0.29/0.50 tff(16,plain,
% 0.29/0.50 (~vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vprojectFirstRaw(vtempty))),
% 0.29/0.50 inference(or_elim,[status(thm)],[15])).
% 0.29/0.50 tff(17,plain,
% 0.29/0.50 (~vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vtempty)),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[16, 7])).
% 0.29/0.50 tff(18,plain,
% 0.29/0.50 (^[VwildcardName0: vTType] : refl(vwelltypedRawtable(VwildcardName0, vtempty) <=> vwelltypedRawtable(VwildcardName0, vtempty))),
% 0.29/0.50 inference(bind,[status(th)],[])).
% 0.29/0.50 tff(19,plain,
% 0.29/0.50 (![VwildcardName0: vTType] : vwelltypedRawtable(VwildcardName0, vtempty) <=> ![VwildcardName0: vTType] : vwelltypedRawtable(VwildcardName0, vtempty)),
% 0.29/0.50 inference(quant_intro,[status(thm)],[18])).
% 0.29/0.50 tff(20,plain,
% 0.29/0.50 (![VwildcardName0: vTType] : vwelltypedRawtable(VwildcardName0, vtempty) <=> ![VwildcardName0: vTType] : vwelltypedRawtable(VwildcardName0, vtempty)),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(21,axiom,(![VwildcardName0: vTType] : vwelltypedRawtable(VwildcardName0, vtempty)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''welltypedRawtable-0'')).
% 0.29/0.50 tff(22,plain,
% 0.29/0.50 (![VwildcardName0: vTType] : vwelltypedRawtable(VwildcardName0, vtempty)),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.29/0.50 tff(23,plain,(
% 0.29/0.50 ![VwildcardName0: vTType] : vwelltypedRawtable(VwildcardName0, vtempty)),
% 0.29/0.50 inference(skolemize,[status(sab)],[22])).
% 0.29/0.50 tff(24,plain,
% 0.29/0.50 (![VwildcardName0: vTType] : vwelltypedRawtable(VwildcardName0, vtempty)),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[23, 19])).
% 0.29/0.50 tff(25,plain,
% 0.29/0.50 ((~![VwildcardName0: vTType] : vwelltypedRawtable(VwildcardName0, vtempty)) | vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vtempty)),
% 0.29/0.50 inference(quant_inst,[status(thm)],[])).
% 0.29/0.50 tff(26,plain,
% 0.29/0.50 (vwelltypedRawtable(vttcons(Va!309, Vct!308, vttempty), vtempty)),
% 0.29/0.50 inference(unit_resolution,[status(thm)],[25, 24])).
% 0.29/0.50 tff(27,plain,
% 0.29/0.50 ($false),
% 0.29/0.50 inference(unit_resolution,[status(thm)],[26, 17])).
% 0.29/0.50 % SZS output end Proof
% 0.29/0.50 % E exiting
%------------------------------------------------------------------------------