%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP032^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 : 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 : Thu Oct 9 01:46:45 PM UTC 2025
% Result : Theorem 171.38s 171.10s
% Output : Proof 171.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ITP032^1 : TPTP v9.2.0. Released v7.5.0.
% 0.11/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.34 % Computer : n007.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Oct 8 18:14:23 EDT 2025
% 0.14/0.34 % CPUTime :
% 171.38/171.10 % SZS status Theorem
% 171.38/171.10 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 171.38/171.10 % Inferences: 37
% 171.38/171.10 % SZS output start Proof
% 171.38/171.10 thf(conj_0,conjecture,((ord_less_int @ (h @ w)) @ (h @ x))).
% 171.38/171.10 thf(h0,negated_conjecture,(~(((ord_less_int @ (h @ w)) @ (h @ x)))),inference(assume_negation,[status(cth)],[conj_0])).
% 171.38/171.10 thf(ax19, axiom, (~(p114)|p170), file('<stdin>', ax19)).
% 171.38/171.10 thf(ax20, axiom, (~(p170)|p169), file('<stdin>', ax20)).
% 171.38/171.10 thf(ax79, axiom, p114, file('<stdin>', ax79)).
% 171.38/171.10 thf(ax21, axiom, (~(p169)|p168), file('<stdin>', ax21)).
% 171.38/171.10 thf(pax125, axiom, (p125=>(fh @ fx)=(fh @ fe)), file('<stdin>', pax125)).
% 171.38/171.10 thf(ax5, axiom, (~(p162)|~(p131)|~(p161)), file('<stdin>', ax5)).
% 171.38/171.10 thf(ax22, axiom, (~(p168)|p162), file('<stdin>', ax22)).
% 171.38/171.10 thf(nax161, axiom, (p161<=(~((~((fbinary1721989714Tree_a @ fh @ ft1=>~(![X2:a]:(fmember_a @ X2 @ (fbinary945792244etOf_a @ ft1)=>ford_less_int @ (fh @ X2) @ (fh @ fx)))))=>~(![X2:a]:(fmember_a @ X2 @ (fbinary945792244etOf_a @ ft2)=>ford_less_int @ (fh @ fx) @ (fh @ X2)))))=>~(fbinary1721989714Tree_a @ fh @ ft2))), file('<stdin>', nax161)).
% 171.38/171.10 thf(ax68, axiom, p125, file('<stdin>', ax68)).
% 171.38/171.10 thf(ax62, axiom, p131, file('<stdin>', ax62)).
% 171.38/171.10 thf(pax132, axiom, (p132=>fmember_a @ fw @ (fbinary945792244etOf_a @ ft1)), file('<stdin>', pax132)).
% 171.38/171.10 thf(nax1, axiom, (p1<=ford_less_int @ (fh @ fw) @ (fh @ fx)), file('<stdin>', nax1)).
% 171.38/171.10 thf(ax192, axiom, ~(p1), file('<stdin>', ax192)).
% 171.38/171.10 thf(ax61, axiom, p132, file('<stdin>', ax61)).
% 171.38/171.10 thf(c_0_14, plain, (~p114|p170), inference(fof_simplification,[status(thm)],[ax19])).
% 171.38/171.10 thf(c_0_15, plain, (~p170|p169), inference(fof_simplification,[status(thm)],[ax20])).
% 171.38/171.10 thf(c_0_16, plain, (p170|~p114), inference(split_conjunct,[status(thm)],[c_0_14])).
% 171.38/171.10 thf(c_0_17, plain, p114, inference(split_conjunct,[status(thm)],[ax79])).
% 171.38/171.10 thf(c_0_18, plain, (~p169|p168), inference(fof_simplification,[status(thm)],[ax21])).
% 171.38/171.10 thf(c_0_19, plain, (p169|~p170), inference(split_conjunct,[status(thm)],[c_0_15])).
% 171.38/171.10 thf(c_0_20, plain, p170, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_17])])).
% 171.38/171.10 thf(c_0_21, plain, (~p125|(fh @ fx)=(fh @ fe)), inference(fof_nnf,[status(thm)],[pax125])).
% 171.38/171.10 thf(c_0_22, plain, (~p162|~p131|~p161), inference(fof_simplification,[status(thm)],[ax5])).
% 171.38/171.10 thf(c_0_23, plain, (~p168|p162), inference(fof_simplification,[status(thm)],[ax22])).
% 171.38/171.10 thf(c_0_24, plain, (p168|~p169), inference(split_conjunct,[status(thm)],[c_0_18])).
% 171.38/171.10 thf(c_0_25, plain, p169, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20])])).
% 171.38/171.10 thf(c_0_26, plain, ![X94:a, X95:a]:((((fbinary1721989714Tree_a @ fh @ ft1|p161)&(~fmember_a @ X94 @ (fbinary945792244etOf_a @ ft1)|ford_less_int @ (fh @ X94) @ (fh @ fx)|p161))&(~fmember_a @ X95 @ (fbinary945792244etOf_a @ ft2)|ford_less_int @ (fh @ fx) @ (fh @ X95)|p161))&(fbinary1721989714Tree_a @ fh @ ft2|p161)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax161])])])])])).
% 171.38/171.10 thf(c_0_27, plain, ((fh @ fx)=(fh @ fe)|~p125), inference(split_conjunct,[status(thm)],[c_0_21])).
% 171.38/171.10 thf(c_0_28, plain, p125, inference(split_conjunct,[status(thm)],[ax68])).
% 171.38/171.10 thf(c_0_29, plain, (~p162|~p131|~p161), inference(split_conjunct,[status(thm)],[c_0_22])).
% 171.38/171.10 thf(c_0_30, plain, p131, inference(split_conjunct,[status(thm)],[ax62])).
% 171.38/171.10 thf(c_0_31, plain, (p162|~p168), inference(split_conjunct,[status(thm)],[c_0_23])).
% 171.38/171.10 thf(c_0_32, plain, p168, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 171.38/171.10 thf(c_0_33, plain, ![X2:a]:(ford_less_int @ (fh @ X2) @ (fh @ fx)|p161|~fmember_a @ X2 @ (fbinary945792244etOf_a @ ft1)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 171.38/171.10 thf(c_0_34, plain, (fh @ fx)=(fh @ fe), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_28])])).
% 171.38/171.10 thf(c_0_35, plain, (~p161|~p162), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 171.38/171.10 thf(c_0_36, plain, p162, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 171.38/171.10 thf(c_0_37, plain, (~p132|fmember_a @ fw @ (fbinary945792244etOf_a @ ft1)), inference(fof_nnf,[status(thm)],[pax132])).
% 171.38/171.10 thf(c_0_38, plain, (~ford_less_int @ (fh @ fw) @ (fh @ fx)|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 171.38/171.10 thf(c_0_39, plain, ~p1, inference(fof_simplification,[status(thm)],[ax192])).
% 171.38/171.10 thf(c_0_40, plain, ![X2:a]:(ford_less_int @ (fh @ X2) @ (fh @ fe)|p161|~fmember_a @ X2 @ (fbinary945792244etOf_a @ ft1)), inference(rw,[status(thm)],[c_0_33, c_0_34])).
% 171.38/171.10 thf(c_0_41, plain, ~p161, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 171.38/171.10 thf(c_0_42, plain, (fmember_a @ fw @ (fbinary945792244etOf_a @ ft1)|~p132), inference(split_conjunct,[status(thm)],[c_0_37])).
% 171.38/171.10 thf(c_0_43, plain, p132, inference(split_conjunct,[status(thm)],[ax61])).
% 171.38/171.10 thf(c_0_44, plain, (p1|~ford_less_int @ (fh @ fw) @ (fh @ fx)), inference(split_conjunct,[status(thm)],[c_0_38])).
% 171.38/171.10 thf(c_0_45, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_39])).
% 171.38/171.10 thf(c_0_46, plain, ![X2:a]:(ford_less_int @ (fh @ X2) @ (fh @ fe)|~fmember_a @ X2 @ (fbinary945792244etOf_a @ ft1)), inference(sr,[status(thm)],[c_0_40, c_0_41])).
% 171.38/171.10 thf(c_0_47, plain, fmember_a @ fw @ (fbinary945792244etOf_a @ ft1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_43])])).
% 171.38/171.10 thf(c_0_48, plain, ~ford_less_int @ (fh @ fw) @ (fh @ fe), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_34]), c_0_45])).
% 171.38/171.10 thf(c_0_49, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_47]), c_0_48]), ['proof']).
% 171.38/171.10 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 171.38/171.10 thf(0,theorem,((ord_less_int @ (h @ w)) @ (h @ x)),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 171.38/171.10 % SZS output end Proof
%------------------------------------------------------------------------------