%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP120^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 : n008.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:01 PM UTC 2025
% Result : Theorem 167.29s 164.50s
% Output : Proof 167.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ITP120^1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.34 % Computer : n008.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:10:08 EDT 2025
% 0.14/0.35 % CPUTime :
% 167.29/164.50 % SZS status Theorem
% 167.29/164.50 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 167.29/164.50 % Inferences: 0
% 167.29/164.50 % SZS output start Proof
% 167.29/164.50 thf(conj_1,conjecture,(((inf @ (((((modula17988509_aux_a @ inf) @ sup) @ b) @ c) @ a2)) @ (((((modula581031071_aux_a @ inf) @ sup) @ a2) @ b) @ c)) = (((((modula1936294176_aux_a @ inf) @ sup) @ a2) @ b) @ c))).
% 167.29/164.50 thf(h0,negated_conjecture,(~((((inf @ (((((modula17988509_aux_a @ inf) @ sup) @ b) @ c) @ a2)) @ (((((modula581031071_aux_a @ inf) @ sup) @ a2) @ b) @ c)) = (((((modula1936294176_aux_a @ inf) @ sup) @ a2) @ b) @ c)))),inference(assume_negation,[status(cth)],[conj_1])).
% 167.29/164.50 thf(pax17, axiom, (p17=>![X8:a, X2:a, X3:a]:(fmodula581031071_aux_a @ finf @ fsup @ X8 @ X2 @ X3)=(fmodula17988509_aux_a @ finf @ fsup @ X3 @ X8 @ X2)), file('<stdin>', pax17)).
% 167.29/164.50 thf(pax10, axiom, (p10=>![X8:a, X2:a, X3:a]:(fmodula1373251614_aux_a @ finf @ fsup @ X8 @ X2 @ X3)=(fmodula17988509_aux_a @ finf @ fsup @ X2 @ X3 @ X8)), file('<stdin>', pax10)).
% 167.29/164.50 thf(nax1, axiom, (p1<=(finf @ (fmodula17988509_aux_a @ finf @ fsup @ fb @ fc @ fa2) @ (fmodula581031071_aux_a @ finf @ fsup @ fa2 @ fb @ fc))=(fmodula1936294176_aux_a @ finf @ fsup @ fa2 @ fb @ fc)), file('<stdin>', nax1)).
% 167.29/164.50 thf(ax35, axiom, p17, file('<stdin>', ax35)).
% 167.29/164.50 thf(ax51, axiom, ~(p1), file('<stdin>', ax51)).
% 167.29/164.50 thf(pax8, axiom, (p8=>![X8:a, X2:a, X3:a]:(fless_eq @ (fmodula1936294176_aux_a @ finf @ fsup @ X8 @ X2 @ X3) @ (fmodula1144073633_aux_a @ finf @ fsup @ X8 @ X2 @ X3)=>(finf @ (fmodula17988509_aux_a @ finf @ fsup @ X8 @ X2 @ X3) @ (fmodula1373251614_aux_a @ finf @ fsup @ X8 @ X2 @ X3))=(fmodula1936294176_aux_a @ finf @ fsup @ X8 @ X2 @ X3))), file('<stdin>', pax8)).
% 167.29/164.50 thf(ax42, axiom, p10, file('<stdin>', ax42)).
% 167.29/164.50 thf(pax35, axiom, (p35=>![X8:a, X2:a, X3:a]:(fmodula1936294176_aux_a @ finf @ fsup @ X8 @ X2 @ X3)=(fmodula1936294176_aux_a @ finf @ fsup @ X3 @ X8 @ X2)), file('<stdin>', pax35)).
% 167.29/164.50 thf(pax29, axiom, (p29=>![X8:a, X2:a, X3:a]:(fmodula1144073633_aux_a @ finf @ fsup @ X8 @ X2 @ X3)=(fmodula1144073633_aux_a @ finf @ fsup @ X3 @ X8 @ X2)), file('<stdin>', pax29)).
% 167.29/164.50 thf(pax2, axiom, (p2=>fless_eq @ (fmodula1936294176_aux_a @ finf @ fsup @ fa2 @ fb @ fc) @ (fmodula1144073633_aux_a @ finf @ fsup @ fa2 @ fb @ fc)), file('<stdin>', pax2)).
% 167.29/164.50 thf(ax44, axiom, p8, file('<stdin>', ax44)).
% 167.29/164.50 thf(ax17, axiom, p35, file('<stdin>', ax17)).
% 167.29/164.50 thf(ax23, axiom, p29, file('<stdin>', ax23)).
% 167.29/164.50 thf(ax50, axiom, p2, file('<stdin>', ax50)).
% 167.29/164.50 thf(c_0_14, plain, ![X215:a, X216:a, X217:a]:(~p17|(fmodula581031071_aux_a @ finf @ fsup @ X215 @ X216 @ X217)=(fmodula17988509_aux_a @ finf @ fsup @ X217 @ X215 @ X216)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax17])])])).
% 167.29/164.50 thf(c_0_15, plain, ![X241:a, X242:a, X243:a]:(~p10|(fmodula1373251614_aux_a @ finf @ fsup @ X241 @ X242 @ X243)=(fmodula17988509_aux_a @ finf @ fsup @ X242 @ X243 @ X241)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax10])])])).
% 167.29/164.50 thf(c_0_16, plain, ((finf @ (fmodula17988509_aux_a @ finf @ fsup @ fb @ fc @ fa2) @ (fmodula581031071_aux_a @ finf @ fsup @ fa2 @ fb @ fc))!=(fmodula1936294176_aux_a @ finf @ fsup @ fa2 @ fb @ fc)|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 167.29/164.50 thf(c_0_17, plain, ![X1:a, X3:a, X2:a]:((fmodula581031071_aux_a @ finf @ fsup @ X1 @ X2 @ X3)=(fmodula17988509_aux_a @ finf @ fsup @ X3 @ X1 @ X2)|~p17), inference(split_conjunct,[status(thm)],[c_0_14])).
% 167.29/164.50 thf(c_0_18, plain, p17, inference(split_conjunct,[status(thm)],[ax35])).
% 167.29/164.50 thf(c_0_19, plain, ~p1, inference(fof_simplification,[status(thm)],[ax51])).
% 167.29/164.50 thf(c_0_20, plain, ![X253:a, X254:a, X255:a]:(~p8|(~fless_eq @ (fmodula1936294176_aux_a @ finf @ fsup @ X253 @ X254 @ X255) @ (fmodula1144073633_aux_a @ finf @ fsup @ X253 @ X254 @ X255)|(finf @ (fmodula17988509_aux_a @ finf @ fsup @ X253 @ X254 @ X255) @ (fmodula1373251614_aux_a @ finf @ fsup @ X253 @ X254 @ X255))=(fmodula1936294176_aux_a @ finf @ fsup @ X253 @ X254 @ X255))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax8])])])).
% 167.29/164.50 thf(c_0_21, plain, ![X3:a, X2:a, X1:a]:((fmodula1373251614_aux_a @ finf @ fsup @ X1 @ X2 @ X3)=(fmodula17988509_aux_a @ finf @ fsup @ X2 @ X3 @ X1)|~p10), inference(split_conjunct,[status(thm)],[c_0_15])).
% 167.29/164.50 thf(c_0_22, plain, p10, inference(split_conjunct,[status(thm)],[ax42])).
% 167.29/164.50 thf(c_0_23, plain, ![X127:a, X128:a, X129:a]:(~p35|(fmodula1936294176_aux_a @ finf @ fsup @ X127 @ X128 @ X129)=(fmodula1936294176_aux_a @ finf @ fsup @ X129 @ X127 @ X128)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax35])])])).
% 167.29/164.50 thf(c_0_24, plain, ![X163:a, X164:a, X165:a]:(~p29|(fmodula1144073633_aux_a @ finf @ fsup @ X163 @ X164 @ X165)=(fmodula1144073633_aux_a @ finf @ fsup @ X165 @ X163 @ X164)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax29])])])).
% 167.29/164.50 thf(c_0_25, plain, (~p2|fless_eq @ (fmodula1936294176_aux_a @ finf @ fsup @ fa2 @ fb @ fc) @ (fmodula1144073633_aux_a @ finf @ fsup @ fa2 @ fb @ fc)), inference(fof_nnf,[status(thm)],[pax2])).
% 167.29/164.50 thf(c_0_26, plain, (p1|(finf @ (fmodula17988509_aux_a @ finf @ fsup @ fb @ fc @ fa2) @ (fmodula581031071_aux_a @ finf @ fsup @ fa2 @ fb @ fc))!=(fmodula1936294176_aux_a @ finf @ fsup @ fa2 @ fb @ fc)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 167.29/164.50 thf(c_0_27, plain, ![X1:a, X3:a, X2:a]:(fmodula581031071_aux_a @ finf @ fsup @ X1 @ X2 @ X3)=(fmodula17988509_aux_a @ finf @ fsup @ X3 @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])])).
% 167.29/164.50 thf(c_0_28, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_19])).
% 167.29/164.50 thf(c_0_29, plain, ![X1:a, X2:a, X3:a]:((finf @ (fmodula17988509_aux_a @ finf @ fsup @ X1 @ X2 @ X3) @ (fmodula1373251614_aux_a @ finf @ fsup @ X1 @ X2 @ X3))=(fmodula1936294176_aux_a @ finf @ fsup @ X1 @ X2 @ X3)|~p8|~fless_eq @ (fmodula1936294176_aux_a @ finf @ fsup @ X1 @ X2 @ X3) @ (fmodula1144073633_aux_a @ finf @ fsup @ X1 @ X2 @ X3)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 167.29/164.50 thf(c_0_30, plain, ![X3:a, X2:a, X1:a]:(fmodula1373251614_aux_a @ finf @ fsup @ X1 @ X2 @ X3)=(fmodula17988509_aux_a @ finf @ fsup @ X2 @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 167.29/164.50 thf(c_0_31, plain, p8, inference(split_conjunct,[status(thm)],[ax44])).
% 167.29/164.50 thf(c_0_32, plain, ![X1:a, X3:a, X2:a]:((fmodula1936294176_aux_a @ finf @ fsup @ X1 @ X2 @ X3)=(fmodula1936294176_aux_a @ finf @ fsup @ X3 @ X1 @ X2)|~p35), inference(split_conjunct,[status(thm)],[c_0_23])).
% 167.29/164.50 thf(c_0_33, plain, p35, inference(split_conjunct,[status(thm)],[ax17])).
% 167.29/164.50 thf(c_0_34, plain, ![X1:a, X3:a, X2:a]:((fmodula1144073633_aux_a @ finf @ fsup @ X1 @ X2 @ X3)=(fmodula1144073633_aux_a @ finf @ fsup @ X3 @ X1 @ X2)|~p29), inference(split_conjunct,[status(thm)],[c_0_24])).
% 167.29/164.50 thf(c_0_35, plain, p29, inference(split_conjunct,[status(thm)],[ax23])).
% 167.29/164.50 thf(c_0_36, plain, (fless_eq @ (fmodula1936294176_aux_a @ finf @ fsup @ fa2 @ fb @ fc) @ (fmodula1144073633_aux_a @ finf @ fsup @ fa2 @ fb @ fc)|~p2), inference(split_conjunct,[status(thm)],[c_0_25])).
% 167.29/164.50 thf(c_0_37, plain, p2, inference(split_conjunct,[status(thm)],[ax50])).
% 167.29/164.50 thf(c_0_38, plain, (finf @ (fmodula17988509_aux_a @ finf @ fsup @ fb @ fc @ fa2) @ (fmodula17988509_aux_a @ finf @ fsup @ fc @ fa2 @ fb))!=(fmodula1936294176_aux_a @ finf @ fsup @ fa2 @ fb @ fc), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27]), c_0_28])).
% 167.29/164.50 thf(c_0_39, plain, ![X1:a, X2:a, X3:a]:((finf @ (fmodula17988509_aux_a @ finf @ fsup @ X1 @ X2 @ X3) @ (fmodula17988509_aux_a @ finf @ fsup @ X2 @ X3 @ X1))=(fmodula1936294176_aux_a @ finf @ fsup @ X1 @ X2 @ X3)|~fless_eq @ (fmodula1936294176_aux_a @ finf @ fsup @ X1 @ X2 @ X3) @ (fmodula1144073633_aux_a @ finf @ fsup @ X1 @ X2 @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30]), c_0_31])])).
% 167.29/164.50 thf(c_0_40, plain, ![X1:a, X3:a, X2:a]:(fmodula1936294176_aux_a @ finf @ fsup @ X1 @ X2 @ X3)=(fmodula1936294176_aux_a @ finf @ fsup @ X3 @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_32, c_0_33])])).
% 167.29/164.50 thf(c_0_41, plain, ![X1:a, X3:a, X2:a]:(fmodula1144073633_aux_a @ finf @ fsup @ X1 @ X2 @ X3)=(fmodula1144073633_aux_a @ finf @ fsup @ X3 @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35])])).
% 167.29/164.50 thf(c_0_42, plain, fless_eq @ (fmodula1936294176_aux_a @ finf @ fsup @ fa2 @ fb @ fc) @ (fmodula1144073633_aux_a @ finf @ fsup @ fa2 @ fb @ fc), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_37])])).
% 167.29/164.50 thf(c_0_43, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_40]), c_0_40]), c_0_41]), c_0_42])]), ['proof']).
% 167.29/164.50 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 167.29/164.50 thf(0,theorem,(((inf @ (((((modula17988509_aux_a @ inf) @ sup) @ b) @ c) @ a2)) @ (((((modula581031071_aux_a @ inf) @ sup) @ a2) @ b) @ c)) = (((((modula1936294176_aux_a @ inf) @ sup) @ a2) @ b) @ c)),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 167.29/164.50 % SZS output end Proof
%------------------------------------------------------------------------------