%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN690-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n001.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:39:50 AM UTC 2025
% Result : Unsatisfiable 0.23s 0.59s
% Output : Proof 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SYN690-1 : TPTP v9.0.0. Released v2.5.0.
% 0.08/0.14 % Command : run_E %s %d THM
% 0.13/0.36 % Computer : n001.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Fri Jun 20 12:43:50 EDT 2025
% 0.13/0.36 % CPUTime :
% 0.23/0.59 % SZS status Unsatisfiable
% 0.23/0.59 % SZS output start Proof
% 0.23/0.59 tff(p4_type, type, (
% 0.23/0.59 p4: ( $i * $i ) > $o)).
% 0.23/0.59 tff(f5_type, type, (
% 0.23/0.59 f5: ( $i * $i ) > $i)).
% 0.23/0.59 tff(f12_type, type, (
% 0.23/0.59 f12: ( $i * $i ) > $i)).
% 0.23/0.59 tff(f30_type, type, (
% 0.23/0.59 f30: ( $i * $i ) > $i)).
% 0.23/0.59 tff(c39_type, type, (
% 0.23/0.59 c39: $i)).
% 0.23/0.59 tff(f32_type, type, (
% 0.23/0.59 f32: ( $i * $i ) > $i)).
% 0.23/0.59 tff(c37_type, type, (
% 0.23/0.59 c37: $i)).
% 0.23/0.59 tff(c42_type, type, (
% 0.23/0.59 c42: $i)).
% 0.23/0.59 tff(f14_type, type, (
% 0.23/0.59 f14: ( $i * $i ) > $i)).
% 0.23/0.59 tff(f26_type, type, (
% 0.23/0.59 f26: ( $i * $i ) > $i)).
% 0.23/0.59 tff(f28_type, type, (
% 0.23/0.59 f28: ( $i * $i ) > $i)).
% 0.23/0.59 tff(c44_type, type, (
% 0.23/0.59 c44: $i)).
% 0.23/0.59 tff(f16_type, type, (
% 0.23/0.59 f16: ( $i * $i ) > $i)).
% 0.23/0.59 tff(c43_type, type, (
% 0.23/0.59 c43: $i)).
% 0.23/0.59 tff(c41_type, type, (
% 0.23/0.59 c41: $i)).
% 0.23/0.59 tff(f7_type, type, (
% 0.23/0.59 f7: ( $i * $i ) > $i)).
% 0.23/0.59 tff(f18_type, type, (
% 0.23/0.59 f18: ( $i * $i ) > $i)).
% 0.23/0.59 tff(c40_type, type, (
% 0.23/0.59 c40: $i)).
% 0.23/0.59 tff(f20_type, type, (
% 0.23/0.59 f20: ( $i * $i ) > $i)).
% 0.23/0.59 tff(c38_type, type, (
% 0.23/0.59 c38: $i)).
% 0.23/0.59 tff(f22_type, type, (
% 0.23/0.59 f22: ( $i * $i ) > $i)).
% 0.23/0.59 tff(f24_type, type, (
% 0.23/0.59 f24: ( $i * $i ) > $i)).
% 0.23/0.59 tff(c45_type, type, (
% 0.23/0.59 c45: $i)).
% 0.23/0.59 tff(p2_type, type, (
% 0.23/0.59 p2: ( $i * $i ) > $o)).
% 0.23/0.59 tff(p34_type, type, (
% 0.23/0.59 p34: ( $i * $i ) > $o)).
% 0.23/0.59 tff(c36_type, type, (
% 0.23/0.59 c36: $i)).
% 0.23/0.59 tff(p35_type, type, (
% 0.23/0.59 p35: ( $i * $i ) > $o)).
% 0.23/0.59 tff(f10_type, type, (
% 0.23/0.59 f10: ( $i * $i ) > $i)).
% 0.23/0.59 tff(1,assumption,(~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))), introduced(assumption)).
% 0.23/0.59 tff(2,plain,
% 0.23/0.59 (^[X113: $i] : refl(p4(f5(c38, X113), f5(f7(c39, c38), X113)) <=> p4(f5(c38, X113), f5(f7(c39, c38), X113)))),
% 0.23/0.59 inference(bind,[status(th)],[])).
% 0.23/0.59 tff(3,plain,
% 0.23/0.59 (![X113: $i] : p4(f5(c38, X113), f5(f7(c39, c38), X113)) <=> ![X113: $i] : p4(f5(c38, X113), f5(f7(c39, c38), X113))),
% 0.23/0.59 inference(quant_intro,[status(thm)],[2])).
% 0.23/0.59 tff(4,plain,
% 0.23/0.59 (![X113: $i] : p4(f5(c38, X113), f5(f7(c39, c38), X113)) <=> ![X113: $i] : p4(f5(c38, X113), f5(f7(c39, c38), X113))),
% 0.23/0.59 inference(rewrite,[status(thm)],[])).
% 0.23/0.59 tff(5,axiom,(![X113: $i] : p4(f5(c38, X113), f5(f7(c39, c38), X113))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_22')).
% 0.23/0.59 tff(6,plain,
% 0.23/0.59 (![X113: $i] : p4(f5(c38, X113), f5(f7(c39, c38), X113))),
% 0.23/0.59 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.23/0.59 tff(7,plain,(
% 0.23/0.59 ![X113: $i] : p4(f5(c38, X113), f5(f7(c39, c38), X113))),
% 0.23/0.59 inference(skolemize,[status(sab)],[6])).
% 0.23/0.59 tff(8,plain,
% 0.23/0.59 (![X113: $i] : p4(f5(c38, X113), f5(f7(c39, c38), X113))),
% 0.23/0.59 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.23/0.59 tff(9,plain,
% 0.23/0.59 ((~![X113: $i] : p4(f5(c38, X113), f5(f7(c39, c38), X113))) | p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))),
% 0.23/0.59 inference(quant_inst,[status(thm)],[])).
% 0.23/0.59 tff(10,plain,
% 0.23/0.59 ($false),
% 0.23/0.59 inference(unit_resolution,[status(thm)],[9, 8, 1])).
% 0.23/0.59 tff(11,plain,(p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))), inference(lemma,lemma(discharge,[]))).
% 0.23/0.59 tff(12,assumption,(~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))), introduced(assumption)).
% 0.23/0.59 tff(13,plain,
% 0.23/0.59 (^[X114: $i] : refl(p4(f5(c40, X114), f5(f7(c39, c40), X114)) <=> p4(f5(c40, X114), f5(f7(c39, c40), X114)))),
% 0.23/0.59 inference(bind,[status(th)],[])).
% 0.23/0.59 tff(14,plain,
% 0.23/0.59 (![X114: $i] : p4(f5(c40, X114), f5(f7(c39, c40), X114)) <=> ![X114: $i] : p4(f5(c40, X114), f5(f7(c39, c40), X114))),
% 0.23/0.59 inference(quant_intro,[status(thm)],[13])).
% 0.23/0.59 tff(15,plain,
% 0.23/0.59 (![X114: $i] : p4(f5(c40, X114), f5(f7(c39, c40), X114)) <=> ![X114: $i] : p4(f5(c40, X114), f5(f7(c39, c40), X114))),
% 0.23/0.59 inference(rewrite,[status(thm)],[])).
% 0.23/0.59 tff(16,axiom,(![X114: $i] : p4(f5(c40, X114), f5(f7(c39, c40), X114))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_21')).
% 0.23/0.59 tff(17,plain,
% 0.23/0.59 (![X114: $i] : p4(f5(c40, X114), f5(f7(c39, c40), X114))),
% 0.23/0.59 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.23/0.59 tff(18,plain,(
% 0.23/0.59 ![X114: $i] : p4(f5(c40, X114), f5(f7(c39, c40), X114))),
% 0.23/0.59 inference(skolemize,[status(sab)],[17])).
% 0.23/0.59 tff(19,plain,
% 0.23/0.59 (![X114: $i] : p4(f5(c40, X114), f5(f7(c39, c40), X114))),
% 0.23/0.59 inference(modus_ponens,[status(thm)],[18, 14])).
% 0.23/0.59 tff(20,plain,
% 0.23/0.59 ((~![X114: $i] : p4(f5(c40, X114), f5(f7(c39, c40), X114))) | p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))),
% 0.23/0.59 inference(quant_inst,[status(thm)],[])).
% 0.23/0.59 tff(21,plain,
% 0.23/0.59 ($false),
% 0.23/0.59 inference(unit_resolution,[status(thm)],[20, 19, 12])).
% 0.23/0.59 tff(22,plain,(p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))), inference(lemma,lemma(discharge,[]))).
% 0.23/0.59 tff(23,plain,
% 0.23/0.59 (^[X31: $i, X32: $i, X34: $i, X33: $i] : refl(((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)) <=> ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)))),
% 0.23/0.59 inference(bind,[status(th)],[])).
% 0.23/0.59 tff(24,plain,
% 0.23/0.59 (![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)) <=> ![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))),
% 0.23/0.59 inference(quant_intro,[status(thm)],[23])).
% 0.23/0.59 tff(25,plain,
% 0.23/0.59 (![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)) <=> ![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))),
% 0.23/0.59 inference(rewrite,[status(thm)],[])).
% 0.23/0.59 tff(26,plain,
% 0.23/0.59 (^[X31: $i, X32: $i, X34: $i, X33: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((p2(X31, X32) | (~p34(c36, X33))) <=> ((~p34(c36, X33)) | p2(X31, X32))), (((p2(X31, X32) | (~p34(c36, X33))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> (((~p34(c36, X33)) | p2(X31, X32)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))))), rewrite((((~p34(c36, X33)) | p2(X31, X32)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> ((~p34(c36, X33)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))), (((p2(X31, X32) | (~p34(c36, X33))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> ((~p34(c36, X33)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)))), ((((p2(X31, X32) | (~p34(c36, X33))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> (((~p34(c36, X33)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))))), rewrite((((~p34(c36, X33)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))), ((((p2(X31, X32) | (~p34(c36, X33))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)))), (((((p2(X31, X32) | (~p34(c36, X33))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34))))) <=> (((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34))))))), rewrite((((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34))))) <=> ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))), (((((p2(X31, X32) | (~p34(c36, X33))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34))))) <=> ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))))),
% 0.23/0.59 inference(bind,[status(th)],[])).
% 0.23/0.59 tff(27,plain,
% 0.23/0.59 (![X31: $i, X32: $i, X34: $i, X33: $i] : ((((p2(X31, X32) | (~p34(c36, X33))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34))))) <=> ![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))),
% 0.23/0.59 inference(quant_intro,[status(thm)],[26])).
% 0.23/0.59 tff(28,axiom,(![X31: $i, X32: $i, X34: $i, X33: $i] : ((((p2(X31, X32) | (~p34(c36, X33))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_62')).
% 0.23/0.59 tff(29,plain,
% 0.23/0.59 (![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))),
% 0.23/0.59 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.23/0.59 tff(30,plain,
% 0.23/0.59 (![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))),
% 0.23/0.59 inference(modus_ponens,[status(thm)],[29, 25])).
% 0.23/0.59 tff(31,plain,(
% 0.23/0.59 ![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))),
% 0.23/0.59 inference(skolemize,[status(sab)],[30])).
% 0.23/0.59 tff(32,plain,
% 0.23/0.59 (![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))),
% 0.45/0.60 inference(modus_ponens,[status(thm)],[31, 24])).
% 0.45/0.60 tff(33,plain,
% 0.45/0.60 ((~p2(c38, c40)) <=> (~p2(c38, c40))),
% 0.45/0.60 inference(rewrite,[status(thm)],[])).
% 0.45/0.60 tff(34,axiom,(~p2(c38, c40)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','not_p2_20')).
% 0.45/0.60 tff(35,plain,
% 0.45/0.60 (~p2(c38, c40)),
% 0.45/0.60 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.45/0.60 tff(36,plain,
% 0.45/0.60 (p34(c36, c37) <=> p34(c36, c37)),
% 0.45/0.60 inference(rewrite,[status(thm)],[])).
% 0.45/0.60 tff(37,axiom,(p34(c36, c37)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p34_19')).
% 0.45/0.60 tff(38,plain,
% 0.45/0.60 (p34(c36, c37)),
% 0.45/0.60 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.45/0.60 tff(39,plain,
% 0.45/0.60 (((~![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))) | (p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))))) <=> ((~![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))) | p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))))),
% 0.45/0.60 inference(rewrite,[status(thm)],[])).
% 0.45/0.60 tff(40,plain,
% 0.45/0.60 (((~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p2(c38, c40)) <=> (p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))))),
% 0.45/0.60 inference(rewrite,[status(thm)],[])).
% 0.45/0.60 tff(41,plain,
% 0.45/0.60 (((~![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))) | ((~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p2(c38, c40))) <=> ((~![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))) | (p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40))))))),
% 0.45/0.60 inference(monotonicity,[status(thm)],[40])).
% 0.45/0.60 tff(42,plain,
% 0.45/0.60 (((~![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))) | ((~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p2(c38, c40))) <=> ((~![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))) | p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))))),
% 0.45/0.60 inference(transitivity,[status(thm)],[41, 39])).
% 0.45/0.60 tff(43,plain,
% 0.45/0.60 ((~![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))) | ((~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p2(c38, c40))),
% 0.45/0.60 inference(quant_inst,[status(thm)],[])).
% 0.45/0.60 tff(44,plain,
% 0.45/0.60 ((~![X31: $i, X32: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(f7(X34, f26(f28(c43, X33), X34)), f30(f32(c42, X33), X34)), f5(f7(X34, f26(f28(c44, X33), X34)), f30(f32(c42, X33), X34)))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | p2(X31, X32))) | p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40))))),
% 0.45/0.60 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.45/0.60 tff(45,plain,
% 0.45/0.60 ((~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40))))),
% 0.45/0.60 inference(unit_resolution,[status(thm)],[44, 38, 35, 32])).
% 0.45/0.60 tff(46,plain,
% 0.45/0.60 (~p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))),
% 0.45/0.60 inference(unit_resolution,[status(thm)],[45, 22, 11])).
% 0.45/0.60 tff(47,plain,
% 0.45/0.60 (^[X105: $i, X104: $i, X103: $i] : refl((p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105))))) <=> (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105))))))),
% 0.45/0.60 inference(bind,[status(th)],[])).
% 0.45/0.60 tff(48,plain,
% 0.45/0.60 (![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105))))) <=> ![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))),
% 0.45/0.60 inference(quant_intro,[status(thm)],[47])).
% 0.45/0.60 tff(49,plain,
% 0.45/0.60 (![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105))))) <=> ![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))),
% 0.45/0.60 inference(rewrite,[status(thm)],[])).
% 0.45/0.60 tff(50,axiom,(![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_58')).
% 0.45/0.60 tff(51,plain,
% 0.45/0.60 (![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))),
% 0.45/0.60 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.45/0.60 tff(52,plain,(
% 0.45/0.60 ![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))),
% 0.45/0.60 inference(skolemize,[status(sab)],[51])).
% 0.45/0.60 tff(53,plain,
% 0.45/0.60 (![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))),
% 0.45/0.61 inference(modus_ponens,[status(thm)],[52, 48])).
% 0.45/0.61 tff(54,plain,
% 0.45/0.61 (((~![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))) | (p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))) | (~p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))))))) <=> ((~![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))) | p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))) | (~p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))))))),
% 0.45/0.61 inference(rewrite,[status(thm)],[])).
% 0.45/0.61 tff(55,plain,
% 0.45/0.61 ((~![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))) | (p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))) | (~p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))))))),
% 0.45/0.61 inference(quant_inst,[status(thm)],[])).
% 0.45/0.61 tff(56,plain,
% 0.45/0.61 ((~![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | (~p4(f5(X103, f12(f14(f16(c41, X103), X104), X105)), f5(X104, f12(f14(f16(c41, X103), X104), X105)))))) | p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))) | (~p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))))),
% 0.45/0.61 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.45/0.61 tff(57,plain,
% 0.45/0.61 (~p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))))),
% 0.45/0.61 inference(unit_resolution,[status(thm)],[56, 53, 46])).
% 0.45/0.61 tff(58,plain,
% 0.45/0.61 (^[X105: $i, X104: $i, X103: $i] : refl((p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105)) <=> (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105)))),
% 0.45/0.61 inference(bind,[status(th)],[])).
% 0.45/0.61 tff(59,plain,
% 0.45/0.61 (![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105)) <=> ![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))),
% 0.45/0.61 inference(quant_intro,[status(thm)],[58])).
% 0.45/0.61 tff(60,plain,
% 0.45/0.61 (![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105)) <=> ![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))),
% 0.45/0.61 inference(rewrite,[status(thm)],[])).
% 0.45/0.61 tff(61,axiom,(![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_57')).
% 0.45/0.61 tff(62,plain,
% 0.45/0.61 (![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))),
% 0.45/0.61 inference(modus_ponens,[status(thm)],[61, 60])).
% 0.45/0.61 tff(63,plain,(
% 0.45/0.61 ![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))),
% 0.45/0.61 inference(skolemize,[status(sab)],[62])).
% 0.45/0.61 tff(64,plain,
% 0.45/0.61 (![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))),
% 0.45/0.61 inference(modus_ponens,[status(thm)],[63, 59])).
% 0.45/0.61 tff(65,plain,
% 0.45/0.61 (((~![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))) | (p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))) | p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39)))) <=> ((~![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))) | p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))) | p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39)))),
% 0.45/0.61 inference(rewrite,[status(thm)],[])).
% 0.45/0.61 tff(66,plain,
% 0.45/0.61 ((~![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))) | (p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))) | p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39)))),
% 0.45/0.61 inference(quant_inst,[status(thm)],[])).
% 0.45/0.61 tff(67,plain,
% 0.45/0.61 ((~![X105: $i, X104: $i, X103: $i] : (p4(f5(f7(c39, X103), X105), f5(f7(c39, X104), X105)) | p35(f10(c37, f12(f14(f16(c41, X103), X104), X105)), X105))) | p4(f5(f7(c39, f26(f28(c43, c37), c39)), f30(f32(c42, c37), c39)), f5(f7(c39, f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))) | p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))),
% 0.45/0.61 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.45/0.61 tff(68,plain,
% 0.45/0.61 (p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))),
% 0.45/0.61 inference(unit_resolution,[status(thm)],[67, 64, 46])).
% 0.45/0.61 tff(69,plain,
% 0.45/0.61 (^[X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : refl(((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)) <=> ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)))),
% 0.45/0.61 inference(bind,[status(th)],[])).
% 0.45/0.61 tff(70,plain,
% 0.45/0.61 (![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)) <=> ![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))),
% 0.45/0.61 inference(quant_intro,[status(thm)],[69])).
% 0.45/0.61 tff(71,plain,
% 0.45/0.61 (![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)) <=> ![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))),
% 0.45/0.61 inference(rewrite,[status(thm)],[])).
% 0.45/0.61 tff(72,plain,
% 0.45/0.61 (^[X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((p2(X31, X32) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35))) | (~p34(c36, X33))) <=> ((~p34(c36, X33)) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))), ((((p2(X31, X32) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35))) | (~p34(c36, X33))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))) <=> (((~p34(c36, X33)) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))))), rewrite((((~p34(c36, X33)) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))) <=> ((~p34(c36, X33)) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))), ((((p2(X31, X32) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35))) | (~p34(c36, X33))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))) <=> ((~p34(c36, X33)) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)))), (((((p2(X31, X32) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35))) | (~p34(c36, X33))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> (((~p34(c36, X33)) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))))), rewrite((((~p34(c36, X33)) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> ((~p34(c36, X33)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))), (((((p2(X31, X32) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35))) | (~p34(c36, X33))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> ((~p34(c36, X33)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)))), ((((((p2(X31, X32) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35))) | (~p34(c36, X33))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> (((~p34(c36, X33)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))))), rewrite((((~p34(c36, X33)) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))), ((((((p2(X31, X32) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35))) | (~p34(c36, X33))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))))),
% 0.45/0.61 inference(bind,[status(th)],[])).
% 0.45/0.61 tff(73,plain,
% 0.45/0.61 (![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : (((((p2(X31, X32) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35))) | (~p34(c36, X33))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) <=> ![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))),
% 0.47/0.61 inference(quant_intro,[status(thm)],[72])).
% 0.47/0.61 tff(74,axiom,(![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : (((((p2(X31, X32) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35))) | (~p34(c36, X33))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32))))) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_61')).
% 0.47/0.61 tff(75,plain,
% 0.47/0.61 (![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))),
% 0.47/0.61 inference(modus_ponens,[status(thm)],[74, 73])).
% 0.47/0.61 tff(76,plain,
% 0.47/0.61 (![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))),
% 0.47/0.61 inference(modus_ponens,[status(thm)],[75, 71])).
% 0.47/0.61 tff(77,plain,(
% 0.47/0.61 ![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))),
% 0.47/0.61 inference(skolemize,[status(sab)],[76])).
% 0.47/0.61 tff(78,plain,
% 0.47/0.61 (![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))),
% 0.47/0.61 inference(modus_ponens,[status(thm)],[77, 70])).
% 0.47/0.61 tff(79,plain,
% 0.47/0.61 (((~![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))) | (p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))))) <=> ((~![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))) | p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))))),
% 0.47/0.62 inference(rewrite,[status(thm)],[])).
% 0.47/0.62 tff(80,plain,
% 0.47/0.62 (((~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | p2(c38, c40)) <=> (p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))))),
% 0.47/0.62 inference(rewrite,[status(thm)],[])).
% 0.47/0.62 tff(81,plain,
% 0.47/0.62 (((~![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))) | ((~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | p2(c38, c40))) <=> ((~![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))) | (p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39)))))),
% 0.47/0.62 inference(monotonicity,[status(thm)],[80])).
% 0.47/0.62 tff(82,plain,
% 0.47/0.62 (((~![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))) | ((~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | p2(c38, c40))) <=> ((~![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))) | p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))))),
% 0.47/0.62 inference(transitivity,[status(thm)],[81, 79])).
% 0.47/0.62 tff(83,plain,
% 0.47/0.62 ((~![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))) | ((~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | p2(c38, c40))),
% 0.47/0.62 inference(quant_inst,[status(thm)],[])).
% 0.47/0.62 tff(84,plain,
% 0.47/0.62 ((~![X31: $i, X32: $i, X35: $i, X34: $i, X33: $i] : ((~p34(c36, X33)) | (~p4(f5(X32, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X32), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p4(f5(X31, f18(f20(f22(f24(c45, X33), X34), X31), X32)), f5(f7(X34, X31), f18(f20(f22(f24(c45, X33), X34), X31), X32)))) | (~p35(f10(X33, X35), f30(f32(c42, X33), X34))) | p4(f5(f26(f28(c43, X33), X34), X35), f5(f26(f28(c44, X33), X34), X35)) | p2(X31, X32))) | p2(c38, c40) | (~p34(c36, c37)) | (~p4(f5(c40, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c40), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | (~p4(f5(c38, f18(f20(f22(f24(c45, c37), c39), c38), c40)), f5(f7(c39, c38), f18(f20(f22(f24(c45, c37), c39), c38), c40)))) | p4(f5(f26(f28(c43, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f5(f26(f28(c44, c37), c39), f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39)))) | (~p35(f10(c37, f12(f14(f16(c41, f26(f28(c43, c37), c39)), f26(f28(c44, c37), c39)), f30(f32(c42, c37), c39))), f30(f32(c42, c37), c39)))),
% 0.47/0.62 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.47/0.62 tff(85,plain,
% 0.47/0.62 ($false),
% 0.47/0.62 inference(unit_resolution,[status(thm)],[84, 38, 35, 78, 22, 11, 68, 57])).
% 0.47/0.62 % SZS output end Proof
% 0.47/0.63 % E exiting
%------------------------------------------------------------------------------