%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN039-1 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n014.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:38:00 AM UTC 2025
% Result : Unsatisfiable 0.61s 0.79s
% Output : Proof 0.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN039-1 : TPTP v9.0.0. Released v1.0.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n014.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 12:26:39 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.61/0.79 % SZS status Unsatisfiable
% 0.61/0.79 % SZS output start Proof
% 0.61/0.79 tff(s_type, type, (
% 0.61/0.79 s: ( $i * $i ) > $o)).
% 0.61/0.79 tff(f1_type, type, (
% 0.61/0.79 f1: ( $i * $i ) > $i)).
% 0.61/0.79 tff(elem_0_type, type, (
% 0.61/0.79 elem_0: $i)).
% 0.61/0.79 tff(q_type, type, (
% 0.61/0.79 q: ( $i * $i ) > $o)).
% 0.61/0.79 tff(p_type, type, (
% 0.61/0.79 p: ( $i * $i ) > $o)).
% 0.61/0.79 tff(1,assumption,(~s(elem!0, elem!0)), introduced(assumption)).
% 0.61/0.79 tff(2,assumption,(~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))), introduced(assumption)).
% 0.61/0.79 tff(3,assumption,(~p(f1(elem!0, elem!0), f1(elem!0, elem!0))), introduced(assumption)).
% 0.61/0.79 tff(4,assumption,(~s(f1(elem!0, elem!0), f1(elem!0, elem!0))), introduced(assumption)).
% 0.61/0.79 tff(5,plain,
% 0.61/0.79 (^[Z: $i, Z1: $i, X: $i, X1: $i] : refl((p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z)) <=> (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z)))),
% 0.61/0.79 inference(bind,[status(th)],[])).
% 0.61/0.79 tff(6,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))),
% 0.61/0.79 inference(quant_intro,[status(thm)],[5])).
% 0.61/0.79 tff(7,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))),
% 0.61/0.79 inference(rewrite,[status(thm)],[])).
% 0.61/0.79 tff(8,plain,
% 0.61/0.79 (^[Z: $i, Z1: $i, X: $i, X1: $i] : rewrite(((p(f1(X, X1), f1(X, X1)) | s(f1(X, X1), Z)) | q(f1(X, X1), Z1)) <=> (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z)))),
% 0.61/0.79 inference(bind,[status(th)],[])).
% 0.61/0.79 tff(9,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((p(f1(X, X1), f1(X, X1)) | s(f1(X, X1), Z)) | q(f1(X, X1), Z1)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))),
% 0.61/0.79 inference(quant_intro,[status(thm)],[8])).
% 0.61/0.79 tff(10,axiom,(![Z: $i, Z1: $i, X: $i, X1: $i] : ((p(f1(X, X1), f1(X, X1)) | s(f1(X, X1), Z)) | q(f1(X, X1), Z1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_5')).
% 0.61/0.79 tff(11,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[10, 9])).
% 0.61/0.79 tff(12,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[11, 7])).
% 0.61/0.79 tff(13,plain,(
% 0.61/0.79 ![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))),
% 0.61/0.79 inference(skolemize,[status(sab)],[12])).
% 0.61/0.79 tff(14,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[13, 6])).
% 0.61/0.79 tff(15,plain,
% 0.61/0.79 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.79 inference(rewrite,[status(thm)],[])).
% 0.61/0.79 tff(16,plain,
% 0.61/0.79 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.79 inference(quant_inst,[status(thm)],[])).
% 0.61/0.79 tff(17,plain,
% 0.61/0.79 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.61/0.79 tff(18,plain,
% 0.61/0.79 (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.61/0.79 inference(unit_resolution,[status(thm)],[17, 14])).
% 0.61/0.79 tff(19,plain,
% 0.61/0.79 (q(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.61/0.79 inference(unit_resolution,[status(thm)],[18, 4, 3])).
% 0.61/0.79 tff(20,plain,
% 0.61/0.79 (^[Z: $i, Z1: $i, X: $i, X1: $i] : refl(((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X)) <=> ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X)))),
% 0.61/0.79 inference(bind,[status(th)],[])).
% 0.61/0.79 tff(21,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.79 inference(quant_intro,[status(thm)],[20])).
% 0.61/0.79 tff(22,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.79 inference(rewrite,[status(thm)],[])).
% 0.61/0.79 tff(23,plain,
% 0.61/0.79 (^[Z: $i, Z1: $i, X: $i, X1: $i] : trans(monotonicity(rewrite((s(Z, X) | (~q(Z1, Z1))) <=> ((~q(Z1, Z1)) | s(Z, X))), (((s(Z, X) | (~q(Z1, Z1))) | (~q(X1, f1(X, X1)))) <=> (((~q(Z1, Z1)) | s(Z, X)) | (~q(X1, f1(X, X1)))))), rewrite((((~q(Z1, Z1)) | s(Z, X)) | (~q(X1, f1(X, X1)))) <=> ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))), (((s(Z, X) | (~q(Z1, Z1))) | (~q(X1, f1(X, X1)))) <=> ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))))),
% 0.61/0.79 inference(bind,[status(th)],[])).
% 0.61/0.79 tff(24,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((s(Z, X) | (~q(Z1, Z1))) | (~q(X1, f1(X, X1)))) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.79 inference(quant_intro,[status(thm)],[23])).
% 0.61/0.79 tff(25,axiom,(![Z: $i, Z1: $i, X: $i, X1: $i] : ((s(Z, X) | (~q(Z1, Z1))) | (~q(X1, f1(X, X1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_25')).
% 0.61/0.79 tff(26,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[25, 24])).
% 0.61/0.79 tff(27,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[26, 22])).
% 0.61/0.79 tff(28,plain,(
% 0.61/0.79 ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.79 inference(skolemize,[status(sab)],[27])).
% 0.61/0.79 tff(29,plain,
% 0.61/0.79 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[28, 21])).
% 0.61/0.79 tff(30,plain,
% 0.61/0.79 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, elem!0) | (~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | (~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.79 inference(rewrite,[status(thm)],[])).
% 0.61/0.79 tff(31,plain,
% 0.61/0.79 (((~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0)) <=> (s(elem!0, elem!0) | (~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.79 inference(rewrite,[status(thm)],[])).
% 0.61/0.79 tff(32,plain,
% 0.61/0.79 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))) | ((~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, elem!0) | (~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.61/0.79 inference(monotonicity,[status(thm)],[31])).
% 0.61/0.79 tff(33,plain,
% 0.61/0.79 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))) | ((~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | (~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.79 inference(transitivity,[status(thm)],[32, 30])).
% 0.61/0.79 tff(34,plain,
% 0.61/0.79 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))) | ((~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0))),
% 0.61/0.79 inference(quant_inst,[status(thm)],[])).
% 0.61/0.79 tff(35,plain,
% 0.61/0.79 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | (~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.61/0.79 tff(36,plain,
% 0.61/0.79 (~q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))),
% 0.61/0.79 inference(unit_resolution,[status(thm)],[35, 29, 1, 19])).
% 0.61/0.79 tff(37,plain,
% 0.61/0.79 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0))))),
% 0.61/0.79 inference(rewrite,[status(thm)],[])).
% 0.61/0.79 tff(38,plain,
% 0.61/0.79 ((p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0))) | s(f1(elem!0, elem!0), f1(elem!0, elem!0))) <=> (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0))))),
% 0.61/0.79 inference(rewrite,[status(thm)],[])).
% 0.61/0.79 tff(39,plain,
% 0.61/0.79 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0))) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.61/0.79 inference(monotonicity,[status(thm)],[38])).
% 0.61/0.79 tff(40,plain,
% 0.61/0.79 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0))) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0))))),
% 0.61/0.79 inference(transitivity,[status(thm)],[39, 37])).
% 0.61/0.79 tff(41,plain,
% 0.61/0.79 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0))) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.79 inference(quant_inst,[status(thm)],[])).
% 0.61/0.79 tff(42,plain,
% 0.61/0.79 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, f1(elem!0, elem!0)))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.61/0.79 tff(43,plain,
% 0.61/0.79 ($false),
% 0.61/0.79 inference(unit_resolution,[status(thm)],[42, 14, 3, 4, 36])).
% 0.61/0.79 tff(44,plain,(s(f1(elem!0, elem!0), f1(elem!0, elem!0)) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(elem!0, elem!0)), inference(lemma,lemma(discharge,[]))).
% 0.61/0.79 tff(45,plain,
% 0.61/0.79 (s(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.61/0.79 inference(unit_resolution,[status(thm)],[44, 3, 1])).
% 0.61/0.79 tff(46,assumption,(s(f1(elem!0, elem!0), f1(elem!0, elem!0))), introduced(assumption)).
% 0.61/0.79 tff(47,assumption,(~s(elem!0, f1(elem!0, elem!0))), introduced(assumption)).
% 0.61/0.79 tff(48,plain,
% 0.61/0.79 (^[Z: $i, X: $i, X1: $i] : refl(((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X)) <=> ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X)))),
% 0.61/0.79 inference(bind,[status(th)],[])).
% 0.61/0.79 tff(49,plain,
% 0.61/0.79 (![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X)) <=> ![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))),
% 0.61/0.79 inference(quant_intro,[status(thm)],[48])).
% 0.61/0.79 tff(50,plain,
% 0.61/0.79 (![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X)) <=> ![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))),
% 0.61/0.79 inference(rewrite,[status(thm)],[])).
% 0.61/0.79 tff(51,plain,
% 0.61/0.79 (^[Z: $i, X: $i, X1: $i] : trans(monotonicity(rewrite((s(Z, X) | (~s(X, f1(X, X1)))) <=> ((~s(X, f1(X, X1))) | s(Z, X))), (((s(Z, X) | (~s(X, f1(X, X1)))) | (~s(X1, X1))) <=> (((~s(X, f1(X, X1))) | s(Z, X)) | (~s(X1, X1))))), rewrite((((~s(X, f1(X, X1))) | s(Z, X)) | (~s(X1, X1))) <=> ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))), (((s(Z, X) | (~s(X, f1(X, X1)))) | (~s(X1, X1))) <=> ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))))),
% 0.61/0.79 inference(bind,[status(th)],[])).
% 0.61/0.79 tff(52,plain,
% 0.61/0.79 (![Z: $i, X: $i, X1: $i] : ((s(Z, X) | (~s(X, f1(X, X1)))) | (~s(X1, X1))) <=> ![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))),
% 0.61/0.79 inference(quant_intro,[status(thm)],[51])).
% 0.61/0.79 tff(53,axiom,(![Z: $i, X: $i, X1: $i] : ((s(Z, X) | (~s(X, f1(X, X1)))) | (~s(X1, X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_21')).
% 0.61/0.79 tff(54,plain,
% 0.61/0.79 (![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[53, 52])).
% 0.61/0.79 tff(55,plain,
% 0.61/0.79 (![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[54, 50])).
% 0.61/0.79 tff(56,plain,(
% 0.61/0.79 ![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))),
% 0.61/0.79 inference(skolemize,[status(sab)],[55])).
% 0.61/0.79 tff(57,plain,
% 0.61/0.79 (![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))),
% 0.61/0.79 inference(modus_ponens,[status(thm)],[56, 49])).
% 0.61/0.79 tff(58,plain,
% 0.61/0.79 (((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | (s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(59,plain,
% 0.61/0.80 (((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0))) <=> (s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(60,plain,
% 0.61/0.80 (((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | (s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.61/0.80 inference(monotonicity,[status(thm)],[59])).
% 0.61/0.80 tff(61,plain,
% 0.61/0.80 (((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(transitivity,[status(thm)],[60, 58])).
% 0.61/0.80 tff(62,plain,
% 0.61/0.80 ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))),
% 0.61/0.80 inference(quant_inst,[status(thm)],[])).
% 0.61/0.80 tff(63,plain,
% 0.61/0.80 ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[62, 61])).
% 0.61/0.80 tff(64,plain,
% 0.61/0.80 (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.80 inference(unit_resolution,[status(thm)],[63, 57, 47, 46])).
% 0.61/0.80 tff(65,assumption,(~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))), introduced(assumption)).
% 0.61/0.80 tff(66,assumption,(~q(f1(elem!0, elem!0), f1(elem!0, elem!0))), introduced(assumption)).
% 0.61/0.80 tff(67,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(68,plain,
% 0.61/0.80 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(quant_inst,[status(thm)],[])).
% 0.61/0.80 tff(69,plain,
% 0.61/0.80 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (p(f1(X, X1), f1(X, X1)) | q(f1(X, X1), Z1) | s(f1(X, X1), Z))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[68, 67])).
% 0.61/0.80 tff(70,plain,
% 0.61/0.80 ($false),
% 0.61/0.80 inference(unit_resolution,[status(thm)],[69, 14, 3, 66, 65])).
% 0.61/0.80 tff(71,plain,(q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))), inference(lemma,lemma(discharge,[]))).
% 0.61/0.80 tff(72,plain,
% 0.61/0.80 (q(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.61/0.80 inference(unit_resolution,[status(thm)],[71, 64, 3])).
% 0.61/0.80 tff(73,plain,
% 0.61/0.80 (^[Z: $i, Z1: $i, X: $i, X1: $i] : refl(((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X)) <=> ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X)))),
% 0.61/0.80 inference(bind,[status(th)],[])).
% 0.61/0.80 tff(74,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.80 inference(quant_intro,[status(thm)],[73])).
% 0.61/0.80 tff(75,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(76,plain,
% 0.61/0.80 (^[Z: $i, Z1: $i, X: $i, X1: $i] : trans(monotonicity(rewrite((s(Z, X) | (~q(Z1, Z1))) <=> ((~q(Z1, Z1)) | s(Z, X))), (((s(Z, X) | (~q(Z1, Z1))) | (~s(X1, X1))) <=> (((~q(Z1, Z1)) | s(Z, X)) | (~s(X1, X1))))), rewrite((((~q(Z1, Z1)) | s(Z, X)) | (~s(X1, X1))) <=> ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))), (((s(Z, X) | (~q(Z1, Z1))) | (~s(X1, X1))) <=> ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))))),
% 0.61/0.80 inference(bind,[status(th)],[])).
% 0.61/0.80 tff(77,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((s(Z, X) | (~q(Z1, Z1))) | (~s(X1, X1))) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.80 inference(quant_intro,[status(thm)],[76])).
% 0.61/0.80 tff(78,axiom,(![Z: $i, Z1: $i, X: $i, X1: $i] : ((s(Z, X) | (~q(Z1, Z1))) | (~s(X1, X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_27')).
% 0.61/0.80 tff(79,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[78, 77])).
% 0.61/0.80 tff(80,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[79, 75])).
% 0.61/0.80 tff(81,plain,(
% 0.61/0.80 ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.80 inference(skolemize,[status(sab)],[80])).
% 0.61/0.80 tff(82,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[81, 74])).
% 0.61/0.80 tff(83,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(84,plain,
% 0.61/0.80 (((~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0))) <=> (s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(85,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.61/0.80 inference(monotonicity,[status(thm)],[84])).
% 0.61/0.80 tff(86,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(transitivity,[status(thm)],[85, 83])).
% 0.61/0.80 tff(87,plain,
% 0.61/0.80 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))),
% 0.61/0.80 inference(quant_inst,[status(thm)],[])).
% 0.61/0.80 tff(88,plain,
% 0.61/0.80 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[87, 86])).
% 0.61/0.80 tff(89,plain,
% 0.61/0.80 ($false),
% 0.61/0.80 inference(unit_resolution,[status(thm)],[88, 82, 47, 72, 46])).
% 0.61/0.80 tff(90,plain,(s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0))), inference(lemma,lemma(discharge,[]))).
% 0.61/0.80 tff(91,plain,
% 0.61/0.80 (s(elem!0, f1(elem!0, elem!0))),
% 0.61/0.80 inference(unit_resolution,[status(thm)],[90, 45, 3])).
% 0.61/0.80 tff(92,assumption,(s(elem!0, f1(elem!0, elem!0))), introduced(assumption)).
% 0.61/0.80 tff(93,plain,
% 0.61/0.80 (^[Z: $i, Z1: $i, X: $i, X1: $i] : refl(((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X)) <=> ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X)))),
% 0.61/0.80 inference(bind,[status(th)],[])).
% 0.61/0.80 tff(94,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))),
% 0.61/0.80 inference(quant_intro,[status(thm)],[93])).
% 0.61/0.80 tff(95,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(96,plain,
% 0.61/0.80 (^[Z: $i, Z1: $i, X: $i, X1: $i] : trans(monotonicity(rewrite((s(Z, X) | (~s(X, f1(X, X1)))) <=> ((~s(X, f1(X, X1))) | s(Z, X))), (((s(Z, X) | (~s(X, f1(X, X1)))) | q(f1(X, X1), Z1)) <=> (((~s(X, f1(X, X1))) | s(Z, X)) | q(f1(X, X1), Z1)))), rewrite((((~s(X, f1(X, X1))) | s(Z, X)) | q(f1(X, X1), Z1)) <=> ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))), (((s(Z, X) | (~s(X, f1(X, X1)))) | q(f1(X, X1), Z1)) <=> ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))))),
% 0.61/0.80 inference(bind,[status(th)],[])).
% 0.61/0.80 tff(97,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((s(Z, X) | (~s(X, f1(X, X1)))) | q(f1(X, X1), Z1)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))),
% 0.61/0.80 inference(quant_intro,[status(thm)],[96])).
% 0.61/0.80 tff(98,axiom,(![Z: $i, Z1: $i, X: $i, X1: $i] : ((s(Z, X) | (~s(X, f1(X, X1)))) | q(f1(X, X1), Z1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_20')).
% 0.61/0.80 tff(99,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[98, 97])).
% 0.61/0.80 tff(100,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[99, 95])).
% 0.61/0.80 tff(101,plain,(
% 0.61/0.80 ![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))),
% 0.61/0.80 inference(skolemize,[status(sab)],[100])).
% 0.61/0.80 tff(102,plain,
% 0.61/0.80 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[101, 94])).
% 0.61/0.80 tff(103,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | (s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(104,plain,
% 0.61/0.80 (((~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(elem!0, elem!0)) <=> (s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(105,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | (s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(monotonicity,[status(thm)],[104])).
% 0.61/0.80 tff(106,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.80 inference(transitivity,[status(thm)],[105, 103])).
% 0.61/0.80 tff(107,plain,
% 0.61/0.80 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(elem!0, elem!0))),
% 0.61/0.80 inference(quant_inst,[status(thm)],[])).
% 0.61/0.80 tff(108,plain,
% 0.61/0.80 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[107, 106])).
% 0.61/0.80 tff(109,plain,
% 0.61/0.80 ($false),
% 0.61/0.80 inference(unit_resolution,[status(thm)],[108, 102, 92, 1, 66])).
% 0.61/0.80 tff(110,plain,(q(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, f1(elem!0, elem!0))) | s(elem!0, elem!0)), inference(lemma,lemma(discharge,[]))).
% 0.61/0.80 tff(111,plain,
% 0.61/0.80 (q(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.61/0.80 inference(unit_resolution,[status(thm)],[110, 91, 1])).
% 0.61/0.80 tff(112,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, elem!0) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(113,plain,
% 0.61/0.80 (((~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0)) <=> (s(elem!0, elem!0) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(114,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, elem!0) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.61/0.80 inference(monotonicity,[status(thm)],[113])).
% 0.61/0.80 tff(115,plain,
% 0.61/0.80 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.61/0.80 inference(transitivity,[status(thm)],[114, 112])).
% 0.61/0.80 tff(116,plain,
% 0.61/0.80 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0))),
% 0.61/0.80 inference(quant_inst,[status(thm)],[])).
% 0.61/0.80 tff(117,plain,
% 0.61/0.80 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[116, 115])).
% 0.61/0.80 tff(118,plain,
% 0.61/0.80 ($false),
% 0.61/0.80 inference(unit_resolution,[status(thm)],[117, 82, 1, 111, 45])).
% 0.61/0.80 tff(119,plain,(p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | s(elem!0, elem!0)), inference(lemma,lemma(discharge,[]))).
% 0.61/0.80 tff(120,plain,
% 0.61/0.80 (p(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.61/0.80 inference(unit_resolution,[status(thm)],[119, 1])).
% 0.61/0.80 tff(121,assumption,(p(f1(elem!0, elem!0), f1(elem!0, elem!0))), introduced(assumption)).
% 0.61/0.80 tff(122,assumption,(~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))), introduced(assumption)).
% 0.61/0.80 tff(123,plain,
% 0.61/0.80 (^[Z: $i, X: $i, X1: $i] : refl(((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X))) <=> ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X))))),
% 0.61/0.80 inference(bind,[status(th)],[])).
% 0.61/0.80 tff(124,plain,
% 0.61/0.80 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X))) <=> ![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.61/0.80 inference(quant_intro,[status(thm)],[123])).
% 0.61/0.80 tff(125,plain,
% 0.61/0.80 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X))) <=> ![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.61/0.80 inference(rewrite,[status(thm)],[])).
% 0.61/0.80 tff(126,plain,
% 0.61/0.80 (^[Z: $i, X: $i, X1: $i] : rewrite((((~p(X, X)) | s(f1(X, X1), Z)) | (~q(X1, f1(X, X1)))) <=> ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X))))),
% 0.61/0.80 inference(bind,[status(th)],[])).
% 0.61/0.80 tff(127,plain,
% 0.61/0.80 (![Z: $i, X: $i, X1: $i] : (((~p(X, X)) | s(f1(X, X1), Z)) | (~q(X1, f1(X, X1)))) <=> ![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.61/0.80 inference(quant_intro,[status(thm)],[126])).
% 0.61/0.80 tff(128,axiom,(![Z: $i, X: $i, X1: $i] : (((~p(X, X)) | s(f1(X, X1), Z)) | (~q(X1, f1(X, X1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_13')).
% 0.61/0.80 tff(129,plain,
% 0.61/0.80 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[128, 127])).
% 0.61/0.80 tff(130,plain,
% 0.61/0.80 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.61/0.80 inference(modus_ponens,[status(thm)],[129, 125])).
% 0.61/0.80 tff(131,plain,(
% 0.61/0.80 ![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.65/0.81 inference(skolemize,[status(sab)],[130])).
% 0.65/0.81 tff(132,plain,
% 0.65/0.81 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[131, 124])).
% 0.65/0.81 tff(133,plain,
% 0.65/0.81 (((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.81 inference(rewrite,[status(thm)],[])).
% 0.65/0.81 tff(134,plain,
% 0.65/0.81 (((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> ((~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.81 inference(rewrite,[status(thm)],[])).
% 0.65/0.81 tff(135,plain,
% 0.65/0.81 (((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))))),
% 0.65/0.81 inference(monotonicity,[status(thm)],[134])).
% 0.65/0.81 tff(136,plain,
% 0.65/0.81 (((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.81 inference(transitivity,[status(thm)],[135, 133])).
% 0.65/0.81 tff(137,plain,
% 0.65/0.81 ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.81 inference(quant_inst,[status(thm)],[])).
% 0.65/0.81 tff(138,plain,
% 0.65/0.81 ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | s(f1(X, X1), Z) | (~p(X, X)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[137, 136])).
% 0.65/0.81 tff(139,plain,
% 0.65/0.81 (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.81 inference(unit_resolution,[status(thm)],[138, 132, 121, 122])).
% 0.65/0.81 tff(140,plain,
% 0.65/0.81 (^[Z: $i, Z1: $i, X: $i, X1: $i] : refl((q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X)) <=> (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X)))),
% 0.65/0.81 inference(bind,[status(th)],[])).
% 0.65/0.81 tff(141,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))),
% 0.65/0.81 inference(quant_intro,[status(thm)],[140])).
% 0.65/0.81 tff(142,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))),
% 0.65/0.81 inference(rewrite,[status(thm)],[])).
% 0.65/0.81 tff(143,plain,
% 0.65/0.81 (^[Z: $i, Z1: $i, X: $i, X1: $i] : trans(monotonicity(rewrite((s(Z, X) | (~q(Z1, Z1))) <=> ((~q(Z1, Z1)) | s(Z, X))), (((s(Z, X) | (~q(Z1, Z1))) | q(f1(X, X1), Z1)) <=> (((~q(Z1, Z1)) | s(Z, X)) | q(f1(X, X1), Z1)))), rewrite((((~q(Z1, Z1)) | s(Z, X)) | q(f1(X, X1), Z1)) <=> (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))), (((s(Z, X) | (~q(Z1, Z1))) | q(f1(X, X1), Z1)) <=> (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))))),
% 0.65/0.81 inference(bind,[status(th)],[])).
% 0.65/0.81 tff(144,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : ((s(Z, X) | (~q(Z1, Z1))) | q(f1(X, X1), Z1)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))),
% 0.65/0.81 inference(quant_intro,[status(thm)],[143])).
% 0.65/0.81 tff(145,axiom,(![Z: $i, Z1: $i, X: $i, X1: $i] : ((s(Z, X) | (~q(Z1, Z1))) | q(f1(X, X1), Z1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_26')).
% 0.65/0.81 tff(146,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[145, 144])).
% 0.65/0.81 tff(147,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[146, 142])).
% 0.65/0.81 tff(148,plain,(
% 0.65/0.81 ![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))),
% 0.65/0.81 inference(skolemize,[status(sab)],[147])).
% 0.65/0.81 tff(149,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[148, 141])).
% 0.65/0.81 tff(150,plain,
% 0.65/0.81 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, elem!0) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.65/0.81 inference(rewrite,[status(thm)],[])).
% 0.65/0.81 tff(151,plain,
% 0.65/0.81 ((q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(elem!0, elem!0)) <=> (s(elem!0, elem!0) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.65/0.81 inference(rewrite,[status(thm)],[])).
% 0.65/0.81 tff(152,plain,
% 0.65/0.81 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, elem!0) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))))),
% 0.65/0.81 inference(monotonicity,[status(thm)],[151])).
% 0.65/0.81 tff(153,plain,
% 0.65/0.81 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.65/0.81 inference(transitivity,[status(thm)],[152, 150])).
% 0.65/0.81 tff(154,plain,
% 0.65/0.81 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(elem!0, elem!0))),
% 0.65/0.81 inference(quant_inst,[status(thm)],[])).
% 0.65/0.81 tff(155,plain,
% 0.65/0.81 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[154, 153])).
% 0.65/0.81 tff(156,plain,
% 0.65/0.81 (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.81 inference(unit_resolution,[status(thm)],[155, 149, 1, 139])).
% 0.65/0.81 tff(157,plain,
% 0.65/0.81 (^[Z: $i, Z1: $i, X: $i, X1: $i] : refl((q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X))) <=> (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X))))),
% 0.65/0.81 inference(bind,[status(th)],[])).
% 0.65/0.81 tff(158,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X))) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.65/0.81 inference(quant_intro,[status(thm)],[157])).
% 0.65/0.81 tff(159,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X))) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.65/0.81 inference(rewrite,[status(thm)],[])).
% 0.65/0.81 tff(160,plain,
% 0.65/0.81 (^[Z: $i, Z1: $i, X: $i, X1: $i] : rewrite((((~p(X, X)) | s(f1(X, X1), Z)) | q(f1(X, X1), Z1)) <=> (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X))))),
% 0.65/0.81 inference(bind,[status(th)],[])).
% 0.65/0.81 tff(161,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (((~p(X, X)) | s(f1(X, X1), Z)) | q(f1(X, X1), Z1)) <=> ![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.65/0.81 inference(quant_intro,[status(thm)],[160])).
% 0.65/0.81 tff(162,axiom,(![Z: $i, Z1: $i, X: $i, X1: $i] : (((~p(X, X)) | s(f1(X, X1), Z)) | q(f1(X, X1), Z1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_14')).
% 0.65/0.81 tff(163,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[162, 161])).
% 0.65/0.81 tff(164,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[163, 159])).
% 0.65/0.81 tff(165,plain,(
% 0.65/0.81 ![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.65/0.81 inference(skolemize,[status(sab)],[164])).
% 0.65/0.81 tff(166,plain,
% 0.65/0.81 (![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[165, 158])).
% 0.65/0.81 tff(167,plain,
% 0.65/0.81 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.81 inference(rewrite,[status(thm)],[])).
% 0.65/0.81 tff(168,plain,
% 0.65/0.81 ((q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> ((~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.81 inference(rewrite,[status(thm)],[])).
% 0.65/0.81 tff(169,plain,
% 0.65/0.81 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))) | (q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))))),
% 0.65/0.81 inference(monotonicity,[status(thm)],[168])).
% 0.65/0.81 tff(170,plain,
% 0.65/0.81 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))) | (q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.81 inference(transitivity,[status(thm)],[169, 167])).
% 0.65/0.81 tff(171,plain,
% 0.65/0.81 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))) | (q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.81 inference(quant_inst,[status(thm)],[])).
% 0.65/0.81 tff(172,plain,
% 0.65/0.81 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | s(f1(X, X1), Z) | (~p(X, X)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))),
% 0.65/0.81 inference(modus_ponens,[status(thm)],[171, 170])).
% 0.65/0.81 tff(173,plain,
% 0.65/0.81 ($false),
% 0.65/0.81 inference(unit_resolution,[status(thm)],[172, 166, 121, 122, 156])).
% 0.65/0.81 tff(174,plain,(s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0)), inference(lemma,lemma(discharge,[]))).
% 0.65/0.81 tff(175,plain,
% 0.65/0.81 (s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))),
% 0.65/0.81 inference(unit_resolution,[status(thm)],[174, 1, 121])).
% 0.65/0.81 tff(176,assumption,(s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))), introduced(assumption)).
% 0.65/0.81 tff(177,plain,
% 0.65/0.81 (^[Z: $i, X: $i, X1: $i] : refl(((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X)) <=> ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X)))),
% 0.65/0.81 inference(bind,[status(th)],[])).
% 0.65/0.81 tff(178,plain,
% 0.65/0.81 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X)) <=> ![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))),
% 0.65/0.81 inference(quant_intro,[status(thm)],[177])).
% 0.65/0.81 tff(179,plain,
% 0.65/0.81 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X)) <=> ![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))),
% 0.65/0.81 inference(rewrite,[status(thm)],[])).
% 0.65/0.81 tff(180,plain,
% 0.65/0.81 (^[Z: $i, X: $i, X1: $i] : trans(monotonicity(rewrite((s(Z, X) | (~s(X, f1(X, X1)))) <=> ((~s(X, f1(X, X1))) | s(Z, X))), (((s(Z, X) | (~s(X, f1(X, X1)))) | (~q(X1, f1(X, X1)))) <=> (((~s(X, f1(X, X1))) | s(Z, X)) | (~q(X1, f1(X, X1)))))), rewrite((((~s(X, f1(X, X1))) | s(Z, X)) | (~q(X1, f1(X, X1)))) <=> ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))), (((s(Z, X) | (~s(X, f1(X, X1)))) | (~q(X1, f1(X, X1)))) <=> ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))))),
% 0.65/0.81 inference(bind,[status(th)],[])).
% 0.65/0.81 tff(181,plain,
% 0.65/0.81 (![Z: $i, X: $i, X1: $i] : ((s(Z, X) | (~s(X, f1(X, X1)))) | (~q(X1, f1(X, X1)))) <=> ![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))),
% 0.65/0.81 inference(quant_intro,[status(thm)],[180])).
% 0.65/0.81 tff(182,axiom,(![Z: $i, X: $i, X1: $i] : ((s(Z, X) | (~s(X, f1(X, X1)))) | (~q(X1, f1(X, X1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_19')).
% 0.65/0.81 tff(183,plain,
% 0.65/0.81 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))),
% 0.65/0.82 inference(modus_ponens,[status(thm)],[182, 181])).
% 0.65/0.82 tff(184,plain,
% 0.65/0.82 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))),
% 0.65/0.82 inference(modus_ponens,[status(thm)],[183, 179])).
% 0.65/0.82 tff(185,plain,(
% 0.65/0.82 ![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))),
% 0.65/0.82 inference(skolemize,[status(sab)],[184])).
% 0.65/0.82 tff(186,plain,
% 0.65/0.82 (![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))),
% 0.65/0.82 inference(modus_ponens,[status(thm)],[185, 178])).
% 0.65/0.82 tff(187,plain,
% 0.65/0.82 (((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))) | ((~q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))) | (~q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.82 inference(rewrite,[status(thm)],[])).
% 0.65/0.82 tff(188,plain,
% 0.65/0.82 ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))) | ((~q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.82 inference(quant_inst,[status(thm)],[])).
% 0.65/0.82 tff(189,plain,
% 0.65/0.82 ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))) | (~q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.82 inference(modus_ponens,[status(thm)],[188, 187])).
% 0.65/0.82 tff(190,plain,
% 0.65/0.82 (~q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))),
% 0.65/0.82 inference(unit_resolution,[status(thm)],[189, 186, 176, 65])).
% 0.65/0.82 tff(191,plain,
% 0.65/0.82 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, elem!0) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.82 inference(rewrite,[status(thm)],[])).
% 0.65/0.82 tff(192,plain,
% 0.65/0.82 ((q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | s(elem!0, elem!0)) <=> (s(elem!0, elem!0) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.82 inference(rewrite,[status(thm)],[])).
% 0.65/0.82 tff(193,plain,
% 0.65/0.82 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (s(elem!0, elem!0) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))))),
% 0.65/0.82 inference(monotonicity,[status(thm)],[192])).
% 0.65/0.82 tff(194,plain,
% 0.65/0.82 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.82 inference(transitivity,[status(thm)],[193, 191])).
% 0.65/0.82 tff(195,plain,
% 0.65/0.82 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | (q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | s(elem!0, elem!0))),
% 0.65/0.82 inference(quant_inst,[status(thm)],[])).
% 0.65/0.82 tff(196,plain,
% 0.65/0.82 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : (q(f1(X, X1), Z1) | (~q(Z1, Z1)) | s(Z, X))) | s(elem!0, elem!0) | (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(elem!0, f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))),
% 0.65/0.82 inference(modus_ponens,[status(thm)],[195, 194])).
% 0.65/0.82 tff(197,plain,
% 0.65/0.82 (~q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))),
% 0.65/0.82 inference(unit_resolution,[status(thm)],[196, 149, 1, 190])).
% 0.65/0.82 tff(198,plain,
% 0.65/0.82 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | (s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.82 inference(rewrite,[status(thm)],[])).
% 0.65/0.82 tff(199,plain,
% 0.65/0.82 (((~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> (s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.82 inference(rewrite,[status(thm)],[])).
% 0.65/0.82 tff(200,plain,
% 0.65/0.82 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | (s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))))),
% 0.65/0.82 inference(monotonicity,[status(thm)],[199])).
% 0.65/0.82 tff(201,plain,
% 0.65/0.82 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))))),
% 0.65/0.82 inference(transitivity,[status(thm)],[200, 198])).
% 0.65/0.82 tff(202,plain,
% 0.65/0.82 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0)))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.82 inference(quant_inst,[status(thm)],[])).
% 0.65/0.82 tff(203,plain,
% 0.65/0.82 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | q(f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))),
% 0.65/0.82 inference(modus_ponens,[status(thm)],[202, 201])).
% 0.65/0.82 tff(204,plain,
% 0.65/0.82 ($false),
% 0.65/0.82 inference(unit_resolution,[status(thm)],[203, 102, 176, 65, 197])).
% 0.65/0.82 tff(205,plain,(s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(elem!0, f1(elem!0, elem!0))))) | s(elem!0, elem!0)), inference(lemma,lemma(discharge,[]))).
% 0.65/0.82 tff(206,plain,
% 0.65/0.82 (s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.82 inference(unit_resolution,[status(thm)],[205, 175, 1])).
% 0.65/0.82 tff(207,plain,
% 0.65/0.82 (((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))) | ((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(elem!0, f1(elem!0, elem!0)))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(elem!0, f1(elem!0, elem!0)))),
% 0.65/0.82 inference(rewrite,[status(thm)],[])).
% 0.65/0.82 tff(208,plain,
% 0.65/0.82 ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))) | ((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(elem!0, f1(elem!0, elem!0)))),
% 0.65/0.82 inference(quant_inst,[status(thm)],[])).
% 0.65/0.82 tff(209,plain,
% 0.65/0.82 ((~![Z: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~s(X, f1(X, X1))) | s(Z, X))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | s(elem!0, f1(elem!0, elem!0))),
% 0.65/0.82 inference(modus_ponens,[status(thm)],[208, 207])).
% 0.65/0.82 tff(210,plain,
% 0.65/0.82 ((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.82 inference(unit_resolution,[status(thm)],[209, 186, 47])).
% 0.65/0.82 tff(211,plain,
% 0.65/0.82 (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.82 inference(unit_resolution,[status(thm)],[210, 206])).
% 0.65/0.82 tff(212,plain,
% 0.65/0.82 (~q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.82 inference(unit_resolution,[status(thm)],[155, 149, 1, 211])).
% 0.65/0.82 tff(213,plain,
% 0.65/0.82 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | (s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.82 inference(rewrite,[status(thm)],[])).
% 0.65/0.82 tff(214,plain,
% 0.65/0.82 (((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0))) <=> (s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.82 inference(rewrite,[status(thm)],[])).
% 0.65/0.82 tff(215,plain,
% 0.65/0.82 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | (s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.65/0.83 inference(monotonicity,[status(thm)],[214])).
% 0.65/0.83 tff(216,plain,
% 0.65/0.83 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.83 inference(transitivity,[status(thm)],[215, 213])).
% 0.65/0.83 tff(217,plain,
% 0.65/0.83 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))),
% 0.65/0.83 inference(quant_inst,[status(thm)],[])).
% 0.65/0.83 tff(218,plain,
% 0.65/0.83 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(elem!0, f1(elem!0, elem!0)) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | q(f1(f1(elem!0, elem!0), f1(elem!0, elem!0)), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.83 inference(modus_ponens,[status(thm)],[217, 216])).
% 0.65/0.83 tff(219,plain,
% 0.65/0.83 ($false),
% 0.65/0.83 inference(unit_resolution,[status(thm)],[218, 102, 47, 206, 212])).
% 0.65/0.83 tff(220,plain,(s(elem!0, elem!0) | s(elem!0, f1(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0)))), inference(lemma,lemma(discharge,[]))).
% 0.65/0.83 tff(221,plain,
% 0.65/0.83 (s(elem!0, f1(elem!0, elem!0))),
% 0.65/0.83 inference(unit_resolution,[status(thm)],[220, 120, 1])).
% 0.65/0.83 tff(222,plain,
% 0.65/0.83 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | (s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.83 inference(rewrite,[status(thm)],[])).
% 0.65/0.83 tff(223,plain,
% 0.65/0.83 (((~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0)) <=> (s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.83 inference(rewrite,[status(thm)],[])).
% 0.65/0.83 tff(224,plain,
% 0.65/0.83 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | (s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.65/0.83 inference(monotonicity,[status(thm)],[223])).
% 0.65/0.83 tff(225,plain,
% 0.65/0.83 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.83 inference(transitivity,[status(thm)],[224, 222])).
% 0.65/0.83 tff(226,plain,
% 0.65/0.83 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | ((~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0))),
% 0.65/0.83 inference(quant_inst,[status(thm)],[])).
% 0.65/0.83 tff(227,plain,
% 0.65/0.83 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | q(f1(X, X1), Z1) | s(Z, X))) | s(elem!0, elem!0) | (~s(elem!0, f1(elem!0, elem!0))) | q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.83 inference(modus_ponens,[status(thm)],[226, 225])).
% 0.65/0.83 tff(228,plain,
% 0.65/0.83 ($false),
% 0.65/0.83 inference(unit_resolution,[status(thm)],[227, 102, 221, 1, 2])).
% 0.65/0.83 tff(229,plain,(q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, elem!0)), inference(lemma,lemma(discharge,[]))).
% 0.65/0.83 tff(230,plain,
% 0.65/0.83 (q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.83 inference(unit_resolution,[status(thm)],[229, 1])).
% 0.65/0.83 tff(231,plain,
% 0.65/0.83 (q(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.65/0.83 inference(unit_resolution,[status(thm)],[110, 221, 1])).
% 0.65/0.83 tff(232,plain,
% 0.65/0.83 (^[Z1: $i, X: $i, X1: $i] : refl(((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X))) <=> ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X))))),
% 0.65/0.83 inference(bind,[status(th)],[])).
% 0.65/0.83 tff(233,plain,
% 0.65/0.83 (![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X))) <=> ![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))),
% 0.65/0.83 inference(quant_intro,[status(thm)],[232])).
% 0.65/0.83 tff(234,plain,
% 0.65/0.83 (![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X))) <=> ![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))),
% 0.65/0.83 inference(rewrite,[status(thm)],[])).
% 0.65/0.83 tff(235,plain,
% 0.65/0.83 (^[Z1: $i, X: $i, X1: $i] : rewrite((((~p(X, X)) | (~q(Z1, Z1))) | (~q(X1, f1(X, X1)))) <=> ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X))))),
% 0.65/0.83 inference(bind,[status(th)],[])).
% 0.65/0.83 tff(236,plain,
% 0.65/0.83 (![Z1: $i, X: $i, X1: $i] : (((~p(X, X)) | (~q(Z1, Z1))) | (~q(X1, f1(X, X1)))) <=> ![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))),
% 0.65/0.83 inference(quant_intro,[status(thm)],[235])).
% 0.65/0.83 tff(237,axiom,(![Z1: $i, X: $i, X1: $i] : (((~p(X, X)) | (~q(Z1, Z1))) | (~q(X1, f1(X, X1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_16')).
% 0.65/0.83 tff(238,plain,
% 0.65/0.83 (![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))),
% 0.65/0.83 inference(modus_ponens,[status(thm)],[237, 236])).
% 0.65/0.83 tff(239,plain,
% 0.65/0.83 (![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))),
% 0.65/0.83 inference(modus_ponens,[status(thm)],[238, 234])).
% 0.65/0.83 tff(240,plain,(
% 0.65/0.83 ![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))),
% 0.65/0.83 inference(skolemize,[status(sab)],[239])).
% 0.65/0.83 tff(241,plain,
% 0.65/0.83 (![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))),
% 0.65/0.83 inference(modus_ponens,[status(thm)],[240, 233])).
% 0.65/0.83 tff(242,plain,
% 0.65/0.83 (((~![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))) | ((~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.83 inference(rewrite,[status(thm)],[])).
% 0.65/0.83 tff(243,plain,
% 0.65/0.83 (((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> ((~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.83 inference(rewrite,[status(thm)],[])).
% 0.65/0.83 tff(244,plain,
% 0.65/0.83 (((~![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))) | ((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))) | ((~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0)))))),
% 0.65/0.83 inference(monotonicity,[status(thm)],[243])).
% 0.65/0.83 tff(245,plain,
% 0.65/0.83 (((~![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))) | ((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.83 inference(transitivity,[status(thm)],[244, 242])).
% 0.65/0.83 tff(246,plain,
% 0.65/0.83 ((~![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))) | ((~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.65/0.83 inference(quant_inst,[status(thm)],[])).
% 0.65/0.83 tff(247,plain,
% 0.65/0.83 ((~![Z1: $i, X: $i, X1: $i] : ((~q(X1, f1(X, X1))) | (~q(Z1, Z1)) | (~p(X, X)))) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~q(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), f1(elem!0, elem!0)))) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.65/0.83 inference(modus_ponens,[status(thm)],[246, 245])).
% 0.65/0.83 tff(248,plain,
% 0.65/0.83 ($false),
% 0.65/0.83 inference(unit_resolution,[status(thm)],[247, 241, 120, 231, 230])).
% 0.65/0.83 tff(249,plain,(s(elem!0, elem!0)), inference(lemma,lemma(discharge,[]))).
% 0.65/0.83 tff(250,plain,
% 0.65/0.83 (^[X: $i, X1: $i] : refl(((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1))) <=> ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1))))),
% 0.65/0.83 inference(bind,[status(th)],[])).
% 0.65/0.83 tff(251,plain,
% 0.65/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1))) <=> ![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))),
% 0.65/0.83 inference(quant_intro,[status(thm)],[250])).
% 0.65/0.83 tff(252,plain,
% 0.65/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1))) <=> ![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))),
% 0.65/0.83 inference(rewrite,[status(thm)],[])).
% 0.65/0.83 tff(253,plain,
% 0.65/0.83 (^[X: $i, X1: $i] : trans(monotonicity(rewrite((p(f1(X, X1), f1(X, X1)) | (~s(X, f1(X, X1)))) <=> ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)))), (((p(f1(X, X1), f1(X, X1)) | (~s(X, f1(X, X1)))) | (~s(X1, X1))) <=> (((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1))) | (~s(X1, X1))))), rewrite((((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1))) | (~s(X1, X1))) <=> ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))), (((p(f1(X, X1), f1(X, X1)) | (~s(X, f1(X, X1)))) | (~s(X1, X1))) <=> ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))))),
% 0.65/0.83 inference(bind,[status(th)],[])).
% 0.65/0.83 tff(254,plain,
% 0.65/0.83 (![X: $i, X1: $i] : ((p(f1(X, X1), f1(X, X1)) | (~s(X, f1(X, X1)))) | (~s(X1, X1))) <=> ![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))),
% 0.65/0.83 inference(quant_intro,[status(thm)],[253])).
% 0.65/0.83 tff(255,axiom,(![X: $i, X1: $i] : ((p(f1(X, X1), f1(X, X1)) | (~s(X, f1(X, X1)))) | (~s(X1, X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_3')).
% 0.65/0.83 tff(256,plain,
% 0.65/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))),
% 0.65/0.83 inference(modus_ponens,[status(thm)],[255, 254])).
% 0.65/0.83 tff(257,plain,
% 0.65/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))),
% 0.65/0.83 inference(modus_ponens,[status(thm)],[256, 252])).
% 0.65/0.83 tff(258,plain,(
% 0.65/0.83 ![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))),
% 0.65/0.83 inference(skolemize,[status(sab)],[257])).
% 0.65/0.83 tff(259,plain,
% 0.65/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))),
% 0.65/0.83 inference(modus_ponens,[status(thm)],[258, 251])).
% 0.65/0.83 tff(260,plain,
% 0.65/0.83 (((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))) | ((~s(elem!0, elem!0)) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, f1(elem!0, elem!0))))) <=> ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))) | (~s(elem!0, elem!0)) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, f1(elem!0, elem!0))))),
% 0.67/0.83 inference(rewrite,[status(thm)],[])).
% 0.67/0.83 tff(261,plain,
% 0.67/0.83 (((~s(elem!0, f1(elem!0, elem!0))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, elem!0))) <=> ((~s(elem!0, elem!0)) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, f1(elem!0, elem!0))))),
% 0.67/0.83 inference(rewrite,[status(thm)],[])).
% 0.67/0.83 tff(262,plain,
% 0.67/0.83 (((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))) | ((~s(elem!0, f1(elem!0, elem!0))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, elem!0)))) <=> ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))) | ((~s(elem!0, elem!0)) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, f1(elem!0, elem!0)))))),
% 0.67/0.83 inference(monotonicity,[status(thm)],[261])).
% 0.67/0.83 tff(263,plain,
% 0.67/0.83 (((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))) | ((~s(elem!0, f1(elem!0, elem!0))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, elem!0)))) <=> ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))) | (~s(elem!0, elem!0)) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, f1(elem!0, elem!0))))),
% 0.67/0.83 inference(transitivity,[status(thm)],[262, 260])).
% 0.67/0.83 tff(264,plain,
% 0.67/0.83 ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))) | ((~s(elem!0, f1(elem!0, elem!0))) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, elem!0)))),
% 0.67/0.83 inference(quant_inst,[status(thm)],[])).
% 0.67/0.83 tff(265,plain,
% 0.67/0.83 ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | p(f1(X, X1), f1(X, X1)) | (~s(X1, X1)))) | (~s(elem!0, elem!0)) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, f1(elem!0, elem!0)))),
% 0.67/0.83 inference(modus_ponens,[status(thm)],[264, 263])).
% 0.67/0.83 tff(266,plain,
% 0.67/0.83 ((~s(elem!0, elem!0)) | p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, f1(elem!0, elem!0)))),
% 0.67/0.83 inference(unit_resolution,[status(thm)],[265, 259])).
% 0.67/0.83 tff(267,plain,
% 0.67/0.83 (p(f1(elem!0, elem!0), f1(elem!0, elem!0)) | (~s(elem!0, f1(elem!0, elem!0)))),
% 0.67/0.83 inference(unit_resolution,[status(thm)],[266, 249])).
% 0.67/0.83 tff(268,plain,
% 0.67/0.83 (~s(elem!0, f1(elem!0, elem!0))),
% 0.67/0.83 inference(unit_resolution,[status(thm)],[267, 3])).
% 0.67/0.83 tff(269,plain,
% 0.67/0.83 (~s(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.67/0.83 inference(unit_resolution,[status(thm)],[90, 268, 3])).
% 0.67/0.83 tff(270,plain,
% 0.67/0.83 (q(f1(elem!0, elem!0), f1(elem!0, elem!0))),
% 0.67/0.83 inference(unit_resolution,[status(thm)],[18, 269, 3])).
% 0.67/0.83 tff(271,plain,
% 0.67/0.83 (((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | ((~s(elem!0, elem!0)) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))) <=> ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | (~s(elem!0, elem!0)) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))),
% 0.67/0.83 inference(rewrite,[status(thm)],[])).
% 0.67/0.83 tff(272,plain,
% 0.67/0.83 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | ((~s(elem!0, elem!0)) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0)))),
% 0.67/0.83 inference(quant_inst,[status(thm)],[])).
% 0.67/0.83 tff(273,plain,
% 0.67/0.83 ((~![Z: $i, Z1: $i, X: $i, X1: $i] : ((~s(X1, X1)) | (~q(Z1, Z1)) | s(Z, X))) | (~s(elem!0, elem!0)) | (~q(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(elem!0, f1(elem!0, elem!0))),
% 0.67/0.83 inference(modus_ponens,[status(thm)],[272, 271])).
% 0.67/0.83 tff(274,plain,
% 0.67/0.83 ($false),
% 0.67/0.83 inference(unit_resolution,[status(thm)],[273, 82, 268, 249, 270])).
% 0.67/0.83 tff(275,plain,(p(f1(elem!0, elem!0), f1(elem!0, elem!0))), inference(lemma,lemma(discharge,[]))).
% 0.67/0.83 tff(276,plain,
% 0.67/0.83 (^[X: $i, X1: $i] : refl(((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X))) <=> ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X))))),
% 0.67/0.83 inference(bind,[status(th)],[])).
% 0.67/0.83 tff(277,plain,
% 0.67/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X))) <=> ![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))),
% 0.67/0.83 inference(quant_intro,[status(thm)],[276])).
% 0.67/0.83 tff(278,plain,
% 0.67/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X))) <=> ![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))),
% 0.67/0.83 inference(rewrite,[status(thm)],[])).
% 0.67/0.83 tff(279,plain,
% 0.67/0.83 (^[X: $i, X1: $i] : rewrite((((~p(X, X)) | (~s(X, f1(X, X1)))) | (~s(X1, X1))) <=> ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X))))),
% 0.67/0.83 inference(bind,[status(th)],[])).
% 0.67/0.83 tff(280,plain,
% 0.67/0.83 (![X: $i, X1: $i] : (((~p(X, X)) | (~s(X, f1(X, X1)))) | (~s(X1, X1))) <=> ![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))),
% 0.67/0.83 inference(quant_intro,[status(thm)],[279])).
% 0.67/0.83 tff(281,axiom,(![X: $i, X1: $i] : (((~p(X, X)) | (~s(X, f1(X, X1)))) | (~s(X1, X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_12')).
% 0.67/0.83 tff(282,plain,
% 0.67/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))),
% 0.67/0.83 inference(modus_ponens,[status(thm)],[281, 280])).
% 0.67/0.83 tff(283,plain,
% 0.67/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))),
% 0.67/0.83 inference(modus_ponens,[status(thm)],[282, 278])).
% 0.67/0.83 tff(284,plain,(
% 0.67/0.83 ![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))),
% 0.67/0.83 inference(skolemize,[status(sab)],[283])).
% 0.67/0.83 tff(285,plain,
% 0.67/0.83 (![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))),
% 0.67/0.83 inference(modus_ponens,[status(thm)],[284, 277])).
% 0.67/0.83 tff(286,plain,
% 0.67/0.83 (((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))) | ((~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))))) <=> ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))))),
% 0.67/0.83 inference(rewrite,[status(thm)],[])).
% 0.67/0.83 tff(287,plain,
% 0.67/0.83 (((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> ((~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))))),
% 0.67/0.83 inference(rewrite,[status(thm)],[])).
% 0.67/0.83 tff(288,plain,
% 0.67/0.83 (((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))) | ((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))) | ((~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)))))),
% 0.67/0.83 inference(monotonicity,[status(thm)],[287])).
% 0.67/0.83 tff(289,plain,
% 0.67/0.83 (((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))) | ((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))))),
% 0.67/0.83 inference(transitivity,[status(thm)],[288, 286])).
% 0.67/0.83 tff(290,plain,
% 0.67/0.83 ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))) | ((~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.67/0.83 inference(quant_inst,[status(thm)],[])).
% 0.67/0.83 tff(291,plain,
% 0.67/0.83 ((~![X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | (~p(X, X)))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)))),
% 0.67/0.83 inference(modus_ponens,[status(thm)],[290, 289])).
% 0.67/0.83 tff(292,plain,
% 0.67/0.83 (~s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))),
% 0.67/0.83 inference(unit_resolution,[status(thm)],[291, 285, 275, 249])).
% 0.67/0.83 tff(293,assumption,(~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))), introduced(assumption)).
% 0.67/0.84 tff(294,assumption,(s(elem!0, elem!0)), introduced(assumption)).
% 0.67/0.84 tff(295,plain,
% 0.67/0.84 (^[Z: $i, X: $i, X1: $i] : refl(((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X))) <=> ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X))))),
% 0.67/0.84 inference(bind,[status(th)],[])).
% 0.67/0.84 tff(296,plain,
% 0.67/0.84 (![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X))) <=> ![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.67/0.84 inference(quant_intro,[status(thm)],[295])).
% 0.67/0.84 tff(297,plain,
% 0.67/0.84 (![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X))) <=> ![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.67/0.84 inference(rewrite,[status(thm)],[])).
% 0.67/0.84 tff(298,plain,
% 0.67/0.84 (^[Z: $i, X: $i, X1: $i] : rewrite((((~p(X, X)) | s(f1(X, X1), Z)) | (~s(X1, X1))) <=> ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X))))),
% 0.67/0.84 inference(bind,[status(th)],[])).
% 0.67/0.84 tff(299,plain,
% 0.67/0.84 (![Z: $i, X: $i, X1: $i] : (((~p(X, X)) | s(f1(X, X1), Z)) | (~s(X1, X1))) <=> ![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.67/0.84 inference(quant_intro,[status(thm)],[298])).
% 0.67/0.84 tff(300,axiom,(![Z: $i, X: $i, X1: $i] : (((~p(X, X)) | s(f1(X, X1), Z)) | (~s(X1, X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','c_15')).
% 0.67/0.84 tff(301,plain,
% 0.67/0.84 (![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.67/0.84 inference(modus_ponens,[status(thm)],[300, 299])).
% 0.67/0.84 tff(302,plain,
% 0.67/0.84 (![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.67/0.84 inference(modus_ponens,[status(thm)],[301, 297])).
% 0.67/0.84 tff(303,plain,(
% 0.67/0.84 ![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.67/0.84 inference(skolemize,[status(sab)],[302])).
% 0.67/0.84 tff(304,plain,
% 0.67/0.84 (![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))),
% 0.67/0.84 inference(modus_ponens,[status(thm)],[303, 296])).
% 0.67/0.84 tff(305,plain,
% 0.67/0.84 (((~![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)))),
% 0.67/0.84 inference(rewrite,[status(thm)],[])).
% 0.67/0.84 tff(306,plain,
% 0.67/0.84 (((~s(elem!0, elem!0)) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0)))) <=> ((~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)))),
% 0.67/0.84 inference(rewrite,[status(thm)],[])).
% 0.67/0.84 tff(307,plain,
% 0.67/0.84 (((~![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~s(elem!0, elem!0)) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))))),
% 0.67/0.84 inference(monotonicity,[status(thm)],[306])).
% 0.67/0.84 tff(308,plain,
% 0.67/0.84 (((~![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~s(elem!0, elem!0)) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)))),
% 0.67/0.84 inference(transitivity,[status(thm)],[307, 305])).
% 0.67/0.84 tff(309,plain,
% 0.67/0.84 ((~![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))) | ((~s(elem!0, elem!0)) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))))),
% 0.67/0.84 inference(quant_inst,[status(thm)],[])).
% 0.67/0.84 tff(310,plain,
% 0.67/0.84 ((~![Z: $i, X: $i, X1: $i] : ((~s(X1, X1)) | s(f1(X, X1), Z) | (~p(X, X)))) | (~s(elem!0, elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))),
% 0.67/0.84 inference(modus_ponens,[status(thm)],[309, 308])).
% 0.67/0.84 tff(311,plain,
% 0.67/0.84 ($false),
% 0.67/0.84 inference(unit_resolution,[status(thm)],[310, 304, 121, 294, 293])).
% 0.67/0.84 tff(312,plain,(s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0))) | (~s(elem!0, elem!0))), inference(lemma,lemma(discharge,[]))).
% 0.67/0.84 tff(313,plain,
% 0.67/0.84 (s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)) | (~p(f1(elem!0, elem!0), f1(elem!0, elem!0)))),
% 0.67/0.84 inference(unit_resolution,[status(thm)],[312, 249])).
% 0.67/0.84 tff(314,plain,
% 0.67/0.84 (s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))),
% 0.67/0.84 inference(unit_resolution,[status(thm)],[313, 275])).
% 0.67/0.84 tff(315,plain,
% 0.67/0.84 (((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | ((~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)) | (~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | (~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)) | (~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))))),
% 0.67/0.84 inference(rewrite,[status(thm)],[])).
% 0.67/0.84 tff(316,plain,
% 0.67/0.84 (((~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))) | (~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0))) <=> ((~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)) | (~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))))),
% 0.67/0.84 inference(rewrite,[status(thm)],[])).
% 0.67/0.84 tff(317,plain,
% 0.67/0.84 (((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | ((~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))) | (~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | ((~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)) | (~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)))))),
% 0.67/0.84 inference(monotonicity,[status(thm)],[316])).
% 0.67/0.84 tff(318,plain,
% 0.67/0.84 (((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | ((~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))) | (~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)))) <=> ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | (~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)) | (~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))))),
% 0.67/0.84 inference(transitivity,[status(thm)],[317, 315])).
% 0.67/0.84 tff(319,plain,
% 0.67/0.84 ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | ((~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0))) | (~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)))),
% 0.67/0.84 inference(quant_inst,[status(thm)],[])).
% 0.67/0.84 tff(320,plain,
% 0.67/0.84 ((~![Z: $i, X: $i, X1: $i] : ((~s(X, f1(X, X1))) | (~s(X1, X1)) | s(Z, X))) | (~s(elem!0, elem!0)) | s(f1(elem!0, elem!0), f1(f1(elem!0, elem!0), elem!0)) | (~s(f1(f1(elem!0, elem!0), elem!0), f1(f1(f1(elem!0, elem!0), elem!0), elem!0)))),
% 0.67/0.84 inference(modus_ponens,[status(thm)],[319, 318])).
% 0.67/0.84 tff(321,plain,
% 0.67/0.84 ($false),
% 0.67/0.84 inference(unit_resolution,[status(thm)],[320, 57, 249, 314, 292])).
% 0.67/0.84 % SZS output end Proof
% 0.67/0.84 % E exiting
%------------------------------------------------------------------------------