%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SET062^7 : TPTP v9.2.0. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n028.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 : Thu Oct 9 02:25:13 PM UTC 2025
% Result : Theorem 168.54s 166.34s
% Output : Proof 168.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET062^7 : TPTP v9.2.0. Released v5.5.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n028.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 8 14:34:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 120.22/118.03 slave returned with unknown status
% 168.54/166.34 % SZS status Theorem
% 168.54/166.34 % Mode: mode328:USE_SINE=true:SINE_TOLERANCE=5.0:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 168.54/166.34 % Inferences: 16149
% 168.54/166.34 % SZS output start Proof
% 168.54/166.34 thf(def_mnot,definition,(mnot = (^[X1:$i>$o]:(^[X2:$i]:(~((X1 @ X2))))))).
% 168.54/166.34 thf(def_mor,definition,(mor = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((~((X1 @ X3))) => (X2 @ X3))))))).
% 168.54/166.34 thf(def_mand,definition,(mand = (^[X1:$i>$o]:(^[X2:$i>$o]:(mnot @ ((mor @ (mnot @ X1)) @ (mnot @ X2))))))).
% 168.54/166.34 thf(def_mimplies,definition,(mimplies = (^[X1:$i>$o]:(mor @ (mnot @ X1))))).
% 168.54/166.34 thf(def_mequiv,definition,(mequiv = (^[X1:$i>$o]:(^[X2:$i>$o]:((mand @ ((mimplies @ X1) @ X2)) @ ((mimplies @ X2) @ X1)))))).
% 168.54/166.34 thf(def_mforall_ind,definition,(mforall_ind = (^[X1:mu>$i>$o]:(^[X2:$i]:(![X3:mu]:(((exists_in_world @ X3) @ X2) => ((X1 @ X3) @ X2))))))).
% 168.54/166.34 thf(def_mexists_ind,definition,(mexists_ind = (^[X1:mu>$i>$o]:(mnot @ (mforall_ind @ (^[X2:mu]:(mnot @ (X1 @ X2)))))))).
% 168.54/166.34 thf(def_mvalid,definition,(mvalid = (!!))).
% 168.54/166.34 thf(thI15,conjecture,(![X1:$i]:(![X2:mu]:(((exists_in_world @ X2) @ X1) => (((subset @ empty_set) @ X2) @ X1))))).
% 168.54/166.34 thf(h0,negated_conjecture,(~((![X1:$i]:(![X2:mu]:(((exists_in_world @ X2) @ X1) => (((subset @ empty_set) @ X2) @ X1)))))),inference(assume_negation,[status(cth)],[thI15])).
% 168.54/166.34 thf(ax918, axiom, (~(p34)|p82), file('<stdin>', ax918)).
% 168.54/166.34 thf(ax940, axiom, (~(p12)|p60), file('<stdin>', ax940)).
% 168.54/166.34 thf(ax834, axiom, (~(p82)|p166), file('<stdin>', ax834)).
% 168.54/166.34 thf(ax966, axiom, p34, file('<stdin>', ax966)).
% 168.54/166.34 thf(pax60, axiom, (p60=>fexists_in_world @ fempty_set @ f__0), file('<stdin>', pax60)).
% 168.54/166.34 thf(ax988, axiom, p12, file('<stdin>', ax988)).
% 168.54/166.34 thf(ax954, axiom, (p1|~(p46)), file('<stdin>', ax954)).
% 168.54/166.34 thf(ax999, axiom, ~(p1), file('<stdin>', ax999)).
% 168.54/166.34 thf(pax166, axiom, (p166=>(fexists_in_world @ fempty_set @ f__0=>![X44:mu]:(fexists_in_world @ X44 @ f__0=>~(((fsubset @ fempty_set @ X44 @ f__0=>![X42:mu]:(fexists_in_world @ X42 @ f__0=>(fmember @ X42 @ fempty_set @ f__0=>fmember @ X42 @ X44 @ f__0)))=>~((![X42:mu]:(fexists_in_world @ X42 @ f__0=>(fmember @ X42 @ fempty_set @ f__0=>fmember @ X42 @ X44 @ f__0))=>fsubset @ fempty_set @ X44 @ f__0))))))), file('<stdin>', pax166)).
% 168.54/166.34 thf(nax46, axiom, (p46<=![X56:mu]:(fexists_in_world @ X56 @ f__0=>fsubset @ fempty_set @ X56 @ f__0)), file('<stdin>', nax46)).
% 168.54/166.34 thf(pax39, axiom, (p39=>![X57:$i, X58:mu]:(fexists_in_world @ X58 @ X57=>~(fmember @ X58 @ fempty_set @ X57))), file('<stdin>', pax39)).
% 168.54/166.34 thf(ax961, axiom, p39, file('<stdin>', ax961)).
% 168.54/166.34 thf(c_0_12, plain, (~p34|p82), inference(fof_simplification,[status(thm)],[ax918])).
% 168.54/166.34 thf(c_0_13, plain, (~p12|p60), inference(fof_simplification,[status(thm)],[ax940])).
% 168.54/166.34 thf(c_0_14, plain, (~p82|p166), inference(fof_simplification,[status(thm)],[ax834])).
% 168.54/166.34 thf(c_0_15, plain, (p82|~p34), inference(split_conjunct,[status(thm)],[c_0_12])).
% 168.54/166.34 thf(c_0_16, plain, p34, inference(split_conjunct,[status(thm)],[ax966])).
% 168.54/166.34 thf(c_0_17, plain, (~p60|fexists_in_world @ fempty_set @ f__0), inference(fof_nnf,[status(thm)],[pax60])).
% 168.54/166.34 thf(c_0_18, plain, (p60|~p12), inference(split_conjunct,[status(thm)],[c_0_13])).
% 168.54/166.34 thf(c_0_19, plain, p12, inference(split_conjunct,[status(thm)],[ax988])).
% 168.54/166.34 thf(c_0_20, plain, (p1|~p46), inference(fof_simplification,[status(thm)],[ax954])).
% 168.54/166.34 thf(c_0_21, plain, ~p1, inference(fof_simplification,[status(thm)],[ax999])).
% 168.54/166.34 thf(c_0_22, plain, ![X1739:mu, X1740:mu]:((~fsubset @ fempty_set @ X1739 @ f__0|(~fexists_in_world @ X1740 @ f__0|(~fmember @ X1740 @ fempty_set @ f__0|fmember @ X1740 @ X1739 @ f__0))|~fexists_in_world @ X1739 @ f__0|~fexists_in_world @ fempty_set @ f__0|~p166)&((fexists_in_world @ (esk838_1 @ X1739) @ f__0|fsubset @ fempty_set @ X1739 @ f__0|~fexists_in_world @ X1739 @ f__0|~fexists_in_world @ fempty_set @ f__0|~p166)&((fmember @ (esk838_1 @ X1739) @ fempty_set @ f__0|fsubset @ fempty_set @ X1739 @ f__0|~fexists_in_world @ X1739 @ f__0|~fexists_in_world @ fempty_set @ f__0|~p166)&(~fmember @ (esk838_1 @ X1739) @ X1739 @ f__0|fsubset @ fempty_set @ X1739 @ f__0|~fexists_in_world @ X1739 @ f__0|~fexists_in_world @ fempty_set @ f__0|~p166)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax166])])])])])).
% 168.54/166.34 thf(c_0_23, plain, (p166|~p82), inference(split_conjunct,[status(thm)],[c_0_14])).
% 168.54/166.34 thf(c_0_24, plain, p82, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_15, c_0_16])])).
% 168.54/166.34 thf(c_0_25, plain, (fexists_in_world @ fempty_set @ f__0|~p60), inference(split_conjunct,[status(thm)],[c_0_17])).
% 168.54/166.34 thf(c_0_26, plain, p60, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19])])).
% 168.54/166.34 thf(c_0_27, plain, ((fexists_in_world @ esk1056_0 @ f__0|p46)&(~fsubset @ fempty_set @ esk1056_0 @ f__0|p46)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax46])])])])])).
% 168.54/166.34 thf(c_0_28, plain, (p1|~p46), inference(split_conjunct,[status(thm)],[c_0_20])).
% 168.54/166.34 thf(c_0_29, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_21])).
% 168.54/166.34 thf(c_0_30, plain, ![X2223:$i, X2224:mu]:(~p39|(~fexists_in_world @ X2224 @ X2223|~fmember @ X2224 @ fempty_set @ X2223)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax39])])])])).
% 168.54/166.34 thf(c_0_31, plain, ![X1:mu]:(fmember @ (esk838_1 @ X1) @ fempty_set @ f__0|fsubset @ fempty_set @ X1 @ f__0|~fexists_in_world @ X1 @ f__0|~fexists_in_world @ fempty_set @ f__0|~p166), inference(split_conjunct,[status(thm)],[c_0_22])).
% 168.54/166.34 thf(c_0_32, plain, p166, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])])).
% 168.54/166.34 thf(c_0_33, plain, fexists_in_world @ fempty_set @ f__0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])])).
% 168.54/166.34 thf(c_0_34, plain, (fexists_in_world @ esk1056_0 @ f__0|p46), inference(split_conjunct,[status(thm)],[c_0_27])).
% 168.54/166.34 thf(c_0_35, plain, ~p46, inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 168.54/166.34 thf(c_0_36, plain, (p46|~fsubset @ fempty_set @ esk1056_0 @ f__0), inference(split_conjunct,[status(thm)],[c_0_27])).
% 168.54/166.34 thf(c_0_37, plain, ![X1:mu]:(fexists_in_world @ (esk838_1 @ X1) @ f__0|fsubset @ fempty_set @ X1 @ f__0|~fexists_in_world @ X1 @ f__0|~fexists_in_world @ fempty_set @ f__0|~p166), inference(split_conjunct,[status(thm)],[c_0_22])).
% 168.54/166.34 thf(c_0_38, plain, ![X1:mu, X3:$i]:(~p39|~fexists_in_world @ X1 @ X3|~fmember @ X1 @ fempty_set @ X3), inference(split_conjunct,[status(thm)],[c_0_30])).
% 168.54/166.34 thf(c_0_39, plain, p39, inference(split_conjunct,[status(thm)],[ax961])).
% 168.54/166.34 thf(c_0_40, plain, ![X1:mu]:(fmember @ (esk838_1 @ X1) @ fempty_set @ f__0|fsubset @ fempty_set @ X1 @ f__0|~fexists_in_world @ X1 @ f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32]), c_0_33])])).
% 168.54/166.34 thf(c_0_41, plain, fexists_in_world @ esk1056_0 @ f__0, inference(sr,[status(thm)],[c_0_34, c_0_35])).
% 168.54/166.34 thf(c_0_42, plain, ~fsubset @ fempty_set @ esk1056_0 @ f__0, inference(sr,[status(thm)],[c_0_36, c_0_35])).
% 168.54/166.34 thf(c_0_43, plain, ![X1:mu]:(fsubset @ fempty_set @ X1 @ f__0|fexists_in_world @ (esk838_1 @ X1) @ f__0|~fexists_in_world @ X1 @ f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_32]), c_0_33])])).
% 168.54/166.34 thf(c_0_44, plain, ![X1:mu, X3:$i]:(~fmember @ X1 @ fempty_set @ X3|~fexists_in_world @ X1 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39])])).
% 168.54/166.34 thf(c_0_45, plain, fmember @ (esk838_1 @ esk1056_0) @ fempty_set @ f__0, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_42])).
% 168.54/166.34 thf(c_0_46, plain, fexists_in_world @ (esk838_1 @ esk1056_0) @ f__0, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_41]), c_0_42])).
% 168.54/166.34 thf(c_0_47, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_45]), c_0_46])]), ['proof']).
% 168.54/166.34 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 168.54/166.34 thf(0,theorem,(![X1:$i]:(![X2:mu]:(((exists_in_world @ X2) @ X1) => (((subset @ empty_set) @ X2) @ X1)))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 168.54/166.34 % SZS output end Proof
%------------------------------------------------------------------------------