%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP141^1 : TPTP v9.2.0. Released v7.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 01:47:05 PM UTC 2025
% Result : Theorem 6.64s 7.05s
% Output : Proof 6.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : ITP141^1 : TPTP v9.2.0. Released v7.5.0.
% 0.14/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.15/0.35 % Computer : n028.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Wed Oct 8 18:23:53 EDT 2025
% 0.15/0.35 % CPUTime :
% 6.64/7.05 % SZS status Theorem
% 6.64/7.05 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 6.64/7.05 % Inferences: 205
% 6.64/7.05 % SZS output start Proof
% 6.64/7.05 thf(ty_com, type, com : $tType).
% 6.64/7.05 thf(ty_state, type, state : $tType).
% 6.64/7.05 thf(ty_a, type, a : $tType).
% 6.64/7.05 thf(ty_eigen__2, type, eigen__2 : a).
% 6.64/7.05 thf(ty_eigen__1, type, eigen__1 : state).
% 6.64/7.05 thf(ty_eigen__0, type, eigen__0 : state).
% 6.64/7.05 thf(ty_exec, type, exec : (state>com>state>$o)).
% 6.64/7.05 thf(ty_body, type, body : com).
% 6.64/7.05 thf(ty_eigen__4, type, eigen__4 : state).
% 6.64/7.05 thf(ty_pa, type, pa : (a>state>$o)).
% 6.64/7.05 thf(ty_eigen__3, type, eigen__3 : a).
% 6.64/7.05 thf(ty_qa, type, qa : (a>state>$o)).
% 6.64/7.05 thf(ty_termi, type, termi : (com>state>$o)).
% 6.64/7.05 thf(ty_x, type, x : state).
% 6.64/7.05 thf(conj_2,conjecture,(~(((![X1:state]:(![X2:state]:((((exec @ X1) @ body) @ X2) => (![X3:a]:((~((((pa @ X3) @ X1) => (~((X1 = x)))))) => ((qa @ X3) @ X2)))))) => (~((![X1:a]:(![X2:state]:((~((((pa @ X1) @ X2) => (~((X2 = x)))))) => ((termi @ body) @ X2)))))))))).
% 6.64/7.05 thf(h0,negated_conjecture,((![X1:state]:(![X2:state]:((((exec @ X1) @ body) @ X2) => (![X3:a]:((~((((pa @ X3) @ X1) => (~((X1 = x)))))) => ((qa @ X3) @ X2)))))) => (~((![X1:a]:(![X2:state]:((~((((pa @ X1) @ X2) => (~((X2 = x)))))) => ((termi @ body) @ X2))))))),inference(assume_negation,[status(cth)],[conj_2])).
% 6.64/7.05 thf(h1,assumption,(~((![X1:state]:(![X2:state]:((((exec @ X1) @ body) @ X2) => (![X3:a]:((~((((pa @ X3) @ X1) => (~((X1 = x)))))) => ((qa @ X3) @ X2)))))))),introduced(assumption,[])).
% 6.64/7.05 thf(h2,assumption,(~((![X1:a]:(![X2:state]:((~((((pa @ X1) @ X2) => (~((X2 = x)))))) => ((termi @ body) @ X2)))))),introduced(assumption,[])).
% 6.64/7.05 thf(h3,assumption,(~((![X1:state]:((((exec @ eigen__0) @ body) @ X1) => (![X2:a]:((~((((pa @ X2) @ eigen__0) => (~((eigen__0 = x)))))) => ((qa @ X2) @ X1))))))),introduced(assumption,[])).
% 6.64/7.05 thf(h4,assumption,(~(((((exec @ eigen__0) @ body) @ eigen__1) => (![X1:a]:((~((((pa @ X1) @ eigen__0) => (~((eigen__0 = x)))))) => ((qa @ X1) @ eigen__1)))))),introduced(assumption,[])).
% 6.64/7.05 thf(h5,assumption,(((exec @ eigen__0) @ body) @ eigen__1),introduced(assumption,[])).
% 6.64/7.05 thf(h6,assumption,(~((![X1:a]:((~((((pa @ X1) @ eigen__0) => (~((eigen__0 = x)))))) => ((qa @ X1) @ eigen__1))))),introduced(assumption,[])).
% 6.64/7.05 thf(h7,assumption,(~(((~((((pa @ eigen__2) @ eigen__0) => (~((eigen__0 = x)))))) => ((qa @ eigen__2) @ eigen__1)))),introduced(assumption,[])).
% 6.64/7.05 thf(h8,assumption,(~((((pa @ eigen__2) @ eigen__0) => (~((eigen__0 = x)))))),introduced(assumption,[])).
% 6.64/7.05 thf(h9,assumption,(~(((qa @ eigen__2) @ eigen__1))),introduced(assumption,[])).
% 6.64/7.05 thf(h10,assumption,((pa @ eigen__2) @ eigen__0),introduced(assumption,[])).
% 6.64/7.05 thf(h11,assumption,(eigen__0 = x),introduced(assumption,[])).
% 6.64/7.05 thf(pax18, axiom, (p18=>(f__0)=(fx)), file('<stdin>', pax18)).
% 6.64/7.05 thf(ax171, axiom, (~(p15)|~(p32)), file('<stdin>', ax171)).
% 6.64/7.05 thf(pax20, axiom, (p20=>fexec @ f__0 @ fbody @ f__1), file('<stdin>', pax20)).
% 6.64/7.05 thf(ax186, axiom, p18, file('<stdin>', ax186)).
% 6.64/7.05 thf(ax189, axiom, p15, file('<stdin>', ax189)).
% 6.64/7.05 thf(nax17, axiom, (p17<=fqa @ f__2 @ f__1), file('<stdin>', nax17)).
% 6.64/7.05 thf(ax187, axiom, ~(p17), file('<stdin>', ax187)).
% 6.64/7.05 thf(nax203, axiom, (p203<=(![X33:state, X2:state]:(fexec @ X33 @ fbody @ X2=>![X3:a]:(~((fpa @ X3 @ X33=>~((X33)=(fx))))=>fqa @ X3 @ X2))=>~(![X34:a, X2:state]:(~((fpa @ X34 @ X2=>~((X2)=(fx))))=>ftermi @ fbody @ X2)))), file('<stdin>', nax203)).
% 6.64/7.05 thf(ax184, axiom, p20, file('<stdin>', ax184)).
% 6.64/7.05 thf(pax19, axiom, (p19=>fpa @ f__2 @ f__0), file('<stdin>', pax19)).
% 6.64/7.05 thf(ax13, axiom, (~(p201)|p202|~(p203)), file('<stdin>', ax13)).
% 6.64/7.05 thf(ax14, axiom, (p32|p201), file('<stdin>', ax14)).
% 6.64/7.05 thf(ax185, axiom, p19, file('<stdin>', ax185)).
% 6.64/7.05 thf(pax16, axiom, (p16=>![X69:state]:(fmember1389040324_state @ (fproduc64584659_state @ X69 @ fx) @ fr=>~((![X53:state, X70:state]:(fexec @ X53 @ fbody @ X70=>![X71:a]:(~((fpa @ X71 @ X53=>~((X53)=(X69))))=>fqa @ X71 @ X70))=>~(![X72:a, X70:state]:(~((fpa @ X72 @ X70=>~((X70)=(X69))))=>ftermi @ fbody @ X70)))))), file('<stdin>', pax16)).
% 6.64/7.05 thf(pax202, axiom, (p202=>(![X35:state, X2:state]:(fexec @ X35 @ fbody @ X2=>![X3:a]:(~((fpa @ X3 @ X35=>~(fmember1389040324_state @ (fproduc64584659_state @ X35 @ fx) @ fr)))=>fqa @ X3 @ X2))=>~(![X36:a, X2:state]:(~((fpa @ X36 @ X2=>~(fmember1389040324_state @ (fproduc64584659_state @ X2 @ fx) @ fr)))=>ftermi @ fbody @ X2)))), file('<stdin>', pax202)).
% 6.64/7.05 thf(ax188, axiom, p16, file('<stdin>', ax188)).
% 6.64/7.05 thf(c_0_16, plain, (~p18|(f__0)=(fx)), inference(fof_nnf,[status(thm)],[pax18])).
% 6.64/7.05 thf(c_0_17, plain, (~p15|~p32), inference(fof_simplification,[status(thm)],[ax171])).
% 6.64/7.05 thf(c_0_18, plain, (~p20|fexec @ f__0 @ fbody @ f__1), inference(fof_nnf,[status(thm)],[pax20])).
% 6.64/7.05 thf(c_0_19, plain, ((f__0)=(fx)|~p18), inference(split_conjunct,[status(thm)],[c_0_16])).
% 6.64/7.05 thf(c_0_20, plain, p18, inference(split_conjunct,[status(thm)],[ax186])).
% 6.64/7.05 thf(c_0_21, plain, (~p15|~p32), inference(split_conjunct,[status(thm)],[c_0_17])).
% 6.64/7.05 thf(c_0_22, plain, p15, inference(split_conjunct,[status(thm)],[ax189])).
% 6.64/7.05 thf(c_0_23, plain, (~fqa @ f__2 @ f__1|p17), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax17])])).
% 6.64/7.05 thf(c_0_24, plain, ~p17, inference(fof_simplification,[status(thm)],[ax187])).
% 6.64/7.05 thf(c_0_25, plain, ![X161:state, X162:state, X163:a, X164:a, X165:state]:((~fexec @ X161 @ fbody @ X162|(~fpa @ X163 @ X161|(X161)!=(fx)|fqa @ X163 @ X162)|p203)&(~fpa @ X164 @ X165|(X165)!=(fx)|ftermi @ fbody @ X165|p203)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax203])])])])])).
% 6.64/7.05 thf(c_0_26, plain, (fexec @ f__0 @ fbody @ f__1|~p20), inference(split_conjunct,[status(thm)],[c_0_18])).
% 6.64/7.05 thf(c_0_27, plain, (f__0)=(fx), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20])])).
% 6.64/7.05 thf(c_0_28, plain, p20, inference(split_conjunct,[status(thm)],[ax184])).
% 6.64/7.05 thf(c_0_29, plain, (~p19|fpa @ f__2 @ f__0), inference(fof_nnf,[status(thm)],[pax19])).
% 6.64/7.05 thf(c_0_30, plain, (~p201|p202|~p203), inference(fof_simplification,[status(thm)],[ax13])).
% 6.64/7.05 thf(c_0_31, plain, (p32|p201), inference(split_conjunct,[status(thm)],[ax14])).
% 6.64/7.05 thf(c_0_32, plain, ~p32, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 6.64/7.05 thf(c_0_33, plain, (p17|~fqa @ f__2 @ f__1), inference(split_conjunct,[status(thm)],[c_0_23])).
% 6.64/7.05 thf(c_0_34, plain, ~p17, inference(split_conjunct,[status(thm)],[c_0_24])).
% 6.64/7.05 thf(c_0_35, plain, ![X3:a, X2:state, X1:state]:(fqa @ X3 @ X2|p203|~fexec @ X1 @ fbody @ X2|~fpa @ X3 @ X1|(X1)!=(fx)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 6.64/7.05 thf(c_0_36, plain, fexec @ fx @ fbody @ f__1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27]), c_0_28])])).
% 6.64/7.05 thf(c_0_37, plain, (fpa @ f__2 @ f__0|~p19), inference(split_conjunct,[status(thm)],[c_0_29])).
% 6.64/7.05 thf(c_0_38, plain, p19, inference(split_conjunct,[status(thm)],[ax185])).
% 6.64/7.05 thf(c_0_39, plain, (p202|~p201|~p203), inference(split_conjunct,[status(thm)],[c_0_30])).
% 6.64/7.05 thf(c_0_40, plain, p201, inference(sr,[status(thm)],[c_0_31, c_0_32])).
% 6.64/7.05 thf(c_0_41, plain, ~fqa @ f__2 @ f__1, inference(sr,[status(thm)],[c_0_33, c_0_34])).
% 6.64/7.05 thf(c_0_42, plain, ![X3:a]:(fqa @ X3 @ f__1|p203|~fpa @ X3 @ fx), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 6.64/7.05 thf(c_0_43, plain, fpa @ f__2 @ fx, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_27]), c_0_38])])).
% 6.64/7.05 thf(c_0_44, plain, ![X290:state, X291:state, X292:state, X293:a, X294:a, X295:state]:((~fexec @ X291 @ fbody @ X292|(~fpa @ X293 @ X291|(X291)!=(X290)|fqa @ X293 @ X292)|~fmember1389040324_state @ (fproduc64584659_state @ X290 @ fx) @ fr|~p16)&(~fpa @ X294 @ X295|(X295)!=(X290)|ftermi @ fbody @ X295|~fmember1389040324_state @ (fproduc64584659_state @ X290 @ fx) @ fr|~p16)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax16])])])])])).
% 6.64/7.05 thf(c_0_45, plain, ((((fpa @ esk44_0 @ esk45_0|fexec @ esk41_0 @ fbody @ esk42_0|~p202)&(fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fexec @ esk41_0 @ fbody @ esk42_0|~p202))&(~ftermi @ fbody @ esk45_0|fexec @ esk41_0 @ fbody @ esk42_0|~p202))&(((((fpa @ esk44_0 @ esk45_0|fpa @ esk43_0 @ esk41_0|~p202)&(fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fpa @ esk43_0 @ esk41_0|~p202))&(~ftermi @ fbody @ esk45_0|fpa @ esk43_0 @ esk41_0|~p202))&(((fpa @ esk44_0 @ esk45_0|fmember1389040324_state @ (fproduc64584659_state @ esk41_0 @ fx) @ fr|~p202)&(fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fmember1389040324_state @ (fproduc64584659_state @ esk41_0 @ fx) @ fr|~p202))&(~ftermi @ fbody @ esk45_0|fmember1389040324_state @ (fproduc64584659_state @ esk41_0 @ fx) @ fr|~p202)))&(((fpa @ esk44_0 @ esk45_0|~fqa @ esk43_0 @ esk42_0|~p202)&(fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|~fqa @ esk43_0 @ esk42_0|~p202))&(~ftermi @ fbody @ esk45_0|~fqa @ esk43_0 @ esk42_0|~p202)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax202])])])])])).
% 6.64/7.05 thf(c_0_46, plain, (p202|~p203), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 6.64/7.05 thf(c_0_47, plain, p203, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_43])])).
% 6.64/7.05 thf(c_0_48, plain, ![X1:state, X2:state, X3:a, X5:state]:(fqa @ X3 @ X2|~fexec @ X1 @ fbody @ X2|~fpa @ X3 @ X1|(X1)!=(X5)|~fmember1389040324_state @ (fproduc64584659_state @ X5 @ fx) @ fr|~p16), inference(split_conjunct,[status(thm)],[c_0_44])).
% 6.64/7.05 thf(c_0_49, plain, p16, inference(split_conjunct,[status(thm)],[ax188])).
% 6.64/7.05 thf(c_0_50, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk41_0 @ fx) @ fr|~ftermi @ fbody @ esk45_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_51, plain, p202, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47])])).
% 6.64/7.05 thf(c_0_52, plain, (~ftermi @ fbody @ esk45_0|~fqa @ esk43_0 @ esk42_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_53, plain, ![X1:state, X3:a, X2:state]:(fqa @ X3 @ X1|~fmember1389040324_state @ (fproduc64584659_state @ X2 @ fx) @ fr|~fexec @ X2 @ fbody @ X1|~fpa @ X3 @ X2), inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49])])])).
% 6.64/7.05 thf(c_0_54, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk41_0 @ fx) @ fr|~ftermi @ fbody @ esk45_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51])])).
% 6.64/7.05 thf(c_0_55, plain, (fpa @ esk43_0 @ esk41_0|~ftermi @ fbody @ esk45_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_56, plain, (fexec @ esk41_0 @ fbody @ esk42_0|~ftermi @ fbody @ esk45_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_57, plain, ![X1:state, X3:a, X2:state]:(ftermi @ fbody @ X1|~fpa @ X3 @ X1|(X1)!=(X2)|~fmember1389040324_state @ (fproduc64584659_state @ X2 @ fx) @ fr|~p16), inference(split_conjunct,[status(thm)],[c_0_44])).
% 6.64/7.05 thf(c_0_58, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fpa @ esk43_0 @ esk41_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_59, plain, (~ftermi @ fbody @ esk45_0|~fqa @ esk43_0 @ esk42_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_52, c_0_51])])).
% 6.64/7.05 thf(c_0_60, plain, ![X1:state, X3:a]:(fqa @ X3 @ X1|~fexec @ esk41_0 @ fbody @ X1|~ftermi @ fbody @ esk45_0|~fpa @ X3 @ esk41_0), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 6.64/7.05 thf(c_0_61, plain, (fpa @ esk43_0 @ esk41_0|~ftermi @ fbody @ esk45_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_51])])).
% 6.64/7.05 thf(c_0_62, plain, (fexec @ esk41_0 @ fbody @ esk42_0|~ftermi @ fbody @ esk45_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_51])])).
% 6.64/7.05 thf(c_0_63, plain, (fpa @ esk44_0 @ esk45_0|fmember1389040324_state @ (fproduc64584659_state @ esk41_0 @ fx) @ fr|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_64, plain, ![X3:a, X1:state]:(ftermi @ fbody @ X1|~fmember1389040324_state @ (fproduc64584659_state @ X1 @ fx) @ fr|~fpa @ X3 @ X1), inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_57, c_0_49])])])).
% 6.64/7.05 thf(c_0_65, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fpa @ esk43_0 @ esk41_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_51])])).
% 6.64/7.05 thf(c_0_66, plain, ~ftermi @ fbody @ esk45_0, inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_60]), c_0_61]), c_0_62])).
% 6.64/7.05 thf(c_0_67, plain, (fpa @ esk44_0 @ esk45_0|fpa @ esk43_0 @ esk41_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_68, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fexec @ esk41_0 @ fbody @ esk42_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_69, plain, (fpa @ esk44_0 @ esk45_0|~fqa @ esk43_0 @ esk42_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_70, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk41_0 @ fx) @ fr|fpa @ esk44_0 @ esk45_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_51])])).
% 6.64/7.05 thf(c_0_71, plain, ![X3:a]:(fpa @ esk43_0 @ esk41_0|~fpa @ X3 @ esk45_0), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_65]), c_0_66])).
% 6.64/7.05 thf(c_0_72, plain, (fpa @ esk43_0 @ esk41_0|fpa @ esk44_0 @ esk45_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_51])])).
% 6.64/7.05 thf(c_0_73, plain, (fpa @ esk44_0 @ esk45_0|fexec @ esk41_0 @ fbody @ esk42_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_74, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fmember1389040324_state @ (fproduc64584659_state @ esk41_0 @ fx) @ fr|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_75, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fexec @ esk41_0 @ fbody @ esk42_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_51])])).
% 6.64/7.05 thf(c_0_76, plain, (fpa @ esk44_0 @ esk45_0|~fqa @ esk43_0 @ esk42_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_51])])).
% 6.64/7.05 thf(c_0_77, plain, ![X1:state, X3:a]:(fpa @ esk44_0 @ esk45_0|fqa @ X3 @ X1|~fexec @ esk41_0 @ fbody @ X1|~fpa @ X3 @ esk41_0), inference(spm,[status(thm)],[c_0_53, c_0_70])).
% 6.64/7.05 thf(c_0_78, plain, fpa @ esk43_0 @ esk41_0, inference(spm,[status(thm)],[c_0_71, c_0_72])).
% 6.64/7.05 thf(c_0_79, plain, (fexec @ esk41_0 @ fbody @ esk42_0|fpa @ esk44_0 @ esk45_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_51])])).
% 6.64/7.05 thf(c_0_80, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk41_0 @ fx) @ fr|fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_74, c_0_51])])).
% 6.64/7.05 thf(c_0_81, plain, ![X3:a]:(fexec @ esk41_0 @ fbody @ esk42_0|~fpa @ X3 @ esk45_0), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_75]), c_0_66])).
% 6.64/7.05 thf(c_0_82, plain, fpa @ esk44_0 @ esk45_0, inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_77]), c_0_78])]), c_0_79])).
% 6.64/7.05 thf(c_0_83, plain, ![X1:state, X3:a]:(fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fqa @ X3 @ X1|~fexec @ esk41_0 @ fbody @ X1|~fpa @ X3 @ esk41_0), inference(spm,[status(thm)],[c_0_53, c_0_80])).
% 6.64/7.05 thf(c_0_84, plain, fexec @ esk41_0 @ fbody @ esk42_0, inference(spm,[status(thm)],[c_0_81, c_0_82])).
% 6.64/7.05 thf(c_0_85, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|~fqa @ esk43_0 @ esk42_0|~p202), inference(split_conjunct,[status(thm)],[c_0_45])).
% 6.64/7.05 thf(c_0_86, plain, ![X3:a]:(fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|fqa @ X3 @ esk42_0|~fpa @ X3 @ esk41_0), inference(spm,[status(thm)],[c_0_83, c_0_84])).
% 6.64/7.05 thf(c_0_87, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr|~fqa @ esk43_0 @ esk42_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_85, c_0_51])])).
% 6.64/7.05 thf(c_0_88, plain, fmember1389040324_state @ (fproduc64584659_state @ esk45_0 @ fx) @ fr, inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_78]), c_0_87])).
% 6.64/7.05 thf(c_0_89, plain, ![X3:a]:~fpa @ X3 @ esk45_0, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_88]), c_0_66])).
% 6.64/7.05 thf(c_0_90, plain, ($false), inference(sr,[status(thm)],[c_0_82, c_0_89]), ['proof']).
% 6.64/7.05 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h10,h11,h8,h9,h7,h5,h6,h4,h3,h1,h0])],[])).
% 6.64/7.05 thf(2,plain,$false,inference(tab_negimp,[status(thm),assumptions([h8,h9,h7,h5,h6,h4,h3,h1,h0]),tab_negimp(discharge,[h10,h11])],[h8,1,h10,h11])).
% 6.64/7.05 thf(3,plain,$false,inference(tab_negimp,[status(thm),assumptions([h7,h5,h6,h4,h3,h1,h0]),tab_negimp(discharge,[h8,h9])],[h7,2,h8,h9])).
% 6.64/7.05 thf(4,plain,$false,inference(tab_negall,[status(thm),assumptions([h5,h6,h4,h3,h1,h0]),tab_negall(discharge,[h7]),tab_negall(eigenvar,eigen__2)],[h6,3,h7])).
% 6.64/7.05 thf(5,plain,$false,inference(tab_negimp,[status(thm),assumptions([h4,h3,h1,h0]),tab_negimp(discharge,[h5,h6])],[h4,4,h5,h6])).
% 6.64/7.05 thf(6,plain,$false,inference(tab_negall,[status(thm),assumptions([h3,h1,h0]),tab_negall(discharge,[h4]),tab_negall(eigenvar,eigen__1)],[h3,5,h4])).
% 6.64/7.05 thf(7,plain,$false,inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_negall(discharge,[h3]),tab_negall(eigenvar,eigen__0)],[h1,6,h3])).
% 6.64/7.05 thf(h12,assumption,(~((![X1:state]:((~((((pa @ eigen__3) @ X1) => (~((X1 = x)))))) => ((termi @ body) @ X1))))),introduced(assumption,[])).
% 6.64/7.05 thf(h13,assumption,(~(((~((((pa @ eigen__3) @ eigen__4) => (~((eigen__4 = x)))))) => ((termi @ body) @ eigen__4)))),introduced(assumption,[])).
% 6.64/7.05 thf(h14,assumption,(~((((pa @ eigen__3) @ eigen__4) => (~((eigen__4 = x)))))),introduced(assumption,[])).
% 6.64/7.05 thf(h15,assumption,(~(((termi @ body) @ eigen__4))),introduced(assumption,[])).
% 6.64/7.05 thf(h16,assumption,((pa @ eigen__3) @ eigen__4),introduced(assumption,[])).
% 6.64/7.05 thf(h17,assumption,(eigen__4 = x),introduced(assumption,[])).
% 6.64/7.05 thf(pax220, axiom, (p220=>(f__4)=(fx)), file('<stdin>', pax220)).
% 6.64/7.05 thf(pax221, axiom, (p221=>fpa @ f__3 @ f__4), file('<stdin>', pax221)).
% 6.64/7.05 thf(ax226, axiom, p220, file('<stdin>', ax226)).
% 6.64/7.05 thf(nax219, axiom, (p219<=ftermi @ fbody @ f__4), file('<stdin>', nax219)).
% 6.64/7.05 thf(ax227, axiom, ~(p219), file('<stdin>', ax227)).
% 6.64/7.05 thf(ax210, axiom, (~(p15)|~(p32)), file('<stdin>', ax210)).
% 6.64/7.05 thf(nax203, axiom, (p203<=(![X59:state, X2:state]:(fexec @ X59 @ fbody @ X2=>![X25:a]:(~((fpa @ X25 @ X59=>~((X59)=(fx))))=>fqa @ X25 @ X2))=>~(![X60:a, X2:state]:(~((fpa @ X60 @ X2=>~((X2)=(fx))))=>ftermi @ fbody @ X2)))), file('<stdin>', nax203)).
% 6.64/7.05 thf(ax225, axiom, p221, file('<stdin>', ax225)).
% 6.64/7.05 thf(ax229, axiom, p15, file('<stdin>', ax229)).
% 6.64/7.05 thf(ax20, axiom, (~(p201)|p202|~(p203)), file('<stdin>', ax20)).
% 6.64/7.05 thf(ax21, axiom, (p32|p201), file('<stdin>', ax21)).
% 6.64/7.05 thf(pax16, axiom, (p16=>![X94:state]:(fmember1389040324_state @ (fproduc64584659_state @ X94 @ fx) @ fr=>~((![X79:state, X95:state]:(fexec @ X79 @ fbody @ X95=>![X96:a]:(~((fpa @ X96 @ X79=>~((X79)=(X94))))=>fqa @ X96 @ X95))=>~(![X97:a, X95:state]:(~((fpa @ X97 @ X95=>~((X95)=(X94))))=>ftermi @ fbody @ X95)))))), file('<stdin>', pax16)).
% 6.64/7.05 thf(pax202, axiom, (p202=>(![X61:state, X2:state]:(fexec @ X61 @ fbody @ X2=>![X25:a]:(~((fpa @ X25 @ X61=>~(fmember1389040324_state @ (fproduc64584659_state @ X61 @ fx) @ fr)))=>fqa @ X25 @ X2))=>~(![X62:a, X2:state]:(~((fpa @ X62 @ X2=>~(fmember1389040324_state @ (fproduc64584659_state @ X2 @ fx) @ fr)))=>ftermi @ fbody @ X2)))), file('<stdin>', pax202)).
% 6.64/7.05 thf(ax228, axiom, p16, file('<stdin>', ax228)).
% 6.64/7.05 thf(c_0_14, plain, (~p220|(f__4)=(fx)), inference(fof_nnf,[status(thm)],[pax220])).
% 6.64/7.05 thf(c_0_15, plain, (~p221|fpa @ f__3 @ f__4), inference(fof_nnf,[status(thm)],[pax221])).
% 6.64/7.05 thf(c_0_16, plain, ((f__4)=(fx)|~p220), inference(split_conjunct,[status(thm)],[c_0_14])).
% 6.64/7.05 thf(c_0_17, plain, p220, inference(split_conjunct,[status(thm)],[ax226])).
% 6.64/7.05 thf(c_0_18, plain, (~ftermi @ fbody @ f__4|p219), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax219])])).
% 6.64/7.05 thf(c_0_19, plain, ~p219, inference(fof_simplification,[status(thm)],[ax227])).
% 6.64/7.05 thf(c_0_20, plain, (~p15|~p32), inference(fof_simplification,[status(thm)],[ax210])).
% 6.64/7.05 thf(c_0_21, plain, ![X252:state, X253:state, X254:a, X255:a, X256:state]:((~fexec @ X252 @ fbody @ X253|(~fpa @ X254 @ X252|(X252)!=(fx)|fqa @ X254 @ X253)|p203)&(~fpa @ X255 @ X256|(X256)!=(fx)|ftermi @ fbody @ X256|p203)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax203])])])])])).
% 6.64/7.05 thf(c_0_22, plain, (fpa @ f__3 @ f__4|~p221), inference(split_conjunct,[status(thm)],[c_0_15])).
% 6.64/7.05 thf(c_0_23, plain, (f__4)=(fx), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_17])])).
% 6.64/7.05 thf(c_0_24, plain, p221, inference(split_conjunct,[status(thm)],[ax225])).
% 6.64/7.05 thf(c_0_25, plain, (p219|~ftermi @ fbody @ f__4), inference(split_conjunct,[status(thm)],[c_0_18])).
% 6.64/7.05 thf(c_0_26, plain, ~p219, inference(split_conjunct,[status(thm)],[c_0_19])).
% 6.64/7.05 thf(c_0_27, plain, (~p15|~p32), inference(split_conjunct,[status(thm)],[c_0_20])).
% 6.64/7.05 thf(c_0_28, plain, p15, inference(split_conjunct,[status(thm)],[ax229])).
% 6.64/7.05 thf(c_0_29, plain, (~p201|p202|~p203), inference(fof_simplification,[status(thm)],[ax20])).
% 6.64/7.05 thf(c_0_30, plain, ![X3:a, X1:state]:(ftermi @ fbody @ X1|p203|~fpa @ X3 @ X1|(X1)!=(fx)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 6.64/7.05 thf(c_0_31, plain, fpa @ f__3 @ fx, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23]), c_0_24])])).
% 6.64/7.05 thf(c_0_32, plain, ~ftermi @ fbody @ fx, inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_23]), c_0_26])).
% 6.64/7.05 thf(c_0_33, plain, (p32|p201), inference(split_conjunct,[status(thm)],[ax21])).
% 6.64/7.05 thf(c_0_34, plain, ~p32, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_28])])).
% 6.64/7.05 thf(c_0_35, plain, ![X381:state, X382:state, X383:state, X384:a, X385:a, X386:state]:((~fexec @ X382 @ fbody @ X383|(~fpa @ X384 @ X382|(X382)!=(X381)|fqa @ X384 @ X383)|~fmember1389040324_state @ (fproduc64584659_state @ X381 @ fx) @ fr|~p16)&(~fpa @ X385 @ X386|(X386)!=(X381)|ftermi @ fbody @ X386|~fmember1389040324_state @ (fproduc64584659_state @ X381 @ fx) @ fr|~p16)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax16])])])])])).
% 6.64/7.05 thf(c_0_36, plain, ((((fpa @ esk77_0 @ esk78_0|fexec @ esk74_0 @ fbody @ esk75_0|~p202)&(fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fexec @ esk74_0 @ fbody @ esk75_0|~p202))&(~ftermi @ fbody @ esk78_0|fexec @ esk74_0 @ fbody @ esk75_0|~p202))&(((((fpa @ esk77_0 @ esk78_0|fpa @ esk76_0 @ esk74_0|~p202)&(fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fpa @ esk76_0 @ esk74_0|~p202))&(~ftermi @ fbody @ esk78_0|fpa @ esk76_0 @ esk74_0|~p202))&(((fpa @ esk77_0 @ esk78_0|fmember1389040324_state @ (fproduc64584659_state @ esk74_0 @ fx) @ fr|~p202)&(fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fmember1389040324_state @ (fproduc64584659_state @ esk74_0 @ fx) @ fr|~p202))&(~ftermi @ fbody @ esk78_0|fmember1389040324_state @ (fproduc64584659_state @ esk74_0 @ fx) @ fr|~p202)))&(((fpa @ esk77_0 @ esk78_0|~fqa @ esk76_0 @ esk75_0|~p202)&(fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|~fqa @ esk76_0 @ esk75_0|~p202))&(~ftermi @ fbody @ esk78_0|~fqa @ esk76_0 @ esk75_0|~p202)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax202])])])])])).
% 6.64/7.05 thf(c_0_37, plain, (p202|~p201|~p203), inference(split_conjunct,[status(thm)],[c_0_29])).
% 6.64/7.05 thf(c_0_38, plain, p203, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_32])).
% 6.64/7.05 thf(c_0_39, plain, p201, inference(sr,[status(thm)],[c_0_33, c_0_34])).
% 6.64/7.05 thf(c_0_40, plain, ![X1:state, X2:state, X3:a, X5:state]:(fqa @ X3 @ X2|~fexec @ X1 @ fbody @ X2|~fpa @ X3 @ X1|(X1)!=(X5)|~fmember1389040324_state @ (fproduc64584659_state @ X5 @ fx) @ fr|~p16), inference(split_conjunct,[status(thm)],[c_0_35])).
% 6.64/7.05 thf(c_0_41, plain, p16, inference(split_conjunct,[status(thm)],[ax228])).
% 6.64/7.05 thf(c_0_42, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk74_0 @ fx) @ fr|~ftermi @ fbody @ esk78_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_43, plain, p202, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])]), c_0_39])])).
% 6.64/7.05 thf(c_0_44, plain, (~ftermi @ fbody @ esk78_0|~fqa @ esk76_0 @ esk75_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_45, plain, ![X1:state, X3:a, X2:state]:(fqa @ X3 @ X1|~fmember1389040324_state @ (fproduc64584659_state @ X2 @ fx) @ fr|~fexec @ X2 @ fbody @ X1|~fpa @ X3 @ X2), inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_41])])])).
% 6.64/7.05 thf(c_0_46, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk74_0 @ fx) @ fr|~ftermi @ fbody @ esk78_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_43])])).
% 6.64/7.05 thf(c_0_47, plain, (fpa @ esk76_0 @ esk74_0|~ftermi @ fbody @ esk78_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_48, plain, (fexec @ esk74_0 @ fbody @ esk75_0|~ftermi @ fbody @ esk78_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_49, plain, ![X1:state, X3:a, X2:state]:(ftermi @ fbody @ X1|~fpa @ X3 @ X1|(X1)!=(X2)|~fmember1389040324_state @ (fproduc64584659_state @ X2 @ fx) @ fr|~p16), inference(split_conjunct,[status(thm)],[c_0_35])).
% 6.64/7.05 thf(c_0_50, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fexec @ esk74_0 @ fbody @ esk75_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_51, plain, (~ftermi @ fbody @ esk78_0|~fqa @ esk76_0 @ esk75_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_43])])).
% 6.64/7.05 thf(c_0_52, plain, ![X1:state, X3:a]:(fqa @ X3 @ X1|~fexec @ esk74_0 @ fbody @ X1|~ftermi @ fbody @ esk78_0|~fpa @ X3 @ esk74_0), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 6.64/7.05 thf(c_0_53, plain, (fpa @ esk76_0 @ esk74_0|~ftermi @ fbody @ esk78_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_43])])).
% 6.64/7.05 thf(c_0_54, plain, (fexec @ esk74_0 @ fbody @ esk75_0|~ftermi @ fbody @ esk78_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_43])])).
% 6.64/7.05 thf(c_0_55, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fmember1389040324_state @ (fproduc64584659_state @ esk74_0 @ fx) @ fr|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_56, plain, ![X3:a, X1:state]:(ftermi @ fbody @ X1|~fmember1389040324_state @ (fproduc64584659_state @ X1 @ fx) @ fr|~fpa @ X3 @ X1), inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_41])])])).
% 6.64/7.05 thf(c_0_57, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fexec @ esk74_0 @ fbody @ esk75_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_43])])).
% 6.64/7.05 thf(c_0_58, plain, ~ftermi @ fbody @ esk78_0, inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_53]), c_0_54])).
% 6.64/7.05 thf(c_0_59, plain, (fpa @ esk77_0 @ esk78_0|fexec @ esk74_0 @ fbody @ esk75_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_60, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fpa @ esk76_0 @ esk74_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_61, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk74_0 @ fx) @ fr|fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_43])])).
% 6.64/7.05 thf(c_0_62, plain, ![X3:a]:(fexec @ esk74_0 @ fbody @ esk75_0|~fpa @ X3 @ esk78_0), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_57]), c_0_58])).
% 6.64/7.05 thf(c_0_63, plain, (fexec @ esk74_0 @ fbody @ esk75_0|fpa @ esk77_0 @ esk78_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_43])])).
% 6.64/7.05 thf(c_0_64, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fpa @ esk76_0 @ esk74_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_43])])).
% 6.64/7.05 thf(c_0_65, plain, (fpa @ esk77_0 @ esk78_0|fpa @ esk76_0 @ esk74_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_66, plain, (fpa @ esk77_0 @ esk78_0|fmember1389040324_state @ (fproduc64584659_state @ esk74_0 @ fx) @ fr|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_67, plain, ![X1:state, X3:a]:(fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fqa @ X3 @ X1|~fexec @ esk74_0 @ fbody @ X1|~fpa @ X3 @ esk74_0), inference(spm,[status(thm)],[c_0_45, c_0_61])).
% 6.64/7.05 thf(c_0_68, plain, fexec @ esk74_0 @ fbody @ esk75_0, inference(spm,[status(thm)],[c_0_62, c_0_63])).
% 6.64/7.05 thf(c_0_69, plain, ![X3:a]:(fpa @ esk76_0 @ esk74_0|~fpa @ X3 @ esk78_0), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_64]), c_0_58])).
% 6.64/7.05 thf(c_0_70, plain, (fpa @ esk76_0 @ esk74_0|fpa @ esk77_0 @ esk78_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_43])])).
% 6.64/7.05 thf(c_0_71, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|~fqa @ esk76_0 @ esk75_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_72, plain, (fpa @ esk77_0 @ esk78_0|~fqa @ esk76_0 @ esk75_0|~p202), inference(split_conjunct,[status(thm)],[c_0_36])).
% 6.64/7.05 thf(c_0_73, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk74_0 @ fx) @ fr|fpa @ esk77_0 @ esk78_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_43])])).
% 6.64/7.05 thf(c_0_74, plain, ![X3:a]:(fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|fqa @ X3 @ esk75_0|~fpa @ X3 @ esk74_0), inference(spm,[status(thm)],[c_0_67, c_0_68])).
% 6.64/7.05 thf(c_0_75, plain, fpa @ esk76_0 @ esk74_0, inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 6.64/7.05 thf(c_0_76, plain, (fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr|~fqa @ esk76_0 @ esk75_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_43])])).
% 6.64/7.05 thf(c_0_77, plain, (fpa @ esk77_0 @ esk78_0|~fqa @ esk76_0 @ esk75_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_43])])).
% 6.64/7.05 thf(c_0_78, plain, ![X1:state, X3:a]:(fpa @ esk77_0 @ esk78_0|fqa @ X3 @ X1|~fexec @ esk74_0 @ fbody @ X1|~fpa @ X3 @ esk74_0), inference(spm,[status(thm)],[c_0_45, c_0_73])).
% 6.64/7.05 thf(c_0_79, plain, fmember1389040324_state @ (fproduc64584659_state @ esk78_0 @ fx) @ fr, inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_74, c_0_75]), c_0_76])).
% 6.64/7.05 thf(c_0_80, plain, fpa @ esk77_0 @ esk78_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_78]), c_0_68]), c_0_75])])).
% 6.64/7.05 thf(c_0_81, plain, ![X3:a]:~fpa @ X3 @ esk78_0, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_79]), c_0_58])).
% 6.64/7.05 thf(c_0_82, plain, ($false), inference(sr,[status(thm)],[c_0_80, c_0_81]), ['proof']).
% 6.64/7.05 thf(8,plain,$false,inference(eprover,[status(thm),assumptions([h16,h17,h14,h15,h13,h12,h2,h0])],[])).
% 6.64/7.05 thf(9,plain,$false,inference(tab_negimp,[status(thm),assumptions([h14,h15,h13,h12,h2,h0]),tab_negimp(discharge,[h16,h17])],[h14,8,h16,h17])).
% 6.64/7.05 thf(10,plain,$false,inference(tab_negimp,[status(thm),assumptions([h13,h12,h2,h0]),tab_negimp(discharge,[h14,h15])],[h13,9,h14,h15])).
% 6.64/7.05 thf(11,plain,$false,inference(tab_negall,[status(thm),assumptions([h12,h2,h0]),tab_negall(discharge,[h13]),tab_negall(eigenvar,eigen__4)],[h12,10,h13])).
% 6.64/7.05 thf(12,plain,$false,inference(tab_negall,[status(thm),assumptions([h2,h0]),tab_negall(discharge,[h12]),tab_negall(eigenvar,eigen__3)],[h2,11,h12])).
% 6.64/7.05 thf(13,plain,$false,inference(tab_imp,[status(thm),assumptions([h0]),tab_imp(discharge,[h1]),tab_imp(discharge,[h2])],[h0,7,12,h1,h2])).
% 6.64/7.05 thf(0,theorem,(~(((![X1:state]:(![X2:state]:((((exec @ X1) @ body) @ X2) => (![X3:a]:((~((((pa @ X3) @ X1) => (~((X1 = x)))))) => ((qa @ X3) @ X2)))))) => (~((![X1:a]:(![X2:state]:((~((((pa @ X1) @ X2) => (~((X2 = x)))))) => ((termi @ body) @ X2))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[13,h0])).
% 6.64/7.05 % SZS output end Proof
%------------------------------------------------------------------------------