%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWC364+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n004.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 : Sat Jun 21 05:31:01 AM UTC 2025
% Result : Theorem 153.01s 153.32s
% Output : Proof 153.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWC364+1 : TPTP v9.0.0. Released v2.4.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.11/0.33 % Computer : n004.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 20 09:07:52 EDT 2025
% 0.11/0.33 % CPUTime :
% 153.01/153.32 % SZS status Theorem
% 153.01/153.32 % SZS output start Proof
% 153.01/153.32 tff(tptp_fun_V_46_type, type, (
% 153.01/153.32 tptp_fun_V_46: $i)).
% 153.01/153.32 tff(app_type, type, (
% 153.01/153.32 app: ( $i * $i ) > $i)).
% 153.01/153.32 tff(tptp_fun_W_5_type, type, (
% 153.01/153.32 tptp_fun_W_5: ( $i * $i ) > $i)).
% 153.01/153.32 tff(tptp_fun_X_8_type, type, (
% 153.01/153.32 tptp_fun_X_8: ( $i * $i ) > $i)).
% 153.01/153.32 tff(nil_type, type, (
% 153.01/153.32 nil: $i)).
% 153.01/153.32 tff(tptp_fun_U_45_type, type, (
% 153.01/153.32 tptp_fun_U_45: $i)).
% 153.01/153.32 tff(cons_type, type, (
% 153.01/153.32 cons: ( $i * $i ) > $i)).
% 153.01/153.32 tff(tptp_fun_Y_47_type, type, (
% 153.01/153.32 tptp_fun_Y_47: $i)).
% 153.01/153.32 tff(tptp_fun_W_7_type, type, (
% 153.01/153.32 tptp_fun_W_7: ( $i * $i ) > $i)).
% 153.01/153.32 tff(ssList_type, type, (
% 153.01/153.32 ssList: $i > $o)).
% 153.01/153.32 tff(segmentP_type, type, (
% 153.01/153.32 segmentP: ( $i * $i ) > $o)).
% 153.01/153.32 tff(neq_type, type, (
% 153.01/153.32 neq: ( $i * $i ) > $o)).
% 153.01/153.32 tff(ssItem_type, type, (
% 153.01/153.32 ssItem: $i > $o)).
% 153.01/153.32 tff(frontsegP_type, type, (
% 153.01/153.32 frontsegP: ( $i * $i ) > $o)).
% 153.01/153.32 tff(1,plain,
% 153.01/153.32 ((ssList(U!45) & ((~segmentP(V!46, U!45)) & ssList(V!46) & (~((~ssItem(Y!47)) | (~(app(cons(Y!47, nil), U!45) = V!46)))) & ssList(U!45) & neq(V!46, nil))) <=> (ssList(U!45) & (~segmentP(V!46, U!45)) & ssList(V!46) & (~((~ssItem(Y!47)) | (~(app(cons(Y!47, nil), U!45) = V!46)))) & neq(V!46, nil))),
% 153.01/153.32 inference(rewrite,[status(thm)],[])).
% 153.01/153.32 tff(2,plain,
% 153.01/153.32 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : (segmentP(V, U) | (~ssList(V)) | ![Y: $i] : ((~ssItem(Y)) | (~(app(cons(Y, nil), U) = V))) | (~ssList(U)) | (~neq(V, nil))))) <=> (~![U: $i] : ((~ssList(U)) | ![V: $i] : (segmentP(V, U) | (~ssList(V)) | ![Y: $i] : ((~ssItem(Y)) | (~(app(cons(Y, nil), U) = V))) | (~ssList(U)) | (~neq(V, nil)))))),
% 153.01/153.32 inference(rewrite,[status(thm)],[])).
% 153.01/153.32 tff(3,plain,
% 153.01/153.32 ((~![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (((~(V = X)) | (~(U = W))) | ((((~neq(V, nil)) | ![Y: $i] : (ssItem(Y) => (~(app(cons(Y, nil), W) = X)))) | segmentP(V, U)) & ((~neq(V, nil)) | neq(X, nil))))))))) <=> (~![U: $i] : ((~ssList(U)) | ![V: $i] : (segmentP(V, U) | (~ssList(V)) | ![Y: $i] : ((~ssItem(Y)) | (~(app(cons(Y, nil), U) = V))) | (~ssList(U)) | (~neq(V, nil)))))),
% 153.01/153.32 inference(rewrite,[status(thm)],[])).
% 153.01/153.32 tff(4,axiom,(~![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (((~(V = X)) | (~(U = W))) | ((((~neq(V, nil)) | ![Y: $i] : (ssItem(Y) => (~(app(cons(Y, nil), W) = X)))) | segmentP(V, U)) & ((~neq(V, nil)) | neq(X, nil))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','co1')).
% 153.01/153.32 tff(5,plain,
% 153.01/153.32 (~![U: $i] : ((~ssList(U)) | ![V: $i] : (segmentP(V, U) | (~ssList(V)) | ![Y: $i] : ((~ssItem(Y)) | (~(app(cons(Y, nil), U) = V))) | (~ssList(U)) | (~neq(V, nil))))),
% 153.01/153.32 inference(modus_ponens,[status(thm)],[4, 3])).
% 153.01/153.32 tff(6,plain,
% 153.01/153.32 (~![U: $i] : ((~ssList(U)) | ![V: $i] : (segmentP(V, U) | (~ssList(V)) | ![Y: $i] : ((~ssItem(Y)) | (~(app(cons(Y, nil), U) = V))) | (~ssList(U)) | (~neq(V, nil))))),
% 153.01/153.32 inference(modus_ponens,[status(thm)],[5, 2])).
% 153.01/153.32 tff(7,plain,
% 153.01/153.32 (~![U: $i] : ((~ssList(U)) | ![V: $i] : (segmentP(V, U) | (~ssList(V)) | ![Y: $i] : ((~ssItem(Y)) | (~(app(cons(Y, nil), U) = V))) | (~ssList(U)) | (~neq(V, nil))))),
% 153.01/153.32 inference(modus_ponens,[status(thm)],[6, 2])).
% 153.01/153.32 tff(8,plain,
% 153.01/153.32 (~![U: $i] : ((~ssList(U)) | ![V: $i] : (segmentP(V, U) | (~ssList(V)) | ![Y: $i] : ((~ssItem(Y)) | (~(app(cons(Y, nil), U) = V))) | (~ssList(U)) | (~neq(V, nil))))),
% 153.01/153.32 inference(modus_ponens,[status(thm)],[7, 2])).
% 153.01/153.32 tff(9,plain,
% 153.01/153.32 (ssList(U!45) & (~segmentP(V!46, U!45)) & ssList(V!46) & (~((~ssItem(Y!47)) | (~(app(cons(Y!47, nil), U!45) = V!46)))) & neq(V!46, nil)),
% 153.01/153.32 inference(modus_ponens,[status(thm)],[8, 1])).
% 153.01/153.32 tff(10,plain,
% 153.01/153.32 (ssList(V!46)),
% 153.01/153.32 inference(and_elim,[status(thm)],[9])).
% 153.01/153.32 tff(11,plain,
% 153.01/153.32 (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U)))))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U)))))))))))),
% 153.01/153.32 inference(bind,[status(th)],[])).
% 153.01/153.32 tff(12,plain,
% 153.01/153.32 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U)))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))),
% 153.01/153.32 inference(quant_intro,[status(thm)],[11])).
% 153.01/153.32 tff(13,plain,
% 153.01/153.32 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U)))))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U)))))))))))),
% 153.01/153.32 inference(bind,[status(th)],[])).
% 153.01/153.32 tff(14,plain,
% 153.01/153.32 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U)))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))),
% 153.01/153.32 inference(quant_intro,[status(thm)],[13])).
% 153.01/153.32 tff(15,plain,
% 153.01/153.32 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U)))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))),
% 153.01/153.32 inference(transitivity,[status(thm)],[14, 12])).
% 153.01/153.32 tff(16,plain,
% 153.01/153.32 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~segmentP(U, V)) | (ssList(tptp_fun_W_7(V, U)) & ssList(tptp_fun_X_8(V, U)) & (app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U))) & (segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (~(ssList(X) & (app(app(W, V), X) = U)))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U)))))))))))),
% 153.01/153.32 inference(bind,[status(th)],[])).
% 153.01/153.32 tff(17,plain,
% 153.01/153.32 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~segmentP(U, V)) | (ssList(tptp_fun_W_7(V, U)) & ssList(tptp_fun_X_8(V, U)) & (app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U))) & (segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (~(ssList(X) & (app(app(W, V), X) = U)))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))),
% 153.01/153.32 inference(quant_intro,[status(thm)],[16])).
% 153.01/153.32 tff(18,plain,
% 153.01/153.32 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~segmentP(U, V)) | (ssList(tptp_fun_W_7(V, U)) & (ssList(tptp_fun_X_8(V, U)) & (app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))) & (segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (~(ssList(X) & (app(app(W, V), X) = U)))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~segmentP(U, V)) | (ssList(tptp_fun_W_7(V, U)) & ssList(tptp_fun_X_8(V, U)) & (app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U))) & (segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (~(ssList(X) & (app(app(W, V), X) = U)))))))))),
% 153.01/153.32 inference(bind,[status(th)],[])).
% 153.01/153.32 tff(19,plain,
% 153.01/153.32 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~segmentP(U, V)) | (ssList(tptp_fun_W_7(V, U)) & (ssList(tptp_fun_X_8(V, U)) & (app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))) & (segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (~(ssList(X) & (app(app(W, V), X) = U)))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~segmentP(U, V)) | (ssList(tptp_fun_W_7(V, U)) & ssList(tptp_fun_X_8(V, U)) & (app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U))) & (segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (~(ssList(X) & (app(app(W, V), X) = U))))))))),
% 153.01/153.32 inference(quant_intro,[status(thm)],[18])).
% 153.01/153.32 tff(20,plain,
% 153.01/153.32 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))))),
% 153.01/153.32 inference(rewrite,[status(thm)],[])).
% 153.01/153.32 tff(21,plain,
% 153.01/153.32 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : trans(monotonicity(rewrite((segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U)))) <=> (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))), ((ssList(V) => (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))) <=> (ssList(V) => (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))))), rewrite((ssList(V) => (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))) <=> ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U)))))), ((ssList(V) => (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))) <=> ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U)))))))), (![V: $i] : (ssList(V) => (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))) <=> ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))))), ((ssList(U) => ![V: $i] : (ssList(V) => (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U)))))) <=> (ssList(U) => ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U)))))))), rewrite((ssList(U) => ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))))), ((ssList(U) => ![V: $i] : (ssList(V) => (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))))))),
% 153.01/153.33 inference(bind,[status(th)],[])).
% 153.01/153.33 tff(22,plain,
% 153.01/153.33 (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))))),
% 153.01/153.33 inference(quant_intro,[status(thm)],[21])).
% 153.01/153.33 tff(23,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax7')).
% 153.01/153.33 tff(24,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[23, 22])).
% 153.01/153.33 tff(25,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (segmentP(U, V) <=> ?[W: $i] : (ssList(W) & ?[X: $i] : (ssList(X) & (app(app(W, V), X) = U))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[24, 20])).
% 153.01/153.33 tff(26,plain,(
% 153.01/153.33 ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~segmentP(U, V)) | (ssList(tptp_fun_W_7(V, U)) & (ssList(tptp_fun_X_8(V, U)) & (app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))) & (segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (~(ssList(X) & (app(app(W, V), X) = U))))))))),
% 153.01/153.33 inference(skolemize,[status(sab)],[25])).
% 153.01/153.33 tff(27,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~segmentP(U, V)) | (ssList(tptp_fun_W_7(V, U)) & ssList(tptp_fun_X_8(V, U)) & (app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U))) & (segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (~(ssList(X) & (app(app(W, V), X) = U))))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[26, 19])).
% 153.01/153.33 tff(28,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[27, 17])).
% 153.01/153.33 tff(29,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[28, 15])).
% 153.01/153.33 tff(30,plain,
% 153.01/153.33 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))) | ((~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46))))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))) | (~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46))))))))))),
% 153.01/153.33 inference(rewrite,[status(thm)],[])).
% 153.01/153.33 tff(31,plain,
% 153.01/153.33 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))) | ((~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46))))))))))),
% 153.01/153.33 inference(quant_inst,[status(thm)],[])).
% 153.01/153.33 tff(32,plain,
% 153.01/153.33 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(U, V)) | (~((~ssList(tptp_fun_W_7(V, U))) | (~ssList(tptp_fun_X_8(V, U))) | (~(app(app(tptp_fun_W_7(V, U), V), tptp_fun_X_8(V, U)) = U)))))) | (~(segmentP(U, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = U))))))))))) | (~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[31, 30])).
% 153.01/153.33 tff(33,plain,
% 153.01/153.33 (![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))),
% 153.01/153.33 inference(unit_resolution,[status(thm)],[32, 29, 10])).
% 153.01/153.33 tff(34,plain,
% 153.01/153.33 (ssList(nil) <=> ssList(nil)),
% 153.01/153.33 inference(rewrite,[status(thm)],[])).
% 153.01/153.33 tff(35,axiom,(ssList(nil)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax17')).
% 153.01/153.33 tff(36,plain,
% 153.01/153.33 (ssList(nil)),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[35, 34])).
% 153.01/153.33 tff(37,plain,
% 153.01/153.33 (((~![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))) | ((~ssList(nil)) | (~((~((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))))) | (~(segmentP(V!46, nil) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, nil), X) = V!46)))))))))) <=> ((~![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))) | (~ssList(nil)) | (~((~((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))))) | (~(segmentP(V!46, nil) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, nil), X) = V!46)))))))))),
% 153.01/153.33 inference(rewrite,[status(thm)],[])).
% 153.01/153.33 tff(38,plain,
% 153.01/153.33 ((~![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))) | ((~ssList(nil)) | (~((~((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))))) | (~(segmentP(V!46, nil) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, nil), X) = V!46)))))))))),
% 153.01/153.33 inference(quant_inst,[status(thm)],[])).
% 153.01/153.33 tff(39,plain,
% 153.01/153.33 ((~![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))) | (~ssList(nil)) | (~((~((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))))) | (~(segmentP(V!46, nil) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, nil), X) = V!46))))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[38, 37])).
% 153.01/153.33 tff(40,plain,
% 153.01/153.33 (~((~((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))))) | (~(segmentP(V!46, nil) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, nil), X) = V!46)))))))),
% 153.01/153.33 inference(unit_resolution,[status(thm)],[39, 36, 33])).
% 153.01/153.33 tff(41,plain,
% 153.01/153.33 (((~((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))))) | (~(segmentP(V!46, nil) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, nil), X) = V!46))))))) | ((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))))),
% 153.01/153.33 inference(tautology,[status(thm)],[])).
% 153.01/153.33 tff(42,plain,
% 153.01/153.33 ((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46))))),
% 153.01/153.33 inference(unit_resolution,[status(thm)],[41, 40])).
% 153.01/153.33 tff(43,plain,
% 153.01/153.33 (^[U: $i] : refl(((~ssList(U)) | segmentP(U, nil)) <=> ((~ssList(U)) | segmentP(U, nil)))),
% 153.01/153.33 inference(bind,[status(th)],[])).
% 153.01/153.33 tff(44,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | segmentP(U, nil)) <=> ![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 153.01/153.33 inference(quant_intro,[status(thm)],[43])).
% 153.01/153.33 tff(45,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | segmentP(U, nil)) <=> ![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 153.01/153.33 inference(rewrite,[status(thm)],[])).
% 153.01/153.33 tff(46,plain,
% 153.01/153.33 (^[U: $i] : rewrite((ssList(U) => segmentP(U, nil)) <=> ((~ssList(U)) | segmentP(U, nil)))),
% 153.01/153.33 inference(bind,[status(th)],[])).
% 153.01/153.33 tff(47,plain,
% 153.01/153.33 (![U: $i] : (ssList(U) => segmentP(U, nil)) <=> ![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 153.01/153.33 inference(quant_intro,[status(thm)],[46])).
% 153.01/153.33 tff(48,axiom,(![U: $i] : (ssList(U) => segmentP(U, nil))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax57')).
% 153.01/153.33 tff(49,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[48, 47])).
% 153.01/153.33 tff(50,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[49, 45])).
% 153.01/153.33 tff(51,plain,(
% 153.01/153.33 ![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 153.01/153.33 inference(skolemize,[status(sab)],[50])).
% 153.01/153.33 tff(52,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[51, 44])).
% 153.01/153.33 tff(53,plain,
% 153.01/153.33 (((~![U: $i] : ((~ssList(U)) | segmentP(U, nil))) | ((~ssList(V!46)) | segmentP(V!46, nil))) <=> ((~![U: $i] : ((~ssList(U)) | segmentP(U, nil))) | (~ssList(V!46)) | segmentP(V!46, nil))),
% 153.01/153.33 inference(rewrite,[status(thm)],[])).
% 153.01/153.33 tff(54,plain,
% 153.01/153.33 ((~![U: $i] : ((~ssList(U)) | segmentP(U, nil))) | ((~ssList(V!46)) | segmentP(V!46, nil))),
% 153.01/153.33 inference(quant_inst,[status(thm)],[])).
% 153.01/153.33 tff(55,plain,
% 153.01/153.33 ((~![U: $i] : ((~ssList(U)) | segmentP(U, nil))) | (~ssList(V!46)) | segmentP(V!46, nil)),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[54, 53])).
% 153.01/153.33 tff(56,plain,
% 153.01/153.33 (segmentP(V!46, nil)),
% 153.01/153.33 inference(unit_resolution,[status(thm)],[55, 52, 10])).
% 153.01/153.33 tff(57,plain,
% 153.01/153.33 ((~((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))))) | (~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46))))),
% 153.01/153.33 inference(tautology,[status(thm)],[])).
% 153.01/153.33 tff(58,plain,
% 153.01/153.33 ((~((~segmentP(V!46, nil)) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))))) | (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46))))),
% 153.01/153.33 inference(unit_resolution,[status(thm)],[57, 56])).
% 153.01/153.33 tff(59,plain,
% 153.01/153.33 (~((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)))),
% 153.01/153.33 inference(unit_resolution,[status(thm)],[58, 42])).
% 153.01/153.33 tff(60,plain,
% 153.01/153.33 (((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46))) | (app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46)),
% 153.01/153.33 inference(tautology,[status(thm)],[])).
% 153.01/153.33 tff(61,plain,
% 153.01/153.33 (app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46),
% 153.01/153.33 inference(unit_resolution,[status(thm)],[60, 59])).
% 153.01/153.33 tff(62,plain,
% 153.01/153.33 (((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46))) | ssList(tptp_fun_X_8(nil, V!46))),
% 153.01/153.33 inference(tautology,[status(thm)],[])).
% 153.01/153.33 tff(63,plain,
% 153.01/153.33 (ssList(tptp_fun_X_8(nil, V!46))),
% 153.01/153.33 inference(unit_resolution,[status(thm)],[62, 59])).
% 153.01/153.33 tff(64,plain,
% 153.01/153.33 (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))))),
% 153.01/153.33 inference(bind,[status(th)],[])).
% 153.01/153.33 tff(65,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 153.01/153.33 inference(quant_intro,[status(thm)],[64])).
% 153.01/153.33 tff(66,plain,
% 153.01/153.33 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))))),
% 153.01/153.33 inference(bind,[status(th)],[])).
% 153.01/153.33 tff(67,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 153.01/153.33 inference(quant_intro,[status(thm)],[66])).
% 153.01/153.33 tff(68,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 153.01/153.33 inference(transitivity,[status(thm)],[67, 65])).
% 153.01/153.33 tff(69,plain,
% 153.01/153.33 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~frontsegP(U, V)) | (ssList(tptp_fun_W_5(V, U)) & (app(V, tptp_fun_W_5(V, U)) = U))) & (frontsegP(U, V) | ![W: $i] : (~(ssList(W) & (app(V, W) = U))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))))),
% 153.01/153.33 inference(bind,[status(th)],[])).
% 153.01/153.33 tff(70,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~frontsegP(U, V)) | (ssList(tptp_fun_W_5(V, U)) & (app(V, tptp_fun_W_5(V, U)) = U))) & (frontsegP(U, V) | ![W: $i] : (~(ssList(W) & (app(V, W) = U))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 153.01/153.33 inference(quant_intro,[status(thm)],[69])).
% 153.01/153.33 tff(71,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))),
% 153.01/153.33 inference(rewrite,[status(thm)],[])).
% 153.01/153.33 tff(72,plain,
% 153.01/153.33 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : trans(monotonicity(rewrite((frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))) <=> (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))), ((ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))) <=> (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))), rewrite((ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))) <=> ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))), ((ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))) <=> ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))))), (![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))) <=> ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> (ssList(U) => ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))))), rewrite((ssList(U) => ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))))),
% 153.01/153.33 inference(bind,[status(th)],[])).
% 153.01/153.33 tff(73,plain,
% 153.01/153.33 (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))),
% 153.01/153.33 inference(quant_intro,[status(thm)],[72])).
% 153.01/153.33 tff(74,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax5')).
% 153.01/153.33 tff(75,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[74, 73])).
% 153.01/153.33 tff(76,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[75, 71])).
% 153.01/153.33 tff(77,plain,(
% 153.01/153.33 ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~frontsegP(U, V)) | (ssList(tptp_fun_W_5(V, U)) & (app(V, tptp_fun_W_5(V, U)) = U))) & (frontsegP(U, V) | ![W: $i] : (~(ssList(W) & (app(V, W) = U)))))))),
% 153.01/153.33 inference(skolemize,[status(sab)],[76])).
% 153.01/153.33 tff(78,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[77, 70])).
% 153.01/153.33 tff(79,plain,
% 153.01/153.33 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[78, 68])).
% 153.01/153.33 tff(80,plain,
% 153.01/153.33 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | (~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))))))))))),
% 153.01/153.33 inference(rewrite,[status(thm)],[])).
% 153.01/153.33 tff(81,plain,
% 153.01/153.33 (((~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))) | (~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))))))) <=> ((~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))))))))))),
% 153.01/153.33 inference(rewrite,[status(thm)],[])).
% 153.01/153.33 tff(82,plain,
% 153.01/153.33 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))) | (~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46))))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))))),
% 153.01/153.33 inference(monotonicity,[status(thm)],[81])).
% 153.01/153.33 tff(83,plain,
% 153.01/153.33 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))) | (~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46))))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | (~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))))))))))),
% 153.01/153.33 inference(transitivity,[status(thm)],[82, 80])).
% 153.01/153.33 tff(84,plain,
% 153.01/153.33 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))) | (~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46))))))))))),
% 153.01/153.33 inference(quant_inst,[status(thm)],[])).
% 153.01/153.33 tff(85,plain,
% 153.01/153.33 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | (~ssList(tptp_fun_X_8(nil, V!46))) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))),
% 153.01/153.33 inference(modus_ponens,[status(thm)],[84, 83])).
% 153.01/153.33 tff(86,plain,
% 153.01/153.33 (![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))),
% 153.01/153.33 inference(unit_resolution,[status(thm)],[85, 79, 63])).
% 153.01/153.33 tff(87,plain,
% 153.01/153.33 (((~![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)) | ![W: $i] : ((~ssList(W)) | (~(app(tptp_fun_X_8(nil, V!46), W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))) <=> ((~![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)) | ![W: $i] : ((~ssList(W)) | (~(app(tptp_fun_X_8(nil, V!46), W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(88,plain,
% 153.01/153.34 ((~![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)) | ![W: $i] : ((~ssList(W)) | (~(app(tptp_fun_X_8(nil, V!46), W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))),
% 153.01/153.34 inference(quant_inst,[status(thm)],[])).
% 153.01/153.34 tff(89,plain,
% 153.01/153.34 ((~![V: $i] : ((~ssList(V)) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), V)) | (~((~ssList(tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46)))) | (~(app(V, tptp_fun_W_5(V, tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~((~(frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)) | ![W: $i] : ((~ssList(W)) | (~(app(tptp_fun_X_8(nil, V!46), W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))))))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[88, 87])).
% 153.01/153.34 tff(90,plain,
% 153.01/153.34 (~((~(frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)) | ![W: $i] : ((~ssList(W)) | (~(app(tptp_fun_X_8(nil, V!46), W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[89, 63, 86])).
% 153.01/153.34 tff(91,plain,
% 153.01/153.34 (((~(frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)) | ![W: $i] : ((~ssList(W)) | (~(app(tptp_fun_X_8(nil, V!46), W) = tptp_fun_X_8(nil, V!46)))))) | (~((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))))))) | ((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))),
% 153.01/153.34 inference(tautology,[status(thm)],[])).
% 153.01/153.34 tff(92,plain,
% 153.01/153.34 ((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[91, 90])).
% 153.01/153.34 tff(93,plain,
% 153.01/153.34 (^[U: $i] : refl(((~ssList(U)) | frontsegP(U, U)) <=> ((~ssList(U)) | frontsegP(U, U)))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(94,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | frontsegP(U, U)) <=> ![U: $i] : ((~ssList(U)) | frontsegP(U, U))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[93])).
% 153.01/153.34 tff(95,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | frontsegP(U, U)) <=> ![U: $i] : ((~ssList(U)) | frontsegP(U, U))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(96,plain,
% 153.01/153.34 (^[U: $i] : rewrite((ssList(U) => frontsegP(U, U)) <=> ((~ssList(U)) | frontsegP(U, U)))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(97,plain,
% 153.01/153.34 (![U: $i] : (ssList(U) => frontsegP(U, U)) <=> ![U: $i] : ((~ssList(U)) | frontsegP(U, U))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[96])).
% 153.01/153.34 tff(98,axiom,(![U: $i] : (ssList(U) => frontsegP(U, U))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax42')).
% 153.01/153.34 tff(99,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | frontsegP(U, U))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[98, 97])).
% 153.01/153.34 tff(100,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | frontsegP(U, U))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[99, 95])).
% 153.01/153.34 tff(101,plain,(
% 153.01/153.34 ![U: $i] : ((~ssList(U)) | frontsegP(U, U))),
% 153.01/153.34 inference(skolemize,[status(sab)],[100])).
% 153.01/153.34 tff(102,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | frontsegP(U, U))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[101, 94])).
% 153.01/153.34 tff(103,plain,
% 153.01/153.34 (((~![U: $i] : ((~ssList(U)) | frontsegP(U, U))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) <=> ((~![U: $i] : ((~ssList(U)) | frontsegP(U, U))) | (~ssList(tptp_fun_X_8(nil, V!46))) | frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(104,plain,
% 153.01/153.34 ((~![U: $i] : ((~ssList(U)) | frontsegP(U, U))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))),
% 153.01/153.34 inference(quant_inst,[status(thm)],[])).
% 153.01/153.34 tff(105,plain,
% 153.01/153.34 ((~![U: $i] : ((~ssList(U)) | frontsegP(U, U))) | (~ssList(tptp_fun_X_8(nil, V!46))) | frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[104, 103])).
% 153.01/153.34 tff(106,plain,
% 153.01/153.34 (frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[105, 102, 63])).
% 153.01/153.34 tff(107,plain,
% 153.01/153.34 ((~((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))) | (~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))))),
% 153.01/153.34 inference(tautology,[status(thm)],[])).
% 153.01/153.34 tff(108,plain,
% 153.01/153.34 ((~((~frontsegP(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))))) | (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[107, 106])).
% 153.01/153.34 tff(109,plain,
% 153.01/153.34 (~((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[108, 92])).
% 153.01/153.34 tff(110,plain,
% 153.01/153.34 (((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))) | (app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46))),
% 153.01/153.34 inference(tautology,[status(thm)],[])).
% 153.01/153.34 tff(111,plain,
% 153.01/153.34 (app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[110, 109])).
% 153.01/153.34 tff(112,plain,
% 153.01/153.34 (((~ssList(tptp_fun_W_7(nil, V!46))) | (~ssList(tptp_fun_X_8(nil, V!46))) | (~(app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = V!46))) | ssList(tptp_fun_W_7(nil, V!46))),
% 153.01/153.34 inference(tautology,[status(thm)],[])).
% 153.01/153.34 tff(113,plain,
% 153.01/153.34 (ssList(tptp_fun_W_7(nil, V!46))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[112, 59])).
% 153.01/153.34 tff(114,plain,
% 153.01/153.34 (^[U: $i] : refl(((~ssList(U)) | (app(U, nil) = U)) <=> ((~ssList(U)) | (app(U, nil) = U)))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(115,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | (app(U, nil) = U)) <=> ![U: $i] : ((~ssList(U)) | (app(U, nil) = U))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[114])).
% 153.01/153.34 tff(116,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | (app(U, nil) = U)) <=> ![U: $i] : ((~ssList(U)) | (app(U, nil) = U))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(117,plain,
% 153.01/153.34 (^[U: $i] : rewrite((ssList(U) => (app(U, nil) = U)) <=> ((~ssList(U)) | (app(U, nil) = U)))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(118,plain,
% 153.01/153.34 (![U: $i] : (ssList(U) => (app(U, nil) = U)) <=> ![U: $i] : ((~ssList(U)) | (app(U, nil) = U))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[117])).
% 153.01/153.34 tff(119,axiom,(![U: $i] : (ssList(U) => (app(U, nil) = U))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax84')).
% 153.01/153.34 tff(120,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | (app(U, nil) = U))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[119, 118])).
% 153.01/153.34 tff(121,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | (app(U, nil) = U))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[120, 116])).
% 153.01/153.34 tff(122,plain,(
% 153.01/153.34 ![U: $i] : ((~ssList(U)) | (app(U, nil) = U))),
% 153.01/153.34 inference(skolemize,[status(sab)],[121])).
% 153.01/153.34 tff(123,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | (app(U, nil) = U))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[122, 115])).
% 153.01/153.34 tff(124,plain,
% 153.01/153.34 (((~![U: $i] : ((~ssList(U)) | (app(U, nil) = U))) | ((~ssList(tptp_fun_W_7(nil, V!46))) | (app(tptp_fun_W_7(nil, V!46), nil) = tptp_fun_W_7(nil, V!46)))) <=> ((~![U: $i] : ((~ssList(U)) | (app(U, nil) = U))) | (~ssList(tptp_fun_W_7(nil, V!46))) | (app(tptp_fun_W_7(nil, V!46), nil) = tptp_fun_W_7(nil, V!46)))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(125,plain,
% 153.01/153.34 ((~![U: $i] : ((~ssList(U)) | (app(U, nil) = U))) | ((~ssList(tptp_fun_W_7(nil, V!46))) | (app(tptp_fun_W_7(nil, V!46), nil) = tptp_fun_W_7(nil, V!46)))),
% 153.01/153.34 inference(quant_inst,[status(thm)],[])).
% 153.01/153.34 tff(126,plain,
% 153.01/153.34 ((~![U: $i] : ((~ssList(U)) | (app(U, nil) = U))) | (~ssList(tptp_fun_W_7(nil, V!46))) | (app(tptp_fun_W_7(nil, V!46), nil) = tptp_fun_W_7(nil, V!46))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[125, 124])).
% 153.01/153.34 tff(127,plain,
% 153.01/153.34 (app(tptp_fun_W_7(nil, V!46), nil) = tptp_fun_W_7(nil, V!46)),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[126, 123, 113])).
% 153.01/153.34 tff(128,plain,
% 153.01/153.34 (tptp_fun_W_7(nil, V!46) = app(tptp_fun_W_7(nil, V!46), nil)),
% 153.01/153.34 inference(symmetry,[status(thm)],[127])).
% 153.01/153.34 tff(129,plain,
% 153.01/153.34 (app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) = app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46))),
% 153.01/153.34 inference(monotonicity,[status(thm)],[128, 111])).
% 153.01/153.34 tff(130,plain,
% 153.01/153.34 (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(131,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[130])).
% 153.01/153.34 tff(132,plain,
% 153.01/153.34 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(133,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[132])).
% 153.01/153.34 tff(134,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))),
% 153.01/153.34 inference(transitivity,[status(thm)],[133, 131])).
% 153.01/153.34 tff(135,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(136,plain,
% 153.01/153.34 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : trans(monotonicity(quant_intro(proof_bind(^[W: $i] : rewrite((ssList(W) => (app(app(U, V), W) = app(U, app(V, W)))) <=> ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))), (![W: $i] : (ssList(W) => (app(app(U, V), W) = app(U, app(V, W)))) <=> ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))), ((ssList(V) => ![W: $i] : (ssList(W) => (app(app(U, V), W) = app(U, app(V, W))))) <=> (ssList(V) => ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))), rewrite((ssList(V) => ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))) <=> ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))), ((ssList(V) => ![W: $i] : (ssList(W) => (app(app(U, V), W) = app(U, app(V, W))))) <=> ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))))), (![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => (app(app(U, V), W) = app(U, app(V, W))))) <=> ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))), ((ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => (app(app(U, V), W) = app(U, app(V, W)))))) <=> (ssList(U) => ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))))), rewrite((ssList(U) => ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))), ((ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => (app(app(U, V), W) = app(U, app(V, W)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(137,plain,
% 153.01/153.34 (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => (app(app(U, V), W) = app(U, app(V, W)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[136])).
% 153.01/153.34 tff(138,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => (app(app(U, V), W) = app(U, app(V, W))))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax82')).
% 153.01/153.34 tff(139,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[138, 137])).
% 153.01/153.34 tff(140,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[139, 135])).
% 153.01/153.34 tff(141,plain,(
% 153.01/153.34 ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))),
% 153.01/153.34 inference(skolemize,[status(sab)],[140])).
% 153.01/153.34 tff(142,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[141, 134])).
% 153.01/153.34 tff(143,plain,
% 153.01/153.34 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))) | ((~ssList(tptp_fun_W_7(nil, V!46))) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), V), W) = app(tptp_fun_W_7(nil, V!46), app(V, W))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))) | (~ssList(tptp_fun_W_7(nil, V!46))) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), V), W) = app(tptp_fun_W_7(nil, V!46), app(V, W))))))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(144,plain,
% 153.01/153.34 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))) | ((~ssList(tptp_fun_W_7(nil, V!46))) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), V), W) = app(tptp_fun_W_7(nil, V!46), app(V, W))))))),
% 153.01/153.34 inference(quant_inst,[status(thm)],[])).
% 153.01/153.34 tff(145,plain,
% 153.01/153.34 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(U, V), W) = app(U, app(V, W))))))) | (~ssList(tptp_fun_W_7(nil, V!46))) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), V), W) = app(tptp_fun_W_7(nil, V!46), app(V, W)))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[144, 143])).
% 153.01/153.34 tff(146,plain,
% 153.01/153.34 (![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), V), W) = app(tptp_fun_W_7(nil, V!46), app(V, W)))))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[145, 142, 113])).
% 153.01/153.34 tff(147,plain,
% 153.01/153.34 (((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), V), W) = app(tptp_fun_W_7(nil, V!46), app(V, W)))))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), W) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), W)))))) <=> ((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), V), W) = app(tptp_fun_W_7(nil, V!46), app(V, W)))))) | (~ssList(tptp_fun_X_8(nil, V!46))) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), W) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), W)))))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(148,plain,
% 153.01/153.34 ((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), V), W) = app(tptp_fun_W_7(nil, V!46), app(V, W)))))) | ((~ssList(tptp_fun_X_8(nil, V!46))) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), W) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), W)))))),
% 153.01/153.34 inference(quant_inst,[status(thm)],[])).
% 153.01/153.34 tff(149,plain,
% 153.01/153.34 ((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), V), W) = app(tptp_fun_W_7(nil, V!46), app(V, W)))))) | (~ssList(tptp_fun_X_8(nil, V!46))) | ![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), W) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), W))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[148, 147])).
% 153.01/153.34 tff(150,plain,
% 153.01/153.34 (![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), W) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), W))))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[149, 63, 146])).
% 153.01/153.34 tff(151,plain,
% 153.01/153.34 (((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = tptp_fun_X_8(nil, V!46)))) | ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))),
% 153.01/153.34 inference(tautology,[status(thm)],[])).
% 153.01/153.34 tff(152,plain,
% 153.01/153.34 (ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[151, 109])).
% 153.01/153.34 tff(153,plain,
% 153.01/153.34 (((~![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), W) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), W))))) | ((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))))))) <=> ((~![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), W) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), W))))) | (~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))))))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(154,plain,
% 153.01/153.34 ((~![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), W) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), W))))) | ((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))))))),
% 153.01/153.34 inference(quant_inst,[status(thm)],[])).
% 153.01/153.34 tff(155,plain,
% 153.01/153.34 ((~![W: $i] : ((~ssList(W)) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), W) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), W))))) | (~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[154, 153])).
% 153.01/153.34 tff(156,plain,
% 153.01/153.34 (app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = app(tptp_fun_W_7(nil, V!46), app(tptp_fun_X_8(nil, V!46), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))))),
% 153.01/153.34 inference(unit_resolution,[status(thm)],[155, 152, 150])).
% 153.01/153.34 tff(157,plain,
% 153.01/153.34 (app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)) = app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46))),
% 153.01/153.34 inference(monotonicity,[status(thm)],[128])).
% 153.01/153.34 tff(158,plain,
% 153.01/153.34 (app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46)) = app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46))),
% 153.01/153.34 inference(symmetry,[status(thm)],[157])).
% 153.01/153.34 tff(159,plain,
% 153.01/153.34 (V!46 = app(app(tptp_fun_W_7(nil, V!46), nil), tptp_fun_X_8(nil, V!46))),
% 153.01/153.34 inference(symmetry,[status(thm)],[61])).
% 153.01/153.34 tff(160,plain,
% 153.01/153.34 (~((~ssItem(Y!47)) | (~(app(cons(Y!47, nil), U!45) = V!46)))),
% 153.01/153.34 inference(and_elim,[status(thm)],[9])).
% 153.01/153.34 tff(161,plain,
% 153.01/153.34 (app(cons(Y!47, nil), U!45) = V!46),
% 153.01/153.34 inference(or_elim,[status(thm)],[160])).
% 153.01/153.34 tff(162,plain,
% 153.01/153.34 (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(163,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[162])).
% 153.01/153.34 tff(164,plain,
% 153.01/153.34 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(165,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[164])).
% 153.01/153.34 tff(166,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))),
% 153.01/153.34 inference(transitivity,[status(thm)],[165, 163])).
% 153.01/153.34 tff(167,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(168,plain,
% 153.01/153.34 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : rewrite((ssItem(V) => (cons(V, U) = app(cons(V, nil), U))) <=> ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))), (![V: $i] : (ssItem(V) => (cons(V, U) = app(cons(V, nil), U))) <=> ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))), ((ssList(U) => ![V: $i] : (ssItem(V) => (cons(V, U) = app(cons(V, nil), U)))) <=> (ssList(U) => ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))))), rewrite((ssList(U) => ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))), ((ssList(U) => ![V: $i] : (ssItem(V) => (cons(V, U) = app(cons(V, nil), U)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))))),
% 153.01/153.34 inference(bind,[status(th)],[])).
% 153.01/153.34 tff(169,plain,
% 153.01/153.34 (![U: $i] : (ssList(U) => ![V: $i] : (ssItem(V) => (cons(V, U) = app(cons(V, nil), U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))),
% 153.01/153.34 inference(quant_intro,[status(thm)],[168])).
% 153.01/153.34 tff(170,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssItem(V) => (cons(V, U) = app(cons(V, nil), U))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax81')).
% 153.01/153.34 tff(171,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[170, 169])).
% 153.01/153.34 tff(172,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[171, 167])).
% 153.01/153.34 tff(173,plain,(
% 153.01/153.34 ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))),
% 153.01/153.34 inference(skolemize,[status(sab)],[172])).
% 153.01/153.34 tff(174,plain,
% 153.01/153.34 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))),
% 153.01/153.34 inference(modus_ponens,[status(thm)],[173, 166])).
% 153.01/153.34 tff(175,plain,
% 153.01/153.34 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))) | ((~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))) | (~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil))))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(176,plain,
% 153.01/153.34 (((~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil)))) <=> ((~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil))))),
% 153.01/153.34 inference(rewrite,[status(thm)],[])).
% 153.01/153.34 tff(177,plain,
% 153.01/153.34 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))) | ((~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))) | ((~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil)))))),
% 153.01/153.35 inference(monotonicity,[status(thm)],[176])).
% 153.01/153.35 tff(178,plain,
% 153.01/153.35 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))) | ((~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))) | (~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil))))),
% 153.01/153.35 inference(transitivity,[status(thm)],[177, 175])).
% 153.01/153.35 tff(179,plain,
% 153.01/153.35 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))) | ((~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil))))),
% 153.01/153.35 inference(quant_inst,[status(thm)],[])).
% 153.01/153.35 tff(180,plain,
% 153.01/153.35 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (cons(V, U) = app(cons(V, nil), U))))) | (~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil)))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[179, 178])).
% 153.01/153.35 tff(181,plain,
% 153.01/153.35 (![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil)))),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[180, 36, 174])).
% 153.01/153.35 tff(182,plain,
% 153.01/153.35 (ssItem(Y!47)),
% 153.01/153.35 inference(or_elim,[status(thm)],[160])).
% 153.01/153.35 tff(183,plain,
% 153.01/153.35 (((~![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil)))) | ((~ssItem(Y!47)) | (cons(Y!47, nil) = app(cons(Y!47, nil), nil)))) <=> ((~![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil)))) | (~ssItem(Y!47)) | (cons(Y!47, nil) = app(cons(Y!47, nil), nil)))),
% 153.01/153.35 inference(rewrite,[status(thm)],[])).
% 153.01/153.35 tff(184,plain,
% 153.01/153.35 ((~![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil)))) | ((~ssItem(Y!47)) | (cons(Y!47, nil) = app(cons(Y!47, nil), nil)))),
% 153.01/153.35 inference(quant_inst,[status(thm)],[])).
% 153.01/153.35 tff(185,plain,
% 153.01/153.35 ((~![V: $i] : ((~ssItem(V)) | (cons(V, nil) = app(cons(V, nil), nil)))) | (~ssItem(Y!47)) | (cons(Y!47, nil) = app(cons(Y!47, nil), nil))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[184, 183])).
% 153.01/153.35 tff(186,plain,
% 153.01/153.35 (cons(Y!47, nil) = app(cons(Y!47, nil), nil)),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[185, 182, 181])).
% 153.01/153.35 tff(187,plain,
% 153.01/153.35 (app(cons(Y!47, nil), nil) = cons(Y!47, nil)),
% 153.01/153.35 inference(symmetry,[status(thm)],[186])).
% 153.01/153.35 tff(188,plain,
% 153.01/153.35 (app(app(cons(Y!47, nil), nil), U!45) = app(cons(Y!47, nil), U!45)),
% 153.01/153.35 inference(monotonicity,[status(thm)],[187])).
% 153.01/153.35 tff(189,plain,
% 153.01/153.35 (app(app(cons(Y!47, nil), nil), U!45) = app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46))),
% 153.01/153.35 inference(transitivity,[status(thm)],[188, 161, 159, 158])).
% 153.01/153.35 tff(190,plain,
% 153.01/153.35 (app(app(app(cons(Y!47, nil), nil), U!45), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = app(app(tptp_fun_W_7(nil, V!46), tptp_fun_X_8(nil, V!46)), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))),
% 153.01/153.35 inference(monotonicity,[status(thm)],[189])).
% 153.01/153.35 tff(191,plain,
% 153.01/153.35 (app(app(app(cons(Y!47, nil), nil), U!45), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = V!46),
% 153.01/153.35 inference(transitivity,[status(thm)],[190, 156, 129, 61])).
% 153.01/153.35 tff(192,plain,
% 153.01/153.35 (ssList(app(cons(Y!47, nil), nil)) <=> ssList(cons(Y!47, nil))),
% 153.01/153.35 inference(monotonicity,[status(thm)],[187])).
% 153.01/153.35 tff(193,plain,
% 153.01/153.35 (ssList(cons(Y!47, nil)) <=> ssList(app(cons(Y!47, nil), nil))),
% 153.01/153.35 inference(symmetry,[status(thm)],[192])).
% 153.01/153.35 tff(194,plain,
% 153.01/153.35 (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))))),
% 153.01/153.35 inference(bind,[status(th)],[])).
% 153.01/153.35 tff(195,plain,
% 153.01/153.35 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))),
% 153.01/153.35 inference(quant_intro,[status(thm)],[194])).
% 153.01/153.35 tff(196,plain,
% 153.01/153.35 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))))),
% 153.01/153.35 inference(bind,[status(th)],[])).
% 153.01/153.35 tff(197,plain,
% 153.01/153.35 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))),
% 153.01/153.35 inference(quant_intro,[status(thm)],[196])).
% 153.01/153.35 tff(198,plain,
% 153.01/153.35 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))),
% 153.01/153.35 inference(transitivity,[status(thm)],[197, 195])).
% 153.01/153.35 tff(199,plain,
% 153.01/153.35 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))),
% 153.01/153.35 inference(rewrite,[status(thm)],[])).
% 153.01/153.35 tff(200,plain,
% 153.01/153.35 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : rewrite((ssItem(V) => ssList(cons(V, U))) <=> ((~ssItem(V)) | ssList(cons(V, U))))), (![V: $i] : (ssItem(V) => ssList(cons(V, U))) <=> ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))), ((ssList(U) => ![V: $i] : (ssItem(V) => ssList(cons(V, U)))) <=> (ssList(U) => ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))))), rewrite((ssList(U) => ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))), ((ssList(U) => ![V: $i] : (ssItem(V) => ssList(cons(V, U)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))))),
% 153.01/153.35 inference(bind,[status(th)],[])).
% 153.01/153.35 tff(201,plain,
% 153.01/153.35 (![U: $i] : (ssList(U) => ![V: $i] : (ssItem(V) => ssList(cons(V, U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))),
% 153.01/153.35 inference(quant_intro,[status(thm)],[200])).
% 153.01/153.35 tff(202,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssItem(V) => ssList(cons(V, U))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax16')).
% 153.01/153.35 tff(203,plain,
% 153.01/153.35 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[202, 201])).
% 153.01/153.35 tff(204,plain,
% 153.01/153.35 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[203, 199])).
% 153.01/153.35 tff(205,plain,(
% 153.01/153.35 ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))),
% 153.01/153.35 inference(skolemize,[status(sab)],[204])).
% 153.01/153.35 tff(206,plain,
% 153.01/153.35 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[205, 198])).
% 153.01/153.35 tff(207,plain,
% 153.01/153.35 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))) | ((~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, nil))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))) | (~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, nil))))),
% 153.01/153.35 inference(rewrite,[status(thm)],[])).
% 153.01/153.35 tff(208,plain,
% 153.01/153.35 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))) | ((~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, nil))))),
% 153.01/153.35 inference(quant_inst,[status(thm)],[])).
% 153.01/153.35 tff(209,plain,
% 153.01/153.35 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, U))))) | (~ssList(nil)) | ![V: $i] : ((~ssItem(V)) | ssList(cons(V, nil)))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[208, 207])).
% 153.01/153.35 tff(210,plain,
% 153.01/153.35 (![V: $i] : ((~ssItem(V)) | ssList(cons(V, nil)))),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[209, 206, 36])).
% 153.01/153.35 tff(211,plain,
% 153.01/153.35 (((~![V: $i] : ((~ssItem(V)) | ssList(cons(V, nil)))) | ((~ssItem(Y!47)) | ssList(cons(Y!47, nil)))) <=> ((~![V: $i] : ((~ssItem(V)) | ssList(cons(V, nil)))) | (~ssItem(Y!47)) | ssList(cons(Y!47, nil)))),
% 153.01/153.35 inference(rewrite,[status(thm)],[])).
% 153.01/153.35 tff(212,plain,
% 153.01/153.35 ((~![V: $i] : ((~ssItem(V)) | ssList(cons(V, nil)))) | ((~ssItem(Y!47)) | ssList(cons(Y!47, nil)))),
% 153.01/153.35 inference(quant_inst,[status(thm)],[])).
% 153.01/153.35 tff(213,plain,
% 153.01/153.35 ((~![V: $i] : ((~ssItem(V)) | ssList(cons(V, nil)))) | (~ssItem(Y!47)) | ssList(cons(Y!47, nil))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[212, 211])).
% 153.01/153.35 tff(214,plain,
% 153.01/153.35 (ssList(cons(Y!47, nil))),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[213, 182, 210])).
% 153.01/153.35 tff(215,plain,
% 153.01/153.35 (ssList(app(cons(Y!47, nil), nil))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[214, 193])).
% 153.01/153.35 tff(216,plain,
% 153.01/153.35 (ssList(U!45)),
% 153.01/153.35 inference(and_elim,[status(thm)],[9])).
% 153.01/153.35 tff(217,plain,
% 153.01/153.35 (((~![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))) | ((~ssList(U!45)) | (~((~((~segmentP(V!46, U!45)) | (~((~ssList(tptp_fun_W_7(U!45, V!46))) | (~ssList(tptp_fun_X_8(U!45, V!46))) | (~(app(app(tptp_fun_W_7(U!45, V!46), U!45), tptp_fun_X_8(U!45, V!46)) = V!46)))))) | (~(segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46)))))))))) <=> ((~![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))) | (~ssList(U!45)) | (~((~((~segmentP(V!46, U!45)) | (~((~ssList(tptp_fun_W_7(U!45, V!46))) | (~ssList(tptp_fun_X_8(U!45, V!46))) | (~(app(app(tptp_fun_W_7(U!45, V!46), U!45), tptp_fun_X_8(U!45, V!46)) = V!46)))))) | (~(segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46)))))))))),
% 153.01/153.35 inference(rewrite,[status(thm)],[])).
% 153.01/153.35 tff(218,plain,
% 153.01/153.35 ((~![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))) | ((~ssList(U!45)) | (~((~((~segmentP(V!46, U!45)) | (~((~ssList(tptp_fun_W_7(U!45, V!46))) | (~ssList(tptp_fun_X_8(U!45, V!46))) | (~(app(app(tptp_fun_W_7(U!45, V!46), U!45), tptp_fun_X_8(U!45, V!46)) = V!46)))))) | (~(segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46)))))))))),
% 153.01/153.35 inference(quant_inst,[status(thm)],[])).
% 153.01/153.35 tff(219,plain,
% 153.01/153.35 ((~![V: $i] : ((~ssList(V)) | (~((~((~segmentP(V!46, V)) | (~((~ssList(tptp_fun_W_7(V, V!46))) | (~ssList(tptp_fun_X_8(V, V!46))) | (~(app(app(tptp_fun_W_7(V, V!46), V), tptp_fun_X_8(V, V!46)) = V!46)))))) | (~(segmentP(V!46, V) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, V), X) = V!46)))))))))) | (~ssList(U!45)) | (~((~((~segmentP(V!46, U!45)) | (~((~ssList(tptp_fun_W_7(U!45, V!46))) | (~ssList(tptp_fun_X_8(U!45, V!46))) | (~(app(app(tptp_fun_W_7(U!45, V!46), U!45), tptp_fun_X_8(U!45, V!46)) = V!46)))))) | (~(segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))))))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[218, 217])).
% 153.01/153.35 tff(220,plain,
% 153.01/153.35 (~((~((~segmentP(V!46, U!45)) | (~((~ssList(tptp_fun_W_7(U!45, V!46))) | (~ssList(tptp_fun_X_8(U!45, V!46))) | (~(app(app(tptp_fun_W_7(U!45, V!46), U!45), tptp_fun_X_8(U!45, V!46)) = V!46)))))) | (~(segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46)))))))),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[219, 216, 33])).
% 153.01/153.35 tff(221,plain,
% 153.01/153.35 (((~((~segmentP(V!46, U!45)) | (~((~ssList(tptp_fun_W_7(U!45, V!46))) | (~ssList(tptp_fun_X_8(U!45, V!46))) | (~(app(app(tptp_fun_W_7(U!45, V!46), U!45), tptp_fun_X_8(U!45, V!46)) = V!46)))))) | (~(segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))))) | (segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46)))))),
% 153.01/153.35 inference(tautology,[status(thm)],[])).
% 153.01/153.35 tff(222,plain,
% 153.01/153.35 (segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[221, 220])).
% 153.01/153.35 tff(223,plain,
% 153.01/153.35 (~segmentP(V!46, U!45)),
% 153.01/153.35 inference(and_elim,[status(thm)],[9])).
% 153.01/153.35 tff(224,plain,
% 153.01/153.35 ((~(segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46)))))) | segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))),
% 153.01/153.35 inference(tautology,[status(thm)],[])).
% 153.01/153.35 tff(225,plain,
% 153.01/153.35 ((~(segmentP(V!46, U!45) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46)))))) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[224, 223])).
% 153.01/153.35 tff(226,plain,
% 153.01/153.35 (![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[225, 222])).
% 153.01/153.35 tff(227,plain,
% 153.01/153.35 (((~![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))) | ((~ssList(app(cons(Y!47, nil), nil))) | ![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46))))) <=> ((~![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))) | (~ssList(app(cons(Y!47, nil), nil))) | ![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46))))),
% 153.01/153.35 inference(rewrite,[status(thm)],[])).
% 153.01/153.35 tff(228,plain,
% 153.01/153.35 ((~![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))) | ((~ssList(app(cons(Y!47, nil), nil))) | ![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46))))),
% 153.01/153.35 inference(quant_inst,[status(thm)],[])).
% 153.01/153.35 tff(229,plain,
% 153.01/153.35 ((~![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~(app(app(W, U!45), X) = V!46))))) | (~ssList(app(cons(Y!47, nil), nil))) | ![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46)))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[228, 227])).
% 153.01/153.35 tff(230,plain,
% 153.01/153.35 ((~ssList(app(cons(Y!47, nil), nil))) | ![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46)))),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[229, 226])).
% 153.01/153.35 tff(231,plain,
% 153.01/153.35 (![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46)))),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[230, 215])).
% 153.01/153.35 tff(232,plain,
% 153.01/153.35 (((~![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46)))) | ((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(app(app(cons(Y!47, nil), nil), U!45), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = V!46)))) <=> ((~![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46)))) | (~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(app(app(cons(Y!47, nil), nil), U!45), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = V!46)))),
% 153.01/153.35 inference(rewrite,[status(thm)],[])).
% 153.01/153.35 tff(233,plain,
% 153.01/153.35 ((~![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46)))) | ((~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(app(app(cons(Y!47, nil), nil), U!45), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = V!46)))),
% 153.01/153.35 inference(quant_inst,[status(thm)],[])).
% 153.01/153.35 tff(234,plain,
% 153.01/153.35 ((~![X: $i] : ((~ssList(X)) | (~(app(app(app(cons(Y!47, nil), nil), U!45), X) = V!46)))) | (~ssList(tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46)))) | (~(app(app(app(cons(Y!47, nil), nil), U!45), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = V!46))),
% 153.01/153.35 inference(modus_ponens,[status(thm)],[233, 232])).
% 153.01/153.35 tff(235,plain,
% 153.01/153.35 (~(app(app(app(cons(Y!47, nil), nil), U!45), tptp_fun_W_5(tptp_fun_X_8(nil, V!46), tptp_fun_X_8(nil, V!46))) = V!46)),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[234, 231, 152])).
% 153.01/153.35 tff(236,plain,
% 153.01/153.35 ($false),
% 153.01/153.35 inference(unit_resolution,[status(thm)],[235, 191])).
% 153.01/153.35 % SZS output end Proof
% 153.42/153.71 % E exiting
%------------------------------------------------------------------------------