%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : CSR018+1 : TPTP v9.0.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.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:01:13 AM UTC 2025
% Result : Theorem 0.94s 1.15s
% Output : Proof 1.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR018+1 : TPTP v9.0.0. Bugfixed v3.1.0.
% 0.11/0.12 % Command : run_E %s %d THM
% 0.12/0.32 % Computer : n006.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu Jun 19 12:26:50 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.94/1.15 % SZS status Theorem
% 0.94/1.15 % SZS output start Proof
% 0.94/1.15 tff(n1_type, type, (
% 0.94/1.15 n1: $i)).
% 0.94/1.15 tff(n2_type, type, (
% 0.94/1.15 n2: $i)).
% 0.94/1.15 tff(n0_type, type, (
% 0.94/1.15 n0: $i)).
% 0.94/1.15 tff(pull_type, type, (
% 0.94/1.15 pull: $i)).
% 0.94/1.15 tff(push_type, type, (
% 0.94/1.15 push: $i)).
% 0.94/1.15 tff(happens_type, type, (
% 0.94/1.15 happens: ( $i * $i ) > $o)).
% 0.94/1.15 tff(spinning_type, type, (
% 0.94/1.15 spinning: $i)).
% 0.94/1.15 tff(backwards_type, type, (
% 0.94/1.15 backwards: $i)).
% 0.94/1.15 tff(forwards_type, type, (
% 0.94/1.15 forwards: $i)).
% 0.94/1.15 tff(initiates_type, type, (
% 0.94/1.15 initiates: ( $i * $i * $i ) > $o)).
% 0.94/1.15 tff(holdsAt_type, type, (
% 0.94/1.15 holdsAt: ( $i * $i ) > $o)).
% 0.94/1.15 tff(plus_type, type, (
% 0.94/1.15 plus: ( $i * $i ) > $i)).
% 0.94/1.15 tff(n3_type, type, (
% 0.94/1.15 n3: $i)).
% 0.94/1.15 tff(less_type, type, (
% 0.94/1.15 less: ( $i * $i ) > $o)).
% 0.94/1.15 tff(n4_type, type, (
% 0.94/1.15 n4: $i)).
% 0.94/1.15 tff(less_or_equal_type, type, (
% 0.94/1.15 less_or_equal: ( $i * $i ) > $o)).
% 0.94/1.15 tff(1,plain,
% 0.94/1.15 (^[Event: $i, Fluent: $i, Time: $i] : refl((initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning)))))) <=> (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning)))))))),
% 0.94/1.15 inference(bind,[status(th)],[])).
% 0.94/1.15 tff(2,plain,
% 0.94/1.15 (![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning)))))) <=> ![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))),
% 0.94/1.15 inference(quant_intro,[status(thm)],[1])).
% 0.94/1.15 tff(3,plain,
% 0.94/1.15 (^[Event: $i, Fluent: $i, Time: $i] : rewrite((initiates(Event, Fluent, Time) <=> (((Event = push) & (Fluent = forwards) & (~happens(pull, Time))) | ((Event = pull) & (Fluent = backwards) & (~happens(push, Time))) | ((Event = pull) & (Fluent = spinning) & happens(push, Time)))) <=> (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning)))))))),
% 0.94/1.15 inference(bind,[status(th)],[])).
% 0.94/1.15 tff(4,plain,
% 0.94/1.15 (![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> (((Event = push) & (Fluent = forwards) & (~happens(pull, Time))) | ((Event = pull) & (Fluent = backwards) & (~happens(push, Time))) | ((Event = pull) & (Fluent = spinning) & happens(push, Time)))) <=> ![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))),
% 0.94/1.15 inference(quant_intro,[status(thm)],[3])).
% 0.94/1.15 tff(5,plain,
% 0.94/1.15 (![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> (((Event = push) & (Fluent = forwards) & (~happens(pull, Time))) | ((Event = pull) & (Fluent = backwards) & (~happens(push, Time))) | ((Event = pull) & (Fluent = spinning) & happens(push, Time)))) <=> ![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> (((Event = push) & (Fluent = forwards) & (~happens(pull, Time))) | ((Event = pull) & (Fluent = backwards) & (~happens(push, Time))) | ((Event = pull) & (Fluent = spinning) & happens(push, Time))))),
% 0.94/1.15 inference(rewrite,[status(thm)],[])).
% 0.94/1.15 tff(6,plain,
% 0.94/1.15 (^[Event: $i, Fluent: $i, Time: $i] : rewrite((initiates(Event, Fluent, Time) <=> (((((Event = push) & (Fluent = forwards)) & (~happens(pull, Time))) | (((Event = pull) & (Fluent = backwards)) & (~happens(push, Time)))) | (((Event = pull) & (Fluent = spinning)) & happens(push, Time)))) <=> (initiates(Event, Fluent, Time) <=> (((Event = push) & (Fluent = forwards) & (~happens(pull, Time))) | ((Event = pull) & (Fluent = backwards) & (~happens(push, Time))) | ((Event = pull) & (Fluent = spinning) & happens(push, Time)))))),
% 0.94/1.15 inference(bind,[status(th)],[])).
% 0.94/1.15 tff(7,plain,
% 0.94/1.15 (![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> (((((Event = push) & (Fluent = forwards)) & (~happens(pull, Time))) | (((Event = pull) & (Fluent = backwards)) & (~happens(push, Time)))) | (((Event = pull) & (Fluent = spinning)) & happens(push, Time)))) <=> ![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> (((Event = push) & (Fluent = forwards) & (~happens(pull, Time))) | ((Event = pull) & (Fluent = backwards) & (~happens(push, Time))) | ((Event = pull) & (Fluent = spinning) & happens(push, Time))))),
% 0.94/1.15 inference(quant_intro,[status(thm)],[6])).
% 0.94/1.15 tff(8,axiom,(![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> (((((Event = push) & (Fluent = forwards)) & (~happens(pull, Time))) | (((Event = pull) & (Fluent = backwards)) & (~happens(push, Time)))) | (((Event = pull) & (Fluent = spinning)) & happens(push, Time))))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+2.ax','initiates_all_defn')).
% 0.94/1.15 tff(9,plain,
% 0.94/1.15 (![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> (((Event = push) & (Fluent = forwards) & (~happens(pull, Time))) | ((Event = pull) & (Fluent = backwards) & (~happens(push, Time))) | ((Event = pull) & (Fluent = spinning) & happens(push, Time))))),
% 0.94/1.15 inference(modus_ponens,[status(thm)],[8, 7])).
% 0.94/1.15 tff(10,plain,
% 0.94/1.15 (![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> (((Event = push) & (Fluent = forwards) & (~happens(pull, Time))) | ((Event = pull) & (Fluent = backwards) & (~happens(push, Time))) | ((Event = pull) & (Fluent = spinning) & happens(push, Time))))),
% 0.94/1.15 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.94/1.15 tff(11,plain,(
% 0.94/1.15 ![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> (((Event = push) & (Fluent = forwards) & (~happens(pull, Time))) | ((Event = pull) & (Fluent = backwards) & (~happens(push, Time))) | ((Event = pull) & (Fluent = spinning) & happens(push, Time))))),
% 0.94/1.15 inference(skolemize,[status(sab)],[10])).
% 0.94/1.15 tff(12,plain,
% 0.94/1.15 (![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))),
% 0.94/1.15 inference(modus_ponens,[status(thm)],[11, 4])).
% 0.94/1.15 tff(13,plain,
% 0.94/1.15 (![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))),
% 0.94/1.15 inference(modus_ponens,[status(thm)],[12, 2])).
% 0.94/1.15 tff(14,plain,
% 0.94/1.15 (((~![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))) | (initiates(pull, backwards, n1) <=> ((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1))))))) <=> ((~![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))) | (initiates(pull, backwards, n1) <=> ((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1)))))))),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(15,plain,
% 0.94/1.16 ((initiates(pull, backwards, n1) <=> ((~(happens(pull, n1) | (~(pull = push)) | (~(backwards = forwards)))) | (~(happens(push, n1) | (~(pull = pull)) | (~(backwards = backwards)))) | (~((~happens(push, n1)) | (~(pull = pull)) | (~(backwards = spinning)))))) <=> (initiates(pull, backwards, n1) <=> ((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1))))))),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(16,plain,
% 0.94/1.16 (((~![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))) | (initiates(pull, backwards, n1) <=> ((~(happens(pull, n1) | (~(pull = push)) | (~(backwards = forwards)))) | (~(happens(push, n1) | (~(pull = pull)) | (~(backwards = backwards)))) | (~((~happens(push, n1)) | (~(pull = pull)) | (~(backwards = spinning))))))) <=> ((~![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))) | (initiates(pull, backwards, n1) <=> ((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1)))))))),
% 0.94/1.16 inference(monotonicity,[status(thm)],[15])).
% 0.94/1.16 tff(17,plain,
% 0.94/1.16 (((~![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))) | (initiates(pull, backwards, n1) <=> ((~(happens(pull, n1) | (~(pull = push)) | (~(backwards = forwards)))) | (~(happens(push, n1) | (~(pull = pull)) | (~(backwards = backwards)))) | (~((~happens(push, n1)) | (~(pull = pull)) | (~(backwards = spinning))))))) <=> ((~![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))) | (initiates(pull, backwards, n1) <=> ((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1)))))))),
% 0.94/1.16 inference(transitivity,[status(thm)],[16, 14])).
% 0.94/1.16 tff(18,plain,
% 0.94/1.16 ((~![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))) | (initiates(pull, backwards, n1) <=> ((~(happens(pull, n1) | (~(pull = push)) | (~(backwards = forwards)))) | (~(happens(push, n1) | (~(pull = pull)) | (~(backwards = backwards)))) | (~((~happens(push, n1)) | (~(pull = pull)) | (~(backwards = spinning))))))),
% 0.94/1.16 inference(quant_inst,[status(thm)],[])).
% 0.94/1.16 tff(19,plain,
% 0.94/1.16 ((~![Event: $i, Fluent: $i, Time: $i] : (initiates(Event, Fluent, Time) <=> ((~(happens(pull, Time) | (~(Event = push)) | (~(Fluent = forwards)))) | (~(happens(push, Time) | (~(Event = pull)) | (~(Fluent = backwards)))) | (~((~happens(push, Time)) | (~(Event = pull)) | (~(Fluent = spinning))))))) | (initiates(pull, backwards, n1) <=> ((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1))))))),
% 0.94/1.16 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.94/1.16 tff(20,plain,
% 0.94/1.16 (initiates(pull, backwards, n1) <=> ((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1)))))),
% 0.94/1.16 inference(unit_resolution,[status(thm)],[19, 13])).
% 0.94/1.16 tff(21,plain,
% 0.94/1.16 (^[Event: $i, Time: $i] : refl((happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0)))))) <=> (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0)))))))),
% 0.94/1.16 inference(bind,[status(th)],[])).
% 0.94/1.16 tff(22,plain,
% 0.94/1.16 (![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0)))))) <=> ![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))),
% 0.94/1.16 inference(quant_intro,[status(thm)],[21])).
% 0.94/1.16 tff(23,plain,
% 0.94/1.16 (^[Event: $i, Time: $i] : rewrite((happens(Event, Time) <=> (((Event = push) & (Time = n2)) | ((Event = pull) & (Time = n2)) | ((Event = pull) & (Time = n1)) | ((Event = push) & (Time = n0)))) <=> (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0)))))))),
% 0.94/1.16 inference(bind,[status(th)],[])).
% 0.94/1.16 tff(24,plain,
% 0.94/1.16 (![Event: $i, Time: $i] : (happens(Event, Time) <=> (((Event = push) & (Time = n2)) | ((Event = pull) & (Time = n2)) | ((Event = pull) & (Time = n1)) | ((Event = push) & (Time = n0)))) <=> ![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))),
% 0.94/1.16 inference(quant_intro,[status(thm)],[23])).
% 0.94/1.16 tff(25,plain,
% 0.94/1.16 (![Event: $i, Time: $i] : (happens(Event, Time) <=> (((Event = push) & (Time = n2)) | ((Event = pull) & (Time = n2)) | ((Event = pull) & (Time = n1)) | ((Event = push) & (Time = n0)))) <=> ![Event: $i, Time: $i] : (happens(Event, Time) <=> (((Event = push) & (Time = n2)) | ((Event = pull) & (Time = n2)) | ((Event = pull) & (Time = n1)) | ((Event = push) & (Time = n0))))),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(26,plain,
% 0.94/1.16 (^[Event: $i, Time: $i] : rewrite((happens(Event, Time) <=> (((((Event = push) & (Time = n0)) | ((Event = pull) & (Time = n1))) | ((Event = pull) & (Time = n2))) | ((Event = push) & (Time = n2)))) <=> (happens(Event, Time) <=> (((Event = push) & (Time = n2)) | ((Event = pull) & (Time = n2)) | ((Event = pull) & (Time = n1)) | ((Event = push) & (Time = n0)))))),
% 0.94/1.16 inference(bind,[status(th)],[])).
% 0.94/1.16 tff(27,plain,
% 0.94/1.16 (![Event: $i, Time: $i] : (happens(Event, Time) <=> (((((Event = push) & (Time = n0)) | ((Event = pull) & (Time = n1))) | ((Event = pull) & (Time = n2))) | ((Event = push) & (Time = n2)))) <=> ![Event: $i, Time: $i] : (happens(Event, Time) <=> (((Event = push) & (Time = n2)) | ((Event = pull) & (Time = n2)) | ((Event = pull) & (Time = n1)) | ((Event = push) & (Time = n0))))),
% 0.94/1.16 inference(quant_intro,[status(thm)],[26])).
% 0.94/1.16 tff(28,axiom,(![Event: $i, Time: $i] : (happens(Event, Time) <=> (((((Event = push) & (Time = n0)) | ((Event = pull) & (Time = n1))) | ((Event = pull) & (Time = n2))) | ((Event = push) & (Time = n2))))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+2.ax','happens_all_defn')).
% 0.94/1.16 tff(29,plain,
% 0.94/1.16 (![Event: $i, Time: $i] : (happens(Event, Time) <=> (((Event = push) & (Time = n2)) | ((Event = pull) & (Time = n2)) | ((Event = pull) & (Time = n1)) | ((Event = push) & (Time = n0))))),
% 0.94/1.16 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.94/1.16 tff(30,plain,
% 0.94/1.16 (![Event: $i, Time: $i] : (happens(Event, Time) <=> (((Event = push) & (Time = n2)) | ((Event = pull) & (Time = n2)) | ((Event = pull) & (Time = n1)) | ((Event = push) & (Time = n0))))),
% 0.94/1.16 inference(modus_ponens,[status(thm)],[29, 25])).
% 0.94/1.16 tff(31,plain,(
% 0.94/1.16 ![Event: $i, Time: $i] : (happens(Event, Time) <=> (((Event = push) & (Time = n2)) | ((Event = pull) & (Time = n2)) | ((Event = pull) & (Time = n1)) | ((Event = push) & (Time = n0))))),
% 0.94/1.16 inference(skolemize,[status(sab)],[30])).
% 0.94/1.16 tff(32,plain,
% 0.94/1.16 (![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))),
% 0.94/1.16 inference(modus_ponens,[status(thm)],[31, 24])).
% 0.94/1.16 tff(33,plain,
% 0.94/1.16 (![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))),
% 0.94/1.16 inference(modus_ponens,[status(thm)],[32, 22])).
% 0.94/1.16 tff(34,plain,
% 0.94/1.16 (((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | happens(pull, n1)) <=> ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | happens(pull, n1))),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(35,plain,
% 0.94/1.16 ((happens(pull, n1) <=> $true) <=> happens(pull, n1)),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(36,plain,
% 0.94/1.16 (((~((~(pull = push)) | (~(n1 = n2)))) | (n1 = n2) | $true | (~((~(pull = push)) | (~(n1 = n0))))) <=> $true),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(37,plain,
% 0.94/1.16 ((~((~(pull = push)) | (~(n1 = n0)))) <=> (~((~(pull = push)) | (~(n1 = n0))))),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(38,plain,
% 0.94/1.16 ((~$false) <=> $true),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(39,plain,
% 0.94/1.16 (($false | $false) <=> $false),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(40,plain,
% 0.94/1.16 ((~$true) <=> $false),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(41,plain,
% 0.94/1.16 ((n1 = n1) <=> $true),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(42,plain,
% 0.94/1.16 ((~(n1 = n1)) <=> (~$true)),
% 0.94/1.16 inference(monotonicity,[status(thm)],[41])).
% 0.94/1.16 tff(43,plain,
% 0.94/1.16 ((~(n1 = n1)) <=> $false),
% 0.94/1.16 inference(transitivity,[status(thm)],[42, 40])).
% 0.94/1.16 tff(44,plain,
% 0.94/1.16 ((pull = pull) <=> $true),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(45,plain,
% 0.94/1.16 ((~(pull = pull)) <=> (~$true)),
% 0.94/1.16 inference(monotonicity,[status(thm)],[44])).
% 0.94/1.16 tff(46,plain,
% 0.94/1.16 ((~(pull = pull)) <=> $false),
% 0.94/1.16 inference(transitivity,[status(thm)],[45, 40])).
% 0.94/1.16 tff(47,plain,
% 0.94/1.16 (((~(pull = pull)) | (~(n1 = n1))) <=> ($false | $false)),
% 0.94/1.16 inference(monotonicity,[status(thm)],[46, 43])).
% 0.94/1.16 tff(48,plain,
% 0.94/1.16 (((~(pull = pull)) | (~(n1 = n1))) <=> $false),
% 0.94/1.16 inference(transitivity,[status(thm)],[47, 39])).
% 0.94/1.16 tff(49,plain,
% 0.94/1.16 ((~((~(pull = pull)) | (~(n1 = n1)))) <=> (~$false)),
% 0.94/1.16 inference(monotonicity,[status(thm)],[48])).
% 0.94/1.16 tff(50,plain,
% 0.94/1.16 ((~((~(pull = pull)) | (~(n1 = n1)))) <=> $true),
% 0.94/1.16 inference(transitivity,[status(thm)],[49, 38])).
% 0.94/1.16 tff(51,plain,
% 0.94/1.16 ((~(~(n1 = n2))) <=> (n1 = n2)),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(52,plain,
% 0.94/1.16 (((~(n1 = n2)) | $false) <=> (~(n1 = n2))),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(53,plain,
% 0.94/1.16 (((~(n1 = n2)) | (~(pull = pull))) <=> ((~(n1 = n2)) | $false)),
% 0.94/1.16 inference(monotonicity,[status(thm)],[46])).
% 0.94/1.16 tff(54,plain,
% 0.94/1.16 (((~(n1 = n2)) | (~(pull = pull))) <=> (~(n1 = n2))),
% 0.94/1.16 inference(transitivity,[status(thm)],[53, 52])).
% 0.94/1.16 tff(55,plain,
% 0.94/1.16 ((~((~(n1 = n2)) | (~(pull = pull)))) <=> (~(~(n1 = n2)))),
% 0.94/1.16 inference(monotonicity,[status(thm)],[54])).
% 0.94/1.16 tff(56,plain,
% 0.94/1.16 ((~((~(n1 = n2)) | (~(pull = pull)))) <=> (n1 = n2)),
% 0.94/1.16 inference(transitivity,[status(thm)],[55, 51])).
% 0.94/1.16 tff(57,plain,
% 0.94/1.16 ((~((~(pull = push)) | (~(n1 = n2)))) <=> (~((~(pull = push)) | (~(n1 = n2))))),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(58,plain,
% 0.94/1.16 (((~((~(pull = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(pull = pull)))) | (~((~(pull = pull)) | (~(n1 = n1)))) | (~((~(pull = push)) | (~(n1 = n0))))) <=> ((~((~(pull = push)) | (~(n1 = n2)))) | (n1 = n2) | $true | (~((~(pull = push)) | (~(n1 = n0)))))),
% 0.94/1.16 inference(monotonicity,[status(thm)],[57, 56, 50, 37])).
% 0.94/1.16 tff(59,plain,
% 0.94/1.16 (((~((~(pull = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(pull = pull)))) | (~((~(pull = pull)) | (~(n1 = n1)))) | (~((~(pull = push)) | (~(n1 = n0))))) <=> $true),
% 0.94/1.16 inference(transitivity,[status(thm)],[58, 36])).
% 0.94/1.16 tff(60,plain,
% 0.94/1.16 ((happens(pull, n1) <=> ((~((~(pull = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(pull = pull)))) | (~((~(pull = pull)) | (~(n1 = n1)))) | (~((~(pull = push)) | (~(n1 = n0)))))) <=> (happens(pull, n1) <=> $true)),
% 0.94/1.16 inference(monotonicity,[status(thm)],[59])).
% 0.94/1.16 tff(61,plain,
% 0.94/1.16 ((happens(pull, n1) <=> ((~((~(pull = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(pull = pull)))) | (~((~(pull = pull)) | (~(n1 = n1)))) | (~((~(pull = push)) | (~(n1 = n0)))))) <=> happens(pull, n1)),
% 0.94/1.16 inference(transitivity,[status(thm)],[60, 35])).
% 0.94/1.16 tff(62,plain,
% 0.94/1.16 (((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(pull, n1) <=> ((~((~(pull = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(pull = pull)))) | (~((~(pull = pull)) | (~(n1 = n1)))) | (~((~(pull = push)) | (~(n1 = n0))))))) <=> ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | happens(pull, n1))),
% 0.94/1.16 inference(monotonicity,[status(thm)],[61])).
% 0.94/1.16 tff(63,plain,
% 0.94/1.16 (((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(pull, n1) <=> ((~((~(pull = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(pull = pull)))) | (~((~(pull = pull)) | (~(n1 = n1)))) | (~((~(pull = push)) | (~(n1 = n0))))))) <=> ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | happens(pull, n1))),
% 0.94/1.16 inference(transitivity,[status(thm)],[62, 34])).
% 0.94/1.16 tff(64,plain,
% 0.94/1.16 ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(pull, n1) <=> ((~((~(pull = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(pull = pull)))) | (~((~(pull = pull)) | (~(n1 = n1)))) | (~((~(pull = push)) | (~(n1 = n0))))))),
% 0.94/1.16 inference(quant_inst,[status(thm)],[])).
% 0.94/1.16 tff(65,plain,
% 0.94/1.16 ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | happens(pull, n1)),
% 0.94/1.16 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.94/1.16 tff(66,plain,
% 0.94/1.16 (happens(pull, n1)),
% 0.94/1.16 inference(unit_resolution,[status(thm)],[65, 33])).
% 0.94/1.16 tff(67,plain,
% 0.94/1.16 ((plus(n1, n1) = n2) <=> (plus(n1, n1) = n2)),
% 0.94/1.16 inference(rewrite,[status(thm)],[])).
% 0.94/1.16 tff(68,axiom,(plus(n1, n1) = n2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','plus1_1')).
% 0.94/1.16 tff(69,plain,
% 0.94/1.16 (plus(n1, n1) = n2),
% 0.94/1.16 inference(modus_ponens,[status(thm)],[68, 67])).
% 0.94/1.16 tff(70,plain,
% 0.94/1.16 (holdsAt(backwards, plus(n1, n1)) <=> holdsAt(backwards, n2)),
% 0.94/1.16 inference(monotonicity,[status(thm)],[69])).
% 0.94/1.16 tff(71,plain,
% 0.94/1.16 (holdsAt(backwards, n2) <=> holdsAt(backwards, plus(n1, n1))),
% 0.94/1.16 inference(symmetry,[status(thm)],[70])).
% 0.94/1.16 tff(72,plain,
% 0.94/1.16 ((~holdsAt(backwards, n2)) <=> (~holdsAt(backwards, plus(n1, n1)))),
% 0.94/1.17 inference(monotonicity,[status(thm)],[71])).
% 0.94/1.17 tff(73,plain,
% 0.94/1.17 ((~holdsAt(backwards, n2)) <=> (~holdsAt(backwards, n2))),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(74,axiom,(~holdsAt(backwards, n2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','backwards_2')).
% 0.94/1.17 tff(75,plain,
% 0.94/1.17 (~holdsAt(backwards, n2)),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[74, 73])).
% 0.94/1.17 tff(76,plain,
% 0.94/1.17 (~holdsAt(backwards, plus(n1, n1))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[75, 72])).
% 0.94/1.17 tff(77,plain,
% 0.94/1.17 (^[Event: $i, Time: $i, Fluent: $i] : refl((holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time))) <=> (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time))))),
% 0.94/1.17 inference(bind,[status(th)],[])).
% 0.94/1.17 tff(78,plain,
% 0.94/1.17 (![Event: $i, Time: $i, Fluent: $i] : (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time))) <=> ![Event: $i, Time: $i, Fluent: $i] : (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))),
% 0.94/1.17 inference(quant_intro,[status(thm)],[77])).
% 0.94/1.17 tff(79,plain,
% 0.94/1.17 (^[Event: $i, Time: $i, Fluent: $i] : trans(monotonicity(trans(monotonicity(rewrite((happens(Event, Time) & initiates(Event, Fluent, Time)) <=> (~((~happens(Event, Time)) | (~initiates(Event, Fluent, Time))))), ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) <=> (~(~((~happens(Event, Time)) | (~initiates(Event, Fluent, Time))))))), rewrite((~(~((~happens(Event, Time)) | (~initiates(Event, Fluent, Time))))) <=> ((~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))), ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) <=> ((~happens(Event, Time)) | (~initiates(Event, Fluent, Time))))), (((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1))) <=> (((~happens(Event, Time)) | (~initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1))))), rewrite((((~happens(Event, Time)) | (~initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1))) <=> (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))), (((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1))) <=> (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))))),
% 0.94/1.17 inference(bind,[status(th)],[])).
% 0.94/1.17 tff(80,plain,
% 0.94/1.17 (![Event: $i, Time: $i, Fluent: $i] : ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1))) <=> ![Event: $i, Time: $i, Fluent: $i] : (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))),
% 0.94/1.17 inference(quant_intro,[status(thm)],[79])).
% 0.94/1.17 tff(81,plain,
% 0.94/1.17 (![Event: $i, Time: $i, Fluent: $i] : ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1))) <=> ![Event: $i, Time: $i, Fluent: $i] : ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1)))),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(82,plain,
% 0.94/1.17 (^[Event: $i, Time: $i, Fluent: $i] : rewrite(((happens(Event, Time) & initiates(Event, Fluent, Time)) => holdsAt(Fluent, plus(Time, n1))) <=> ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1))))),
% 0.94/1.17 inference(bind,[status(th)],[])).
% 0.94/1.17 tff(83,plain,
% 0.94/1.17 (![Event: $i, Time: $i, Fluent: $i] : ((happens(Event, Time) & initiates(Event, Fluent, Time)) => holdsAt(Fluent, plus(Time, n1))) <=> ![Event: $i, Time: $i, Fluent: $i] : ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1)))),
% 0.94/1.17 inference(quant_intro,[status(thm)],[82])).
% 0.94/1.17 tff(84,axiom,(![Event: $i, Time: $i, Fluent: $i] : ((happens(Event, Time) & initiates(Event, Fluent, Time)) => holdsAt(Fluent, plus(Time, n1)))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax','happens_holds')).
% 0.94/1.17 tff(85,plain,
% 0.94/1.17 (![Event: $i, Time: $i, Fluent: $i] : ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1)))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[84, 83])).
% 0.94/1.17 tff(86,plain,
% 0.94/1.17 (![Event: $i, Time: $i, Fluent: $i] : ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1)))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[85, 81])).
% 0.94/1.17 tff(87,plain,(
% 0.94/1.17 ![Event: $i, Time: $i, Fluent: $i] : ((~(happens(Event, Time) & initiates(Event, Fluent, Time))) | holdsAt(Fluent, plus(Time, n1)))),
% 0.94/1.17 inference(skolemize,[status(sab)],[86])).
% 0.94/1.17 tff(88,plain,
% 0.94/1.17 (![Event: $i, Time: $i, Fluent: $i] : (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[87, 80])).
% 0.94/1.17 tff(89,plain,
% 0.94/1.17 (![Event: $i, Time: $i, Fluent: $i] : (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[88, 78])).
% 0.94/1.17 tff(90,plain,
% 0.94/1.17 (((~![Event: $i, Time: $i, Fluent: $i] : (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))) | (holdsAt(backwards, plus(n1, n1)) | (~happens(pull, n1)) | (~initiates(pull, backwards, n1)))) <=> ((~![Event: $i, Time: $i, Fluent: $i] : (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))) | holdsAt(backwards, plus(n1, n1)) | (~happens(pull, n1)) | (~initiates(pull, backwards, n1)))),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(91,plain,
% 0.94/1.17 ((~![Event: $i, Time: $i, Fluent: $i] : (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))) | (holdsAt(backwards, plus(n1, n1)) | (~happens(pull, n1)) | (~initiates(pull, backwards, n1)))),
% 0.94/1.17 inference(quant_inst,[status(thm)],[])).
% 0.94/1.17 tff(92,plain,
% 0.94/1.17 ((~![Event: $i, Time: $i, Fluent: $i] : (holdsAt(Fluent, plus(Time, n1)) | (~happens(Event, Time)) | (~initiates(Event, Fluent, Time)))) | holdsAt(backwards, plus(n1, n1)) | (~happens(pull, n1)) | (~initiates(pull, backwards, n1))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[91, 90])).
% 0.94/1.17 tff(93,plain,
% 0.94/1.17 (~initiates(pull, backwards, n1)),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[92, 89, 76, 66])).
% 0.94/1.17 tff(94,plain,
% 0.94/1.17 ((~(initiates(pull, backwards, n1) <=> ((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1))))))) | initiates(pull, backwards, n1) | (~((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1))))))),
% 0.94/1.17 inference(tautology,[status(thm)],[])).
% 0.94/1.17 tff(95,plain,
% 0.94/1.17 (~((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1)))))),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[94, 93, 20])).
% 0.94/1.17 tff(96,plain,
% 0.94/1.17 (((~happens(push, n1)) | (~((~(pull = push)) | (~(backwards = forwards)) | happens(pull, n1))) | (~((~(backwards = spinning)) | (~happens(push, n1))))) | happens(push, n1)),
% 0.94/1.17 inference(tautology,[status(thm)],[])).
% 0.94/1.17 tff(97,plain,
% 0.94/1.17 (happens(push, n1)),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[96, 95])).
% 0.94/1.17 tff(98,assumption,(~(happens(push, n1) <=> ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull))))))), introduced(assumption)).
% 0.94/1.17 tff(99,plain,
% 0.94/1.17 (((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(push, n1) <=> ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull))))))) <=> ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(push, n1) <=> ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull)))))))),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(100,plain,
% 0.94/1.17 ((happens(push, n1) <=> ((~((~(push = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(push = pull)))) | (~((~(push = pull)) | (~(n1 = n1)))) | (~((~(push = push)) | (~(n1 = n0)))))) <=> (happens(push, n1) <=> ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull))))))),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(101,plain,
% 0.94/1.17 (((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(push, n1) <=> ((~((~(push = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(push = pull)))) | (~((~(push = pull)) | (~(n1 = n1)))) | (~((~(push = push)) | (~(n1 = n0))))))) <=> ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(push, n1) <=> ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull)))))))),
% 0.94/1.17 inference(monotonicity,[status(thm)],[100])).
% 0.94/1.17 tff(102,plain,
% 0.94/1.17 (((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(push, n1) <=> ((~((~(push = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(push = pull)))) | (~((~(push = pull)) | (~(n1 = n1)))) | (~((~(push = push)) | (~(n1 = n0))))))) <=> ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(push, n1) <=> ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull)))))))),
% 0.94/1.17 inference(transitivity,[status(thm)],[101, 99])).
% 0.94/1.17 tff(103,plain,
% 0.94/1.17 ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(push, n1) <=> ((~((~(push = push)) | (~(n1 = n2)))) | (~((~(n1 = n2)) | (~(push = pull)))) | (~((~(push = pull)) | (~(n1 = n1)))) | (~((~(push = push)) | (~(n1 = n0))))))),
% 0.94/1.17 inference(quant_inst,[status(thm)],[])).
% 0.94/1.17 tff(104,plain,
% 0.94/1.17 ((~![Event: $i, Time: $i] : (happens(Event, Time) <=> ((~((~(Event = push)) | (~(Time = n2)))) | (~((~(Time = n2)) | (~(Event = pull)))) | (~((~(Event = pull)) | (~(Time = n1)))) | (~((~(Event = push)) | (~(Time = n0))))))) | (happens(push, n1) <=> ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull))))))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.94/1.17 tff(105,plain,
% 0.94/1.17 ($false),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[104, 33, 98])).
% 0.94/1.17 tff(106,plain,(happens(push, n1) <=> ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull)))))), inference(lemma,lemma(discharge,[]))).
% 0.94/1.17 tff(107,plain,
% 0.94/1.17 ((~(happens(push, n1) <=> ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull))))))) | (~happens(push, n1)) | ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull)))))),
% 0.94/1.17 inference(tautology,[status(thm)],[])).
% 0.94/1.17 tff(108,plain,
% 0.94/1.17 ((~happens(push, n1)) | ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull)))))),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[107, 106])).
% 0.94/1.17 tff(109,plain,
% 0.94/1.17 ((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull))))),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[108, 97])).
% 0.94/1.17 tff(110,assumption,(n1 = n2), introduced(assumption)).
% 0.94/1.17 tff(111,plain,
% 0.94/1.17 (n2 = n1),
% 0.94/1.17 inference(symmetry,[status(thm)],[110])).
% 0.94/1.17 tff(112,plain,
% 0.94/1.17 (plus(n2, n2) = plus(n1, n1)),
% 0.94/1.17 inference(monotonicity,[status(thm)],[111, 111])).
% 0.94/1.17 tff(113,plain,
% 0.94/1.17 (plus(n1, n2) = plus(n2, n2)),
% 0.94/1.17 inference(monotonicity,[status(thm)],[110])).
% 0.94/1.17 tff(114,plain,
% 0.94/1.17 ((plus(n1, n2) = n3) <=> (plus(n1, n2) = n3)),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(115,axiom,(plus(n1, n2) = n3), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','plus1_2')).
% 0.94/1.17 tff(116,plain,
% 0.94/1.17 (plus(n1, n2) = n3),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[115, 114])).
% 0.94/1.17 tff(117,plain,
% 0.94/1.17 (n3 = plus(n1, n2)),
% 0.94/1.17 inference(symmetry,[status(thm)],[116])).
% 0.94/1.17 tff(118,plain,
% 0.94/1.17 (n3 = n2),
% 0.94/1.17 inference(transitivity,[status(thm)],[117, 113, 112, 69])).
% 0.94/1.17 tff(119,assumption,(~(less(n3, n4) <=> less_or_equal(n3, n3))), introduced(assumption)).
% 0.94/1.17 tff(120,plain,
% 0.94/1.17 (^[X: $i] : refl((less(X, n4) <=> less_or_equal(X, n3)) <=> (less(X, n4) <=> less_or_equal(X, n3)))),
% 0.94/1.17 inference(bind,[status(th)],[])).
% 0.94/1.17 tff(121,plain,
% 0.94/1.17 (![X: $i] : (less(X, n4) <=> less_or_equal(X, n3)) <=> ![X: $i] : (less(X, n4) <=> less_or_equal(X, n3))),
% 0.94/1.17 inference(quant_intro,[status(thm)],[120])).
% 0.94/1.17 tff(122,plain,
% 0.94/1.17 (![X: $i] : (less(X, n4) <=> less_or_equal(X, n3)) <=> ![X: $i] : (less(X, n4) <=> less_or_equal(X, n3))),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(123,axiom,(![X: $i] : (less(X, n4) <=> less_or_equal(X, n3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','less4')).
% 0.94/1.17 tff(124,plain,
% 0.94/1.17 (![X: $i] : (less(X, n4) <=> less_or_equal(X, n3))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[123, 122])).
% 0.94/1.17 tff(125,plain,(
% 0.94/1.17 ![X: $i] : (less(X, n4) <=> less_or_equal(X, n3))),
% 0.94/1.17 inference(skolemize,[status(sab)],[124])).
% 0.94/1.17 tff(126,plain,
% 0.94/1.17 (![X: $i] : (less(X, n4) <=> less_or_equal(X, n3))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[125, 121])).
% 0.94/1.17 tff(127,plain,
% 0.94/1.17 ((~![X: $i] : (less(X, n4) <=> less_or_equal(X, n3))) | (less(n3, n4) <=> less_or_equal(n3, n3))),
% 0.94/1.17 inference(quant_inst,[status(thm)],[])).
% 0.94/1.17 tff(128,plain,
% 0.94/1.17 ($false),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[127, 126, 119])).
% 0.94/1.17 tff(129,plain,(less(n3, n4) <=> less_or_equal(n3, n3)), inference(lemma,lemma(discharge,[]))).
% 0.94/1.17 tff(130,assumption,(less(n3, n4) <=> less_or_equal(n3, n3)), introduced(assumption)).
% 0.94/1.17 tff(131,plain,
% 0.94/1.17 (^[X: $i, Y: $i] : refl((less_or_equal(X, Y) <=> ((X = Y) | less(X, Y))) <=> (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y))))),
% 0.94/1.17 inference(bind,[status(th)],[])).
% 0.94/1.17 tff(132,plain,
% 0.94/1.17 (![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y))) <=> ![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))),
% 0.94/1.17 inference(quant_intro,[status(thm)],[131])).
% 0.94/1.17 tff(133,plain,
% 0.94/1.17 (![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y))) <=> ![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(134,plain,
% 0.94/1.17 (^[X: $i, Y: $i] : rewrite((less_or_equal(X, Y) <=> (less(X, Y) | (X = Y))) <=> (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y))))),
% 0.94/1.17 inference(bind,[status(th)],[])).
% 0.94/1.17 tff(135,plain,
% 0.94/1.17 (![X: $i, Y: $i] : (less_or_equal(X, Y) <=> (less(X, Y) | (X = Y))) <=> ![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))),
% 0.94/1.17 inference(quant_intro,[status(thm)],[134])).
% 0.94/1.17 tff(136,axiom,(![X: $i, Y: $i] : (less_or_equal(X, Y) <=> (less(X, Y) | (X = Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','less_or_equal')).
% 0.94/1.17 tff(137,plain,
% 0.94/1.17 (![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[136, 135])).
% 0.94/1.17 tff(138,plain,
% 0.94/1.17 (![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[137, 133])).
% 0.94/1.17 tff(139,plain,(
% 0.94/1.17 ![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))),
% 0.94/1.17 inference(skolemize,[status(sab)],[138])).
% 0.94/1.17 tff(140,plain,
% 0.94/1.17 (![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[139, 132])).
% 0.94/1.17 tff(141,plain,
% 0.94/1.17 (((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n3, n3)) <=> ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n3, n3))),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(142,plain,
% 0.94/1.17 ((less_or_equal(n3, n3) <=> $true) <=> less_or_equal(n3, n3)),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(143,plain,
% 0.94/1.17 (($true | less(n3, n3)) <=> $true),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(144,plain,
% 0.94/1.17 ((n3 = n3) <=> $true),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(145,plain,
% 0.94/1.17 (((n3 = n3) | less(n3, n3)) <=> ($true | less(n3, n3))),
% 0.94/1.17 inference(monotonicity,[status(thm)],[144])).
% 0.94/1.17 tff(146,plain,
% 0.94/1.17 (((n3 = n3) | less(n3, n3)) <=> $true),
% 0.94/1.17 inference(transitivity,[status(thm)],[145, 143])).
% 0.94/1.17 tff(147,plain,
% 0.94/1.17 ((less_or_equal(n3, n3) <=> ((n3 = n3) | less(n3, n3))) <=> (less_or_equal(n3, n3) <=> $true)),
% 0.94/1.17 inference(monotonicity,[status(thm)],[146])).
% 0.94/1.17 tff(148,plain,
% 0.94/1.17 ((less_or_equal(n3, n3) <=> ((n3 = n3) | less(n3, n3))) <=> less_or_equal(n3, n3)),
% 0.94/1.17 inference(transitivity,[status(thm)],[147, 142])).
% 0.94/1.17 tff(149,plain,
% 0.94/1.17 (((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | (less_or_equal(n3, n3) <=> ((n3 = n3) | less(n3, n3)))) <=> ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n3, n3))),
% 0.94/1.17 inference(monotonicity,[status(thm)],[148])).
% 0.94/1.17 tff(150,plain,
% 0.94/1.17 (((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | (less_or_equal(n3, n3) <=> ((n3 = n3) | less(n3, n3)))) <=> ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n3, n3))),
% 0.94/1.17 inference(transitivity,[status(thm)],[149, 141])).
% 0.94/1.17 tff(151,plain,
% 0.94/1.17 ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | (less_or_equal(n3, n3) <=> ((n3 = n3) | less(n3, n3)))),
% 0.94/1.17 inference(quant_inst,[status(thm)],[])).
% 0.94/1.17 tff(152,plain,
% 0.94/1.17 ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n3, n3)),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[151, 150])).
% 0.94/1.17 tff(153,plain,
% 0.94/1.17 (less_or_equal(n3, n3)),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[152, 140])).
% 0.94/1.17 tff(154,assumption,(~less(n3, n4)), introduced(assumption)).
% 0.94/1.17 tff(155,plain,
% 0.94/1.17 ((~(less(n3, n4) <=> less_or_equal(n3, n3))) | less(n3, n4) | (~less_or_equal(n3, n3))),
% 0.94/1.17 inference(tautology,[status(thm)],[])).
% 0.94/1.17 tff(156,plain,
% 0.94/1.17 ((~(less(n3, n4) <=> less_or_equal(n3, n3))) | (~less_or_equal(n3, n3))),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[155, 154])).
% 0.94/1.17 tff(157,plain,
% 0.94/1.17 ($false),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[156, 153, 130])).
% 0.94/1.17 tff(158,plain,((~(less(n3, n4) <=> less_or_equal(n3, n3))) | less(n3, n4)), inference(lemma,lemma(discharge,[]))).
% 0.94/1.17 tff(159,plain,
% 0.94/1.17 (less(n3, n4)),
% 0.94/1.17 inference(unit_resolution,[status(thm)],[158, 129])).
% 0.94/1.17 tff(160,assumption,(n3 = n2), introduced(assumption)).
% 0.94/1.17 tff(161,plain,
% 0.94/1.17 (plus(n1, n3) = plus(n1, n2)),
% 0.94/1.17 inference(monotonicity,[status(thm)],[160])).
% 0.94/1.17 tff(162,plain,
% 0.94/1.17 ((plus(n1, n3) = n4) <=> (plus(n1, n3) = n4)),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(163,axiom,(plus(n1, n3) = n4), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','plus1_3')).
% 0.94/1.17 tff(164,plain,
% 0.94/1.17 (plus(n1, n3) = n4),
% 0.94/1.17 inference(modus_ponens,[status(thm)],[163, 162])).
% 0.94/1.17 tff(165,plain,
% 0.94/1.17 (n4 = plus(n1, n3)),
% 0.94/1.17 inference(symmetry,[status(thm)],[164])).
% 0.94/1.17 tff(166,plain,
% 0.94/1.17 (n4 = n2),
% 0.94/1.17 inference(transitivity,[status(thm)],[165, 161, 116, 160])).
% 0.94/1.17 tff(167,plain,
% 0.94/1.17 (less(n3, n4) <=> less(n3, n2)),
% 0.94/1.17 inference(monotonicity,[status(thm)],[166])).
% 0.94/1.17 tff(168,plain,
% 0.94/1.17 (less(n3, n2) <=> less(n3, n4)),
% 0.94/1.17 inference(symmetry,[status(thm)],[167])).
% 0.94/1.17 tff(169,plain,
% 0.94/1.17 ((~less(n3, n2)) <=> (~less(n3, n4))),
% 0.94/1.17 inference(monotonicity,[status(thm)],[168])).
% 0.94/1.17 tff(170,plain,
% 0.94/1.17 (^[X: $i] : refl((less(X, n2) <=> less_or_equal(X, n1)) <=> (less(X, n2) <=> less_or_equal(X, n1)))),
% 0.94/1.17 inference(bind,[status(th)],[])).
% 0.94/1.17 tff(171,plain,
% 0.94/1.17 (![X: $i] : (less(X, n2) <=> less_or_equal(X, n1)) <=> ![X: $i] : (less(X, n2) <=> less_or_equal(X, n1))),
% 0.94/1.17 inference(quant_intro,[status(thm)],[170])).
% 0.94/1.17 tff(172,plain,
% 0.94/1.17 (![X: $i] : (less(X, n2) <=> less_or_equal(X, n1)) <=> ![X: $i] : (less(X, n2) <=> less_or_equal(X, n1))),
% 0.94/1.17 inference(rewrite,[status(thm)],[])).
% 0.94/1.17 tff(173,axiom,(![X: $i] : (less(X, n2) <=> less_or_equal(X, n1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','less2')).
% 0.94/1.17 tff(174,plain,
% 0.94/1.17 (![X: $i] : (less(X, n2) <=> less_or_equal(X, n1))),
% 0.94/1.18 inference(modus_ponens,[status(thm)],[173, 172])).
% 0.94/1.18 tff(175,plain,(
% 0.94/1.18 ![X: $i] : (less(X, n2) <=> less_or_equal(X, n1))),
% 0.94/1.18 inference(skolemize,[status(sab)],[174])).
% 0.94/1.18 tff(176,plain,
% 0.94/1.18 (![X: $i] : (less(X, n2) <=> less_or_equal(X, n1))),
% 0.94/1.18 inference(modus_ponens,[status(thm)],[175, 171])).
% 0.94/1.18 tff(177,plain,
% 0.94/1.18 ((~![X: $i] : (less(X, n2) <=> less_or_equal(X, n1))) | (less(n3, n2) <=> less_or_equal(n3, n1))),
% 0.94/1.18 inference(quant_inst,[status(thm)],[])).
% 0.94/1.18 tff(178,plain,
% 0.94/1.18 (less(n3, n2) <=> less_or_equal(n3, n1)),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[177, 176])).
% 0.94/1.18 tff(179,plain,
% 0.94/1.18 (less_or_equal(n3, n1) <=> less_or_equal(n2, n1)),
% 0.94/1.18 inference(monotonicity,[status(thm)],[160])).
% 0.94/1.18 tff(180,plain,
% 0.94/1.18 (less_or_equal(n2, n1) <=> less_or_equal(n3, n1)),
% 0.94/1.18 inference(symmetry,[status(thm)],[179])).
% 0.94/1.18 tff(181,plain,
% 0.94/1.18 ((~less_or_equal(n2, n1)) <=> (~less_or_equal(n3, n1))),
% 0.94/1.18 inference(monotonicity,[status(thm)],[180])).
% 0.94/1.18 tff(182,plain,
% 0.94/1.18 ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | (less_or_equal(n2, n1) <=> ((n2 = n1) | less(n2, n1)))),
% 0.94/1.18 inference(quant_inst,[status(thm)],[])).
% 0.94/1.18 tff(183,plain,
% 0.94/1.18 (less_or_equal(n2, n1) <=> ((n2 = n1) | less(n2, n1))),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[182, 140])).
% 0.94/1.18 tff(184,plain,
% 0.94/1.18 (^[X: $i, Y: $i] : refl((~(((Y = X) | less(Y, X)) <=> less(X, Y))) <=> (~(((Y = X) | less(Y, X)) <=> less(X, Y))))),
% 0.94/1.18 inference(bind,[status(th)],[])).
% 0.94/1.18 tff(185,plain,
% 0.94/1.18 (![X: $i, Y: $i] : (~(((Y = X) | less(Y, X)) <=> less(X, Y))) <=> ![X: $i, Y: $i] : (~(((Y = X) | less(Y, X)) <=> less(X, Y)))),
% 0.94/1.18 inference(quant_intro,[status(thm)],[184])).
% 0.94/1.18 tff(186,plain,
% 0.94/1.18 (^[X: $i, Y: $i] : trans(trans(monotonicity(rewrite(((~less(Y, X)) & (~(Y = X))) <=> (~((Y = X) | less(Y, X)))), ((less(X, Y) <=> ((~less(Y, X)) & (~(Y = X)))) <=> (less(X, Y) <=> (~((Y = X) | less(Y, X)))))), rewrite((less(X, Y) <=> (~((Y = X) | less(Y, X)))) <=> (~(((Y = X) | less(Y, X)) <=> less(X, Y)))), ((less(X, Y) <=> ((~less(Y, X)) & (~(Y = X)))) <=> (~(((Y = X) | less(Y, X)) <=> less(X, Y))))), rewrite((~(((Y = X) | less(Y, X)) <=> less(X, Y))) <=> (~(((Y = X) | less(Y, X)) <=> less(X, Y)))), ((less(X, Y) <=> ((~less(Y, X)) & (~(Y = X)))) <=> (~(((Y = X) | less(Y, X)) <=> less(X, Y)))))),
% 0.94/1.18 inference(bind,[status(th)],[])).
% 0.94/1.18 tff(187,plain,
% 0.94/1.18 (![X: $i, Y: $i] : (less(X, Y) <=> ((~less(Y, X)) & (~(Y = X)))) <=> ![X: $i, Y: $i] : (~(((Y = X) | less(Y, X)) <=> less(X, Y)))),
% 0.94/1.18 inference(quant_intro,[status(thm)],[186])).
% 0.94/1.18 tff(188,plain,
% 0.94/1.18 (![X: $i, Y: $i] : (less(X, Y) <=> ((~less(Y, X)) & (~(Y = X)))) <=> ![X: $i, Y: $i] : (less(X, Y) <=> ((~less(Y, X)) & (~(Y = X))))),
% 0.94/1.18 inference(rewrite,[status(thm)],[])).
% 0.94/1.18 tff(189,axiom,(![X: $i, Y: $i] : (less(X, Y) <=> ((~less(Y, X)) & (~(Y = X))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','less_property')).
% 0.94/1.18 tff(190,plain,
% 0.94/1.18 (![X: $i, Y: $i] : (less(X, Y) <=> ((~less(Y, X)) & (~(Y = X))))),
% 0.94/1.18 inference(modus_ponens,[status(thm)],[189, 188])).
% 0.94/1.18 tff(191,plain,(
% 0.94/1.18 ![X: $i, Y: $i] : (less(X, Y) <=> ((~less(Y, X)) & (~(Y = X))))),
% 0.94/1.18 inference(skolemize,[status(sab)],[190])).
% 0.94/1.18 tff(192,plain,
% 0.94/1.18 (![X: $i, Y: $i] : (~(((Y = X) | less(Y, X)) <=> less(X, Y)))),
% 0.94/1.18 inference(modus_ponens,[status(thm)],[191, 187])).
% 0.94/1.18 tff(193,plain,
% 0.94/1.18 (![X: $i, Y: $i] : (~(((Y = X) | less(Y, X)) <=> less(X, Y)))),
% 0.94/1.18 inference(modus_ponens,[status(thm)],[192, 185])).
% 0.94/1.18 tff(194,plain,
% 0.94/1.18 ((~![X: $i, Y: $i] : (~(((Y = X) | less(Y, X)) <=> less(X, Y)))) | (~(((n2 = n1) | less(n2, n1)) <=> less(n1, n2)))),
% 0.94/1.18 inference(quant_inst,[status(thm)],[])).
% 0.94/1.18 tff(195,plain,
% 0.94/1.18 (~(((n2 = n1) | less(n2, n1)) <=> less(n1, n2))),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[194, 193])).
% 0.94/1.18 tff(196,plain,
% 0.94/1.18 ((~![X: $i] : (less(X, n2) <=> less_or_equal(X, n1))) | (less(n1, n2) <=> less_or_equal(n1, n1))),
% 0.94/1.18 inference(quant_inst,[status(thm)],[])).
% 0.94/1.18 tff(197,plain,
% 0.94/1.18 (less(n1, n2) <=> less_or_equal(n1, n1)),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[196, 176])).
% 0.94/1.18 tff(198,plain,
% 0.94/1.18 (((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n1, n1)) <=> ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n1, n1))),
% 0.94/1.18 inference(rewrite,[status(thm)],[])).
% 0.94/1.18 tff(199,plain,
% 0.94/1.18 ((less_or_equal(n1, n1) <=> $true) <=> less_or_equal(n1, n1)),
% 0.94/1.18 inference(rewrite,[status(thm)],[])).
% 0.94/1.18 tff(200,plain,
% 0.94/1.18 (($true | less(n1, n1)) <=> $true),
% 0.94/1.18 inference(rewrite,[status(thm)],[])).
% 0.94/1.18 tff(201,plain,
% 0.94/1.18 (((n1 = n1) | less(n1, n1)) <=> ($true | less(n1, n1))),
% 0.94/1.18 inference(monotonicity,[status(thm)],[41])).
% 0.94/1.18 tff(202,plain,
% 0.94/1.18 (((n1 = n1) | less(n1, n1)) <=> $true),
% 0.94/1.18 inference(transitivity,[status(thm)],[201, 200])).
% 0.94/1.18 tff(203,plain,
% 0.94/1.18 ((less_or_equal(n1, n1) <=> ((n1 = n1) | less(n1, n1))) <=> (less_or_equal(n1, n1) <=> $true)),
% 0.94/1.18 inference(monotonicity,[status(thm)],[202])).
% 0.94/1.18 tff(204,plain,
% 0.94/1.18 ((less_or_equal(n1, n1) <=> ((n1 = n1) | less(n1, n1))) <=> less_or_equal(n1, n1)),
% 0.94/1.18 inference(transitivity,[status(thm)],[203, 199])).
% 0.94/1.18 tff(205,plain,
% 0.94/1.18 (((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | (less_or_equal(n1, n1) <=> ((n1 = n1) | less(n1, n1)))) <=> ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n1, n1))),
% 0.94/1.18 inference(monotonicity,[status(thm)],[204])).
% 0.94/1.18 tff(206,plain,
% 0.94/1.18 (((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | (less_or_equal(n1, n1) <=> ((n1 = n1) | less(n1, n1)))) <=> ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n1, n1))),
% 0.94/1.18 inference(transitivity,[status(thm)],[205, 198])).
% 0.94/1.18 tff(207,plain,
% 0.94/1.18 ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | (less_or_equal(n1, n1) <=> ((n1 = n1) | less(n1, n1)))),
% 0.94/1.18 inference(quant_inst,[status(thm)],[])).
% 0.94/1.18 tff(208,plain,
% 0.94/1.18 ((~![X: $i, Y: $i] : (less_or_equal(X, Y) <=> ((X = Y) | less(X, Y)))) | less_or_equal(n1, n1)),
% 0.94/1.18 inference(modus_ponens,[status(thm)],[207, 206])).
% 0.94/1.18 tff(209,plain,
% 0.94/1.18 (less_or_equal(n1, n1)),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[208, 140])).
% 0.94/1.18 tff(210,plain,
% 0.94/1.18 ((~(less(n1, n2) <=> less_or_equal(n1, n1))) | less(n1, n2) | (~less_or_equal(n1, n1))),
% 0.94/1.18 inference(tautology,[status(thm)],[])).
% 0.94/1.18 tff(211,plain,
% 0.94/1.18 ((~(less(n1, n2) <=> less_or_equal(n1, n1))) | less(n1, n2)),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[210, 209])).
% 0.94/1.18 tff(212,plain,
% 0.94/1.18 (less(n1, n2)),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[211, 197])).
% 0.94/1.18 tff(213,plain,
% 0.94/1.18 ((((n2 = n1) | less(n2, n1)) <=> less(n1, n2)) | (~((n2 = n1) | less(n2, n1))) | (~less(n1, n2))),
% 0.94/1.18 inference(tautology,[status(thm)],[])).
% 0.94/1.18 tff(214,plain,
% 0.94/1.18 (~((n2 = n1) | less(n2, n1))),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[213, 212, 195])).
% 0.94/1.18 tff(215,plain,
% 0.94/1.18 ((~(less_or_equal(n2, n1) <=> ((n2 = n1) | less(n2, n1)))) | (~less_or_equal(n2, n1)) | ((n2 = n1) | less(n2, n1))),
% 0.94/1.18 inference(tautology,[status(thm)],[])).
% 0.94/1.18 tff(216,plain,
% 0.94/1.18 (~less_or_equal(n2, n1)),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[215, 214, 183])).
% 0.94/1.18 tff(217,plain,
% 0.94/1.18 (~less_or_equal(n3, n1)),
% 0.94/1.18 inference(modus_ponens,[status(thm)],[216, 181])).
% 0.94/1.18 tff(218,plain,
% 0.94/1.18 ((~(less(n3, n2) <=> less_or_equal(n3, n1))) | (~less(n3, n2)) | less_or_equal(n3, n1)),
% 0.94/1.18 inference(tautology,[status(thm)],[])).
% 0.94/1.18 tff(219,plain,
% 0.94/1.18 (~less(n3, n2)),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[218, 217, 178])).
% 0.94/1.18 tff(220,plain,
% 0.94/1.18 (~less(n3, n4)),
% 0.94/1.18 inference(modus_ponens,[status(thm)],[219, 169])).
% 0.94/1.18 tff(221,assumption,(less(n3, n4)), introduced(assumption)).
% 0.94/1.18 tff(222,plain,
% 0.94/1.18 ($false),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[221, 220])).
% 0.94/1.18 tff(223,plain,((~less(n3, n4)) | (~(n3 = n2))), inference(lemma,lemma(discharge,[]))).
% 0.94/1.18 tff(224,plain,
% 0.94/1.18 (~(n3 = n2)),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[223, 159])).
% 0.94/1.18 tff(225,plain,
% 0.94/1.18 ($false),
% 0.94/1.18 inference(unit_resolution,[status(thm)],[224, 118])).
% 0.94/1.18 tff(226,plain,(~(n1 = n2)), inference(lemma,lemma(discharge,[]))).
% 0.94/1.18 tff(227,plain,
% 0.94/1.18 ((~(push = pull)) <=> (~(push = pull))),
% 0.94/1.18 inference(rewrite,[status(thm)],[])).
% 0.94/1.18 tff(228,axiom,(~(push = pull)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+2.ax','push_not_pull')).
% 1.02/1.18 tff(229,plain,
% 1.02/1.18 (~(push = pull)),
% 1.02/1.18 inference(modus_ponens,[status(thm)],[228, 227])).
% 1.02/1.18 tff(230,plain,
% 1.02/1.18 (((~(n1 = n2)) | (~(push = pull))) | (push = pull)),
% 1.02/1.18 inference(tautology,[status(thm)],[])).
% 1.02/1.18 tff(231,plain,
% 1.02/1.18 ((~(n1 = n2)) | (~(push = pull))),
% 1.02/1.18 inference(unit_resolution,[status(thm)],[230, 229])).
% 1.02/1.18 tff(232,plain,
% 1.02/1.18 ((~((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull)))))) | (push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull))))),
% 1.02/1.18 inference(tautology,[status(thm)],[])).
% 1.02/1.18 tff(233,plain,
% 1.02/1.18 ((~((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull)))))) | (n1 = n2) | (n1 = n0)),
% 1.02/1.18 inference(unit_resolution,[status(thm)],[232, 229, 231])).
% 1.02/1.18 tff(234,plain,
% 1.02/1.18 ((~((push = pull) | (n1 = n2) | (n1 = n0) | (~((~(n1 = n2)) | (~(push = pull)))))) | (n1 = n0)),
% 1.02/1.18 inference(unit_resolution,[status(thm)],[233, 226])).
% 1.02/1.18 tff(235,plain,
% 1.02/1.18 (n1 = n0),
% 1.02/1.18 inference(unit_resolution,[status(thm)],[234, 109])).
% 1.02/1.18 tff(236,plain,
% 1.02/1.18 (n0 = n1),
% 1.02/1.18 inference(symmetry,[status(thm)],[235])).
% 1.02/1.18 tff(237,plain,
% 1.02/1.18 ((plus(n0, n0) = n0) <=> (plus(n0, n0) = n0)),
% 1.02/1.18 inference(rewrite,[status(thm)],[])).
% 1.02/1.18 tff(238,axiom,(plus(n0, n0) = n0), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','plus0_0')).
% 1.02/1.18 tff(239,plain,
% 1.02/1.18 (plus(n0, n0) = n0),
% 1.02/1.18 inference(modus_ponens,[status(thm)],[238, 237])).
% 1.02/1.18 tff(240,plain,
% 1.02/1.18 (plus(n0, n0) = plus(n1, n1)),
% 1.02/1.18 inference(monotonicity,[status(thm)],[236, 236])).
% 1.02/1.18 tff(241,plain,
% 1.02/1.18 (plus(n1, n1) = plus(n0, n0)),
% 1.02/1.18 inference(symmetry,[status(thm)],[240])).
% 1.02/1.18 tff(242,plain,
% 1.02/1.18 (n2 = plus(n1, n1)),
% 1.02/1.18 inference(symmetry,[status(thm)],[69])).
% 1.02/1.18 tff(243,plain,
% 1.02/1.18 (n2 = n1),
% 1.02/1.18 inference(transitivity,[status(thm)],[242, 241, 239, 236])).
% 1.02/1.18 tff(244,plain,
% 1.02/1.18 ((n1 = n2) <=> (n2 = n1)),
% 1.02/1.18 inference(commutativity,[status(thm)],[])).
% 1.02/1.18 tff(245,plain,
% 1.02/1.18 ((~(n1 = n2)) <=> (~(n2 = n1))),
% 1.02/1.18 inference(monotonicity,[status(thm)],[244])).
% 1.02/1.18 tff(246,plain,
% 1.02/1.18 (~(n2 = n1)),
% 1.02/1.18 inference(modus_ponens,[status(thm)],[226, 245])).
% 1.02/1.18 tff(247,plain,
% 1.02/1.18 ($false),
% 1.02/1.18 inference(unit_resolution,[status(thm)],[246, 243])).
% 1.02/1.18 % SZS output end Proof
% 1.03/1.18 % E exiting
%------------------------------------------------------------------------------