%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWV436^4 : TPTP v9.3.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:39:53 AM UTC 2026
% Result : Theorem 84.90s 18.36s
% Output : Refutation 73.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV436^4 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n016.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 16:08:49 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.04/0.86 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.88/1.24 % [INFO] Parsing done (382ms).
% 1.88/1.26 % [INFO] Running in sequential loop mode.
% 2.88/1.73 % [INFO] eprover registered as external prover.
% 2.88/1.74 % [INFO] Scanning for conjecture ...
% 3.30/1.94 % [INFO] Found a conjecture (or negated_conjecture) and 5 axioms. Running axiom selection ...
% 3.30/1.98 % [INFO] Axiom selection finished. Selected 5 axioms (removed 0 axioms).
% 3.30/1.99 % [INFO] Problem is higher-order (TPTP THF).
% 3.30/2.00 % [INFO] Type checking passed.
% 3.30/2.01 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 84.90/18.35 % External prover 'e' found a proof!
% 84.90/18.35 % [INFO] Killing All external provers ...
% 84.90/18.35 % Time passed: 17987ms (effective reasoning time: 17078ms)
% 84.90/18.35 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 84.90/18.35 % Axioms used in derivation (5): trans_axiom, ax1, ax2, refl_axiom, ax3
% 84.90/18.36 % No. of inferences in proof: 249
% 84.90/18.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 17987 ms resp. 17078 ms w/o parsing
% 73.89/18.61 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 73.89/18.61 thf(individuals_type, type, individuals: $tType).
% 73.89/18.61 thf(prop_a_decl, type, prop_a: ($i > $o)).
% 73.89/18.61 thf(prop_b_decl, type, prop_b: ($i > $o)).
% 73.89/18.61 thf(prop_c_decl, type, prop_c: ($i > $o)).
% 73.89/18.61 thf(mfalse_decl, type, mfalse: ($i > $o)).
% 73.89/18.61 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 73.89/18.61 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 73.89/18.61 thf(mimpl_decl, type, mimpl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 73.89/18.61 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 73.89/18.61 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 73.89/18.61 thf(rel_decl, type, rel: ($i > ($i > $o))).
% 73.89/18.61 thf(icl_atom_decl, type, icl_atom: (($i > $o) > ($i > $o))).
% 73.89/18.61 thf(icl_princ_decl, type, icl_princ: (($i > $o) > ($i > $o))).
% 73.89/18.61 thf(icl_impl_decl, type, icl_impl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 73.89/18.61 thf(icl_false_decl, type, icl_false: ($i > $o)).
% 73.89/18.61 thf(icl_says_decl, type, icl_says: (($i > $o) > (($i > $o) > ($i > $o)))).
% 73.89/18.61 thf(iclval_decl, type, iclval: (($i > $o) > $o)).
% 73.89/18.61 thf(admin_decl, type, admin: ($i > $o)).
% 73.89/18.61 thf(bob_decl, type, bob: ($i > $o)).
% 73.89/18.61 thf(deletefile1_decl, type, deletefile1: ($i > $o)).
% 73.89/18.61 thf(sk1_decl, type, sk1: $i).
% 73.89/18.61 thf(sk2_decl, type, sk2: $i).
% 73.89/18.61 thf(sk3_decl, type, sk3: ($i > (($i > $o) > $i))).
% 73.89/18.61 thf(sk4_decl, type, sk4: ($i > (($i > $o) > $i))).
% 73.89/18.61 thf(mfalse_def, definition, mfalse = (^ [A:$i]: (($false))) ).
% 73.89/18.61 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 73.89/18.61 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 73.89/18.61 thf(mimpl_def, definition, mimpl = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 73.89/18.61 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: ((A @ C @ D) => (B @ D))) ).
% 73.89/18.61 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 73.89/18.61 thf(icl_atom_def, definition, icl_atom = (mbox @ rel) ).
% 73.89/18.61 thf(icl_princ_def, definition, icl_princ = (^ [A:($i > $o)]: (A)) ).
% 73.89/18.61 thf(icl_impl_def, definition, icl_impl = (^ [A:($i > $o),B:($i > $o)]: (mbox @ rel @ (mimpl @ A @ B))) ).
% 73.89/18.61 thf(icl_false_def, definition, icl_false = (mfalse) ).
% 73.89/18.61 thf(icl_says_def, definition, icl_says = (^ [A:($i > $o),B:($i > $o)]: (mbox @ rel @ (mor @ A @ B))) ).
% 73.89/18.61 thf(iclval_def, definition, iclval = (mvalid) ).
% 73.89/18.61 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:$i]: ((rel @ A @ B) => (deletefile1 @ B)))) ).
% 73.89/18.61 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ ((rel @ sk1 @ A) => (deletefile1 @ A))) ).
% 73.89/18.61 thf(sk3_def, definition, sk3 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((rel @ A @ C) => (B @ C)))) ).
% 73.89/18.61 thf(sk4_def, definition, sk4 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((rel @ A @ C) => (B @ C)))) ).
% 73.89/18.61 thf(3,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ rel @ A) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',refl_axiom)).
% 73.89/18.61 thf(12,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((rel @ B @ C) => (A @ C))) | (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 73.89/18.61 thf(13,plain,(! [B:$i,A:($i > $o)] : ((((rel @ B @ (sk3 @ B @ (A))) | (A @ B)) & (~ (A @ (sk3 @ B @ (A))) | (A @ B))))),inference(cnf,[status(esa)],[12])).
% 73.89/18.61 thf(14,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | (A @ B))),inference(cnfConj,[status(thm)],[13])).
% 73.89/18.61 thf(1,conjecture,((iclval @ (icl_atom @ deletefile1))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ex3)).
% 73.89/18.61 thf(2,negated_conjecture,((~ (iclval @ (icl_atom @ deletefile1)))),inference(neg_conjecture,[status(cth)],[1])).
% 73.89/18.61 thf(8,plain,((~ (! [A:$i,B:$i]: ((rel @ A @ B) => (deletefile1 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 73.89/18.61 thf(9,plain,(((rel @ sk1 @ sk2) & ~ (deletefile1 @ sk2))),inference(cnf,[status(esa)],[8])).
% 73.89/18.61 thf(10,plain,((rel @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[9])).
% 73.89/18.61 thf(5,axiom,((iclval @ (icl_says @ (icl_impl @ (icl_princ @ admin) @ icl_false) @ (icl_atom @ deletefile1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1)).
% 73.89/18.61 thf(24,plain,((! [A:$i,B:$i]: ((rel @ A @ B) => (! [C:$i]: ((rel @ B @ C) => (~ (admin @ C))) | ! [C:$i]: ((rel @ B @ C) => (deletefile1 @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 73.89/18.61 thf(25,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (~ (admin @ C)) | (~ (rel @ B @ D)) | (deletefile1 @ D))),inference(cnf,[status(esa)],[24])).
% 73.89/18.61 thf(78,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (~ (admin @ C)) | ~ (($true)) | (deletefile1 @ D) | ((rel @ sk1 @ sk2) != (rel @ B @ D)))),inference(paramod_ordered,[status(thm)],[10,25])).
% 73.89/18.61 thf(79,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (~ (admin @ C)) | (deletefile1 @ D) | ((rel @ sk1 @ sk2) != (rel @ B @ D)))),inference(simp,[status(thm)],[78])).
% 73.89/18.61 thf(80,plain,(! [B:$i,A:$i] : ((~ (rel @ A @ sk1)) | (~ (rel @ sk1 @ B)) | (~ (admin @ B)) | (deletefile1 @ sk2))),inference(pattern_uni,[status(thm)],[79:[bind(A, $thf(A)),bind(B, $thf(sk1)),bind(C, $thf(C)),bind(D, $thf(sk2))]])).
% 73.89/18.61 thf(87,plain,(! [B:$i,A:$i] : ((~ (rel @ A @ sk1)) | (~ (rel @ sk1 @ B)) | (~ (admin @ B)) | (deletefile1 @ sk2))),inference(simp,[status(thm)],[80])).
% 73.89/18.61 thf(11,plain,((~ (deletefile1 @ sk2))),inference(cnfConj,[status(thm)],[9])).
% 73.89/18.61 thf(93,plain,(! [B:$i,A:$i] : ((~ (rel @ A @ sk1)) | (~ (rel @ sk1 @ B)) | (~ (admin @ B)) | ($false))),inference(rewrite,[status(thm)],[87,11])).
% 73.89/18.61 thf(94,plain,(! [B:$i,A:$i] : ((~ (rel @ A @ sk1)) | (~ (rel @ sk1 @ B)) | (~ (admin @ B)))),inference(simp,[status(thm)],[93])).
% 73.89/18.61 thf(100,plain,(! [B:$i,A:$i] : ((~ (rel @ A @ sk1)) | (~ (admin @ B)) | ((rel @ sk1 @ B) != (rel @ A @ sk1)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[94])).
% 73.89/18.61 thf(102,plain,((~ (rel @ sk1 @ sk1)) | (~ (admin @ sk1))),inference(pattern_uni,[status(thm)],[100:[bind(A, $thf(sk1)),bind(B, $thf(sk1))]])).
% 73.89/18.61 thf(220,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ~ (($true)) | (~ (admin @ sk1)) | ((A @ B) != (rel @ sk1 @ sk1)))),inference(paramod_ordered,[status(thm)],[14,102])).
% 73.89/18.61 thf(221,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | (~ (admin @ sk1)) | ((A @ B) != (rel @ sk1 @ sk1)))),inference(simp,[status(thm)],[220])).
% 73.89/18.61 thf(228,plain,((rel @ sk1 @ (sk3 @ sk1 @ (rel @ sk1))) | (~ (admin @ sk1))),inference(pre_uni,[status(thm)],[221:[bind(A, $thf(rel @ sk1)),bind(B, $thf(sk1))]])).
% 73.89/18.61 thf(15,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk3 @ B @ (A)))) | (A @ B))),inference(cnfConj,[status(thm)],[13])).
% 73.89/18.61 thf(1355,plain,(! [B:$i,A:($i > $o)] : ((~ (admin @ sk1)) | ~ (($true)) | (A @ B) | ((rel @ sk1 @ (sk3 @ sk1 @ (rel @ sk1))) != (A @ (sk3 @ B @ (A)))))),inference(paramod_ordered,[status(thm)],[228,15])).
% 73.89/18.61 thf(1356,plain,(! [B:$i,A:($i > $o)] : ((~ (admin @ sk1)) | (A @ B) | ((rel @ sk1 @ (sk3 @ sk1 @ (rel @ sk1))) != (A @ (sk3 @ B @ (A)))))),inference(simp,[status(thm)],[1355])).
% 73.89/18.61 thf(1394,plain,((~ (admin @ sk1)) | (rel @ sk1 @ sk1)),inference(pre_uni,[status(thm)],[1356:[bind(A, $thf(rel @ sk1)),bind(B, $thf(sk1))]])).
% 73.89/18.61 thf(1422,plain,((~ (admin @ sk1)) | ~ (($true)) | (~ (admin @ sk1)) | ((rel @ sk1 @ sk1) != (rel @ sk1 @ sk1))),inference(paramod_ordered,[status(thm)],[1394,102])).
% 73.89/18.61 thf(1423,plain,((~ (admin @ sk1)) | ((rel @ sk1 @ sk1) != (rel @ sk1 @ sk1))),inference(simp,[status(thm)],[1422])).
% 73.89/18.61 thf(1424,plain,((~ (admin @ sk1))),inference(pattern_uni,[status(thm)],[1423:[]])).
% 73.89/18.61 thf(1484,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ~ (($true)) | ((A @ B) != (admin @ sk1)))),inference(paramod_ordered,[status(thm)],[14,1424])).
% 73.89/18.61 thf(1485,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ((A @ B) != (admin @ sk1)))),inference(simp,[status(thm)],[1484])).
% 73.89/18.61 thf(1491,plain,((rel @ sk1 @ (sk3 @ sk1 @ (admin)))),inference(pre_uni,[status(thm)],[1485:[bind(A, $thf(admin)),bind(B, $thf(sk1))]])).
% 73.89/18.61 thf(37,plain,(! [B:($i > $o),A:$i] : ((~ (~ (B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))))) | (~ (B @ A)))),inference(prim_subst,[status(thm)],[15:[bind(A, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 73.89/18.61 thf(56,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | (~ (B @ A)))),inference(cnf,[status(esa)],[37])).
% 73.89/18.61 thf(57,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | (~ (B @ A)))),inference(simp,[status(thm)],[56])).
% 73.89/18.61 thf(3688,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((rel @ sk1 @ (sk3 @ sk1 @ (admin))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[1491,57])).
% 73.89/18.61 thf(3689,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((rel @ sk1 @ (sk3 @ sk1 @ (admin))) != (B @ A)))),inference(simp,[status(thm)],[3688])).
% 73.89/18.61 thf(3830,plain,((rel @ (sk3 @ sk1 @ (^ [A:$i]: ~ (rel @ A @ (sk3 @ sk1 @ admin)))) @ (sk3 @ sk1 @ (admin)))),inference(pre_uni,[status(thm)],[3689:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (rel @ C @ (sk3 @ sk1 @ admin))))]])).
% 73.89/18.61 thf(157,plain,(! [A:$i] : ((rel @ A @ (sk3 @ A @ (^ [B:$i]: (($false))))) | ($false))),inference(prim_subst,[status(thm)],[14:[bind(A, $thf(^ [C:$i]: (($false))))]])).
% 73.89/18.61 thf(196,plain,(! [A:$i] : ((rel @ A @ (sk3 @ A @ (^ [B:$i]: (($false))))))),inference(simp,[status(thm)],[157])).
% 73.89/18.61 thf(282,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel @ B @ sk1)) | ~ (($true)) | (~ (admin @ C)) | ((rel @ A @ (sk3 @ A @ (^ [D:$i]: (($false))))) != (rel @ sk1 @ C)))),inference(paramod_ordered,[status(thm)],[196,94])).
% 73.89/18.61 thf(283,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel @ B @ sk1)) | (~ (admin @ C)) | ((rel @ A @ (sk3 @ A @ (^ [D:$i]: (($false))))) != (rel @ sk1 @ C)))),inference(simp,[status(thm)],[282])).
% 73.89/18.61 thf(284,plain,(! [A:$i] : ((~ (rel @ A @ sk1)) | (~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))))),inference(pattern_uni,[status(thm)],[283:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(sk3 @ sk1 @ (^ [D:$i]: (($false)))))]])).
% 73.89/18.61 thf(299,plain,(! [A:$i] : ((~ (rel @ A @ sk1)) | (~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))))),inference(simp,[status(thm)],[284])).
% 73.89/18.61 thf(1753,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk1 @ sk2) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[10,299])).
% 73.89/18.61 thf(1754,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk1 @ sk2) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[1753])).
% 73.89/18.61 thf(1814,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | (sk1 != A) | (sk2 != sk1))),inference(simp,[status(thm)],[1754])).
% 73.89/18.61 thf(1837,plain,((~ (admin @ (sk3 @ sk1 @ (^ [A:$i]: (($false)))))) | (sk2 != sk1)),inference(simp,[status(thm)],[1814])).
% 73.89/18.61 thf(16,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk3 @ B @ (A)) = (sk3 @ B @ ((=) @ $i @ (sk3 @ B @ A))))) | ((sk3 @ B @ (A)) = B))),inference(replace_leibeq,[status(thm)],[15:[bind(A, $thf((=) @ $i @ (sk3 @ B @ A)))]])).
% 73.89/18.61 thf(17,plain,(! [B:$i,A:($i > $o)] : (((sk3 @ B @ (A)) != (sk3 @ B @ ((=) @ $i @ (sk3 @ B @ A)))) | ((sk3 @ B @ (A)) = B))),inference(lifteq,[status(thm)],[16])).
% 73.89/18.61 thf(7,axiom,((iclval @ (icl_says @ (icl_princ @ bob) @ (icl_atom @ deletefile1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3)).
% 73.89/18.61 thf(28,plain,((! [A:$i,B:$i]: ((rel @ A @ B) => ((bob @ B) | ! [C:$i]: ((rel @ B @ C) => (deletefile1 @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 73.89/18.61 thf(29,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel @ A @ B)) | (bob @ B) | (~ (rel @ B @ C)) | (deletefile1 @ C))),inference(cnf,[status(esa)],[28])).
% 73.89/18.61 thf(2244,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel @ A @ B)) | (bob @ B) | ~ (($true)) | (deletefile1 @ C) | ((rel @ sk1 @ sk2) != (rel @ B @ C)))),inference(paramod_ordered,[status(thm)],[10,29])).
% 73.89/18.61 thf(2245,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel @ A @ B)) | (bob @ B) | (deletefile1 @ C) | ((rel @ sk1 @ sk2) != (rel @ B @ C)))),inference(simp,[status(thm)],[2244])).
% 73.89/18.61 thf(2246,plain,(! [A:$i] : ((~ (rel @ A @ sk1)) | (bob @ sk1) | (deletefile1 @ sk2))),inference(pattern_uni,[status(thm)],[2245:[bind(A, $thf(A)),bind(B, $thf(sk1)),bind(C, $thf(sk2))]])).
% 73.89/18.61 thf(2500,plain,(! [A:$i] : ((~ (rel @ A @ sk1)) | (bob @ sk1) | ($false))),inference(rewrite,[status(thm)],[2246,11])).
% 73.89/18.61 thf(2501,plain,(! [A:$i] : ((~ (rel @ A @ sk1)) | (bob @ sk1))),inference(simp,[status(thm)],[2500])).
% 73.89/18.61 thf(2508,plain,(! [C:$i,B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ~ (($true)) | (bob @ sk1) | ((A @ B) != (rel @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[14,2501])).
% 73.89/18.61 thf(2509,plain,(! [C:$i,B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | (bob @ sk1) | ((A @ B) != (rel @ C @ sk1)))),inference(simp,[status(thm)],[2508])).
% 73.89/18.61 thf(2538,plain,(! [A:($i > $i)] : ((rel @ sk1 @ (sk3 @ sk1 @ (^ [B:$i]: (rel @ (A @ B) @ B)))) | (bob @ sk1))),inference(pre_uni,[status(thm)],[2509:[bind(A, $thf(^ [E:$i]: (rel @ (D @ E) @ E))),bind(B, $thf(sk1)),bind(C, $thf(D @ sk1))]])).
% 73.89/18.61 thf(2552,plain,(! [A:($i > $i)] : ((rel @ sk1 @ (sk3 @ sk1 @ (^ [B:$i]: (rel @ (A @ B) @ B)))) | (bob @ sk1))),inference(simp,[status(thm)],[2538])).
% 73.89/18.61 thf(32,plain,(! [B:$i,A:($i > $o)] : ((A @ B) | ((A @ (sk3 @ B @ (A))) != (~ (A @ B))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[15])).
% 73.89/18.61 thf(51,plain,(! [B:$i,A:($i > $o)] : ((A @ B) | ((A @ (sk3 @ B @ (A))) != (~ (A @ B))))),inference(simp,[status(thm)],[32])).
% 73.89/18.61 thf(2820,plain,(! [C:$i,B:($i > $o),A:($i > $i)] : ((bob @ sk1) | (B @ C) | (~ (~ (B @ C))) | ((rel @ sk1 @ (sk3 @ sk1 @ (^ [D:$i]: (rel @ (A @ D) @ D)))) != (B @ (sk3 @ C @ (B)))))),inference(paramod_ordered,[status(thm)],[2552,51])).
% 73.89/18.61 thf(2821,plain,(! [C:$i,B:($i > $o),A:($i > $i)] : ((bob @ sk1) | (B @ C) | ((rel @ sk1 @ (sk3 @ sk1 @ (^ [D:$i]: (rel @ (A @ D) @ D)))) != (B @ (sk3 @ C @ (B)))))),inference(simp,[status(thm)],[2820])).
% 73.89/18.61 thf(2873,plain,((bob @ sk1) | (rel @ sk1 @ sk1)),inference(pre_uni,[status(thm)],[2821:[bind(A, $thf(^ [D:$i]: (sk1))),bind(B, $thf(rel @ sk1)),bind(C, $thf(sk1))]])).
% 73.89/18.61 thf(2938,plain,(! [A:$i] : ((bob @ sk1) | ~ (($true)) | (bob @ sk1) | ((rel @ sk1 @ sk1) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[2873,2501])).
% 73.89/18.61 thf(2939,plain,(! [A:$i] : ((bob @ sk1) | ((rel @ sk1 @ sk1) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[2938])).
% 73.89/18.61 thf(2940,plain,((bob @ sk1)),inference(pattern_uni,[status(thm)],[2939:[bind(A, $thf(sk1))]])).
% 73.89/18.61 thf(3692,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((bob @ sk1) != (B @ A)))),inference(paramod_ordered,[status(thm)],[2940,57])).
% 73.89/18.61 thf(3693,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((bob @ sk1) != (B @ A)))),inference(simp,[status(thm)],[3692])).
% 73.89/18.61 thf(3824,plain,((bob @ (sk3 @ sk1 @ (^ [A:$i]: ~ (bob @ A))))),inference(pre_uni,[status(thm)],[3693:[bind(A, $thf(sk1)),bind(B, $thf(bob))]])).
% 73.89/18.61 thf(3985,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((bob @ (sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ C)))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3824,57])).
% 73.89/18.61 thf(3986,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((bob @ (sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ C)))) != (B @ A)))),inference(simp,[status(thm)],[3985])).
% 73.89/18.61 thf(3996,plain,((bob @ (sk3 @ (sk3 @ sk1 @ (^ [A:$i]: ~ (bob @ (sk3 @ A @ (^ [B:$i]: ~ (bob @ B)))))) @ (^ [A:$i]: ~ (bob @ A))))),inference(pre_uni,[status(thm)],[3986:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (bob @ (sk3 @ C @ (^ [D:$i]: ~ (bob @ D))))))]])).
% 73.89/18.61 thf(4,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ rel @ A) @ (mbox @ rel @ (mbox @ rel @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',trans_axiom)).
% 73.89/18.61 thf(18,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((rel @ B @ C) => (A @ C))) | ! [C:$i]: ((rel @ B @ C) => (! [D:$i]: ((rel @ C @ D) => (A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 73.89/18.61 thf(121,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ~ (($true)) | ((A @ B) != (deletefile1 @ sk2)))),inference(paramod_ordered,[status(thm)],[14,11])).
% 73.89/18.61 thf(122,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ((A @ B) != (deletefile1 @ sk2)))),inference(simp,[status(thm)],[121])).
% 73.89/18.61 thf(171,plain,((rel @ sk2 @ (sk3 @ sk2 @ (deletefile1)))),inference(pre_uni,[status(thm)],[122:[bind(A, $thf(deletefile1)),bind(B, $thf(sk2))]])).
% 73.89/18.61 thf(1520,plain,(! [B:$i,A:$i] : ((~ (rel @ A @ sk1)) | ~ (($true)) | (~ (admin @ B)) | ((rel @ sk1 @ (sk3 @ sk1 @ (admin))) != (rel @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[1491,94])).
% 73.89/18.61 thf(1521,plain,(! [B:$i,A:$i] : ((~ (rel @ A @ sk1)) | (~ (admin @ B)) | ((rel @ sk1 @ (sk3 @ sk1 @ (admin))) != (rel @ sk1 @ B)))),inference(simp,[status(thm)],[1520])).
% 73.89/18.61 thf(1522,plain,(! [A:$i] : ((~ (rel @ A @ sk1)) | (~ (admin @ (sk3 @ sk1 @ (admin)))))),inference(pattern_uni,[status(thm)],[1521:[bind(A, $thf(A)),bind(B, $thf(sk3 @ sk1 @ (admin)))]])).
% 73.89/18.61 thf(2190,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk2 @ (sk3 @ sk2 @ (deletefile1))) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[171,1522])).
% 73.89/18.61 thf(2191,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk2 @ (sk3 @ sk2 @ (deletefile1))) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[2190])).
% 73.89/18.61 thf(2214,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | (sk2 != A) | ((sk3 @ sk2 @ (deletefile1)) != sk1))),inference(simp,[status(thm)],[2191])).
% 73.89/18.61 thf(2224,plain,((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((sk3 @ sk2 @ (deletefile1)) != sk1)),inference(simp,[status(thm)],[2214])).
% 73.89/18.61 thf(3698,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((rel @ sk1 @ sk2) != (B @ A)))),inference(paramod_ordered,[status(thm)],[10,57])).
% 73.89/18.61 thf(3699,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((rel @ sk1 @ sk2) != (B @ A)))),inference(simp,[status(thm)],[3698])).
% 73.89/18.61 thf(3861,plain,((rel @ sk1 @ (sk3 @ sk2 @ (^ [A:$i]: ~ (rel @ sk1 @ A))))),inference(pre_uni,[status(thm)],[3699:[bind(A, $thf(sk2)),bind(B, $thf(rel @ sk1))]])).
% 73.89/18.61 thf(4137,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((rel @ sk1 @ (sk3 @ sk2 @ (^ [C:$i]: ~ (rel @ sk1 @ C)))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3861,57])).
% 73.89/18.61 thf(4138,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((rel @ sk1 @ (sk3 @ sk2 @ (^ [C:$i]: ~ (rel @ sk1 @ C)))) != (B @ A)))),inference(simp,[status(thm)],[4137])).
% 73.89/18.61 thf(4165,plain,((rel @ sk1 @ (sk3 @ (sk3 @ sk2 @ (^ [A:$i]: ~ (rel @ sk1 @ A))) @ (^ [A:$i]: ~ (rel @ sk1 @ A))))),inference(pre_uni,[status(thm)],[4138:[bind(A, $thf(sk3 @ sk2 @ (^ [C:$i]: ~ (rel @ sk1 @ C)))),bind(B, $thf(rel @ sk1))]])).
% 73.89/18.61 thf(3745,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((rel @ sk2 @ (sk3 @ sk2 @ (deletefile1))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[171,57])).
% 73.89/18.61 thf(3746,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((rel @ sk2 @ (sk3 @ sk2 @ (deletefile1))) != (B @ A)))),inference(simp,[status(thm)],[3745])).
% 73.89/18.61 thf(3858,plain,((rel @ (sk3 @ sk2 @ (^ [A:$i]: ~ (rel @ A @ (sk3 @ sk2 @ deletefile1)))) @ (sk3 @ sk2 @ (deletefile1)))),inference(pre_uni,[status(thm)],[3746:[bind(A, $thf(sk2)),bind(B, $thf(^ [C:$i]: (rel @ C @ (sk3 @ sk2 @ deletefile1))))]])).
% 73.89/18.61 thf(95,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (rel @ sk1 @ B)) | (~ (admin @ B)) | ((rel @ sk1 @ sk2) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[10,94])).
% 73.89/18.61 thf(96,plain,(! [B:$i,A:$i] : ((~ (rel @ sk1 @ B)) | (~ (admin @ B)) | ((rel @ sk1 @ sk2) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[95])).
% 73.89/18.61 thf(101,plain,(! [B:$i,A:$i] : ((~ (rel @ sk1 @ B)) | (~ (admin @ B)) | (sk1 != A) | (sk2 != sk1))),inference(simp,[status(thm)],[96])).
% 73.89/18.61 thf(103,plain,(! [A:$i] : ((~ (rel @ sk1 @ A)) | (~ (admin @ A)) | (sk2 != sk1))),inference(simp,[status(thm)],[101])).
% 73.89/18.61 thf(4958,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ A)) | (sk2 != sk1) | ((rel @ sk1 @ (sk3 @ sk2 @ (^ [B:$i]: ~ (rel @ sk1 @ B)))) != (rel @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[3861,103])).
% 73.89/18.61 thf(4959,plain,(! [A:$i] : ((~ (admin @ A)) | (sk2 != sk1) | ((rel @ sk1 @ (sk3 @ sk2 @ (^ [B:$i]: ~ (rel @ sk1 @ B)))) != (rel @ sk1 @ A)))),inference(simp,[status(thm)],[4958])).
% 73.89/18.61 thf(4960,plain,((~ (admin @ (sk3 @ sk2 @ (^ [A:$i]: ~ (rel @ sk1 @ A))))) | (sk2 != sk1)),inference(pattern_uni,[status(thm)],[4959:[bind(A, $thf(sk3 @ sk2 @ (^ [B:$i]: ~ (rel @ sk1 @ B))))]])).
% 73.89/18.61 thf(97,plain,(! [B:$i,A:$i] : ((~ (rel @ A @ sk1)) | ~ (($true)) | (~ (admin @ B)) | ((rel @ sk1 @ sk2) != (rel @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[10,94])).
% 73.89/18.61 thf(98,plain,(! [B:$i,A:$i] : ((~ (rel @ A @ sk1)) | (~ (admin @ B)) | ((rel @ sk1 @ sk2) != (rel @ sk1 @ B)))),inference(simp,[status(thm)],[97])).
% 73.89/18.61 thf(99,plain,(! [A:$i] : ((~ (rel @ A @ sk1)) | (~ (admin @ sk2)))),inference(pattern_uni,[status(thm)],[98:[bind(A, $thf(A)),bind(B, $thf(sk2))]])).
% 73.89/18.61 thf(316,plain,(! [C:$i,B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ~ (($true)) | (~ (admin @ sk2)) | ((A @ B) != (rel @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[14,99])).
% 73.89/18.61 thf(317,plain,(! [C:$i,B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | (~ (admin @ sk2)) | ((A @ B) != (rel @ C @ sk1)))),inference(simp,[status(thm)],[316])).
% 73.89/18.61 thf(324,plain,(! [A:($i > $i)] : ((rel @ sk1 @ (sk3 @ sk1 @ (^ [B:$i]: (rel @ (A @ B) @ B)))) | (~ (admin @ sk2)))),inference(pre_uni,[status(thm)],[317:[bind(A, $thf(^ [E:$i]: (rel @ (D @ E) @ E))),bind(B, $thf(sk1)),bind(C, $thf(D @ sk1))]])).
% 73.89/18.61 thf(332,plain,(! [A:($i > $i)] : ((rel @ sk1 @ (sk3 @ sk1 @ (^ [B:$i]: (rel @ (A @ B) @ B)))) | (~ (admin @ sk2)))),inference(simp,[status(thm)],[324])).
% 73.89/18.61 thf(3276,plain,(! [C:$i,B:($i > $o),A:($i > $i)] : ((~ (admin @ sk2)) | ~ (($true)) | (B @ C) | ((rel @ sk1 @ (sk3 @ sk1 @ (^ [D:$i]: (rel @ (A @ D) @ D)))) != (B @ (sk3 @ C @ (B)))))),inference(paramod_ordered,[status(thm)],[332,15])).
% 73.89/18.61 thf(3277,plain,(! [C:$i,B:($i > $o),A:($i > $i)] : ((~ (admin @ sk2)) | (B @ C) | ((rel @ sk1 @ (sk3 @ sk1 @ (^ [D:$i]: (rel @ (A @ D) @ D)))) != (B @ (sk3 @ C @ (B)))))),inference(simp,[status(thm)],[3276])).
% 73.89/18.61 thf(3286,plain,((~ (admin @ sk2)) | (rel @ sk1 @ sk1)),inference(pre_uni,[status(thm)],[3277:[bind(A, $thf(^ [D:$i]: (sk1))),bind(B, $thf(rel @ sk1)),bind(C, $thf(sk1))]])).
% 73.89/18.61 thf(3353,plain,(! [A:$i] : ((~ (admin @ sk2)) | ~ (($true)) | (~ (admin @ sk2)) | ((rel @ sk1 @ sk1) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[3286,99])).
% 73.89/18.61 thf(3354,plain,(! [A:$i] : ((~ (admin @ sk2)) | ((rel @ sk1 @ sk1) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[3353])).
% 73.89/18.61 thf(3355,plain,((~ (admin @ sk2))),inference(pattern_uni,[status(thm)],[3354:[bind(A, $thf(sk1))]])).
% 73.89/18.61 thf(3438,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ~ (($true)) | ((A @ B) != (admin @ sk2)))),inference(paramod_ordered,[status(thm)],[14,3355])).
% 73.89/18.61 thf(3439,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ((A @ B) != (admin @ sk2)))),inference(simp,[status(thm)],[3438])).
% 73.89/18.61 thf(3446,plain,((rel @ sk2 @ (sk3 @ sk2 @ (admin)))),inference(pre_uni,[status(thm)],[3439:[bind(A, $thf(admin)),bind(B, $thf(sk2))]])).
% 73.89/18.61 thf(3488,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk2 @ (sk3 @ sk2 @ (admin))) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[3446,1522])).
% 73.89/18.61 thf(3489,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk2 @ (sk3 @ sk2 @ (admin))) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[3488])).
% 73.89/18.61 thf(3522,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | (sk2 != A) | ((sk3 @ sk2 @ (admin)) != sk1))),inference(simp,[status(thm)],[3489])).
% 73.89/18.61 thf(3530,plain,((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((sk3 @ sk2 @ (admin)) != sk1)),inference(simp,[status(thm)],[3522])).
% 73.89/18.61 thf(3994,plain,((bob @ (sk3 @ (sk3 @ sk1 @ (^ [A:$i]: ~ (bob @ A))) @ (^ [A:$i]: ~ (bob @ A))))),inference(pre_uni,[status(thm)],[3986:[bind(A, $thf(sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ C)))),bind(B, $thf(bob))]])).
% 73.89/18.61 thf(4186,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((bob @ (sk3 @ (sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ C))) @ (^ [C:$i]: ~ (bob @ C)))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3994,57])).
% 73.89/18.61 thf(4187,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((bob @ (sk3 @ (sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ C))) @ (^ [C:$i]: ~ (bob @ C)))) != (B @ A)))),inference(simp,[status(thm)],[4186])).
% 73.89/18.61 thf(4198,plain,((bob @ (sk3 @ (sk3 @ (sk3 @ sk1 @ (^ [A:$i]: ~ (bob @ A))) @ (^ [A:$i]: ~ (bob @ (sk3 @ A @ (^ [B:$i]: ~ (bob @ B)))))) @ (^ [A:$i]: ~ (bob @ A))))),inference(pre_uni,[status(thm)],[4187:[bind(A, $thf(sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ C)))),bind(B, $thf(^ [C:$i]: (bob @ (sk3 @ C @ (^ [D:$i]: ~ (bob @ D))))))]])).
% 73.89/18.61 thf(1842,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ~ (($true)) | (sk2 != sk1) | ((A @ B) != (admin @ (sk3 @ sk1 @ (^ [C:$i]: (($false)))))))),inference(paramod_ordered,[status(thm)],[14,1837])).
% 73.89/18.61 thf(1843,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | (sk2 != sk1) | ((A @ B) != (admin @ (sk3 @ sk1 @ (^ [C:$i]: (($false)))))))),inference(simp,[status(thm)],[1842])).
% 73.89/18.61 thf(1858,plain,((rel @ sk1 @ (sk3 @ sk1 @ (^ [A:$i]: (admin @ (sk3 @ A @ (^ [B:$i]: (($false)))))))) | (sk2 != sk1)),inference(pre_uni,[status(thm)],[1843:[bind(A, $thf(^ [C:$i]: (admin @ (sk3 @ C @ (^ [D:$i]: (($false))))))),bind(B, $thf(sk1))]])).
% 73.89/18.61 thf(4946,plain,(! [A:$i] : ((sk2 != sk1) | ~ (($true)) | (~ (admin @ A)) | (sk2 != sk1) | ((rel @ sk1 @ (sk3 @ sk1 @ (^ [B:$i]: (admin @ (sk3 @ B @ (^ [C:$i]: (($false)))))))) != (rel @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[1858,103])).
% 73.89/18.61 thf(4947,plain,(! [A:$i] : ((sk2 != sk1) | (~ (admin @ A)) | ((rel @ sk1 @ (sk3 @ sk1 @ (^ [B:$i]: (admin @ (sk3 @ B @ (^ [C:$i]: (($false)))))))) != (rel @ sk1 @ A)))),inference(simp,[status(thm)],[4946])).
% 73.89/18.61 thf(4948,plain,((sk2 != sk1) | (~ (admin @ (sk3 @ sk1 @ (^ [A:$i]: (admin @ (sk3 @ A @ (^ [B:$i]: (($false)))))))))),inference(pattern_uni,[status(thm)],[4947:[bind(A, $thf(sk3 @ sk1 @ (^ [B:$i]: (admin @ (sk3 @ B @ (^ [C:$i]: (($false))))))))]])).
% 73.89/18.61 thf(33,plain,(! [A:$i] : ((~ (prop_a @ (sk3 @ A @ (prop_a)))) | (prop_a @ A))),inference(prim_subst,[status(thm)],[15:[bind(A, $thf(prop_a))]])).
% 73.89/18.61 thf(52,plain,(! [A:$i] : ((~ (prop_a @ (sk3 @ A @ (prop_a)))) | (prop_a @ A))),inference(simp,[status(thm)],[33])).
% 73.89/18.61 thf(2164,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk1 @ sk2) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[10,1522])).
% 73.89/18.61 thf(2165,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk1 @ sk2) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[2164])).
% 73.89/18.61 thf(2206,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | (sk1 != A) | (sk2 != sk1))),inference(simp,[status(thm)],[2165])).
% 73.89/18.61 thf(2239,plain,((~ (admin @ (sk3 @ sk1 @ (admin)))) | (sk2 != sk1)),inference(simp,[status(thm)],[2206])).
% 73.89/18.61 thf(2328,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | ~ (($true)) | (sk2 != sk1) | ((A @ B) != (admin @ (sk3 @ sk1 @ (admin)))))),inference(paramod_ordered,[status(thm)],[14,2239])).
% 73.89/18.61 thf(2329,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk3 @ B @ (A))) | (sk2 != sk1) | ((A @ B) != (admin @ (sk3 @ sk1 @ (admin)))))),inference(simp,[status(thm)],[2328])).
% 73.89/18.61 thf(2339,plain,((rel @ sk1 @ (sk3 @ sk1 @ (^ [A:$i]: (admin @ (sk3 @ A @ admin))))) | (sk2 != sk1)),inference(pre_uni,[status(thm)],[2329:[bind(A, $thf(^ [C:$i]: (admin @ (sk3 @ C @ admin)))),bind(B, $thf(sk1))]])).
% 73.89/18.61 thf(3855,plain,((rel @ sk2 @ (sk3 @ (sk3 @ sk2 @ (deletefile1)) @ (^ [A:$i]: ~ (rel @ sk2 @ A))))),inference(pre_uni,[status(thm)],[3746:[bind(A, $thf(sk3 @ sk2 @ (deletefile1))),bind(B, $thf(rel @ sk2))]])).
% 73.89/18.61 thf(19,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((((rel @ B @ (sk4 @ B @ (A))) | ~ (rel @ B @ C) | ~ (rel @ C @ D) | (A @ D)) & (~ (A @ (sk4 @ B @ (A))) | ~ (rel @ B @ C) | ~ (rel @ C @ D) | (A @ D))))),inference(cnf,[status(esa)],[18])).
% 73.89/18.61 thf(20,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[19])).
% 73.89/18.61 thf(36,plain,(! [A:$i] : ((~ (bob @ (sk3 @ A @ (bob)))) | (bob @ A))),inference(prim_subst,[status(thm)],[15:[bind(A, $thf(bob))]])).
% 73.89/18.61 thf(55,plain,(! [A:$i] : ((~ (bob @ (sk3 @ A @ (bob)))) | (bob @ A))),inference(simp,[status(thm)],[36])).
% 73.89/18.61 thf(3549,plain,(! [A:$i] : (~ (($true)) | (bob @ A) | ((bob @ (sk3 @ A @ (bob))) != (bob @ sk1)))),inference(paramod_ordered,[status(thm)],[2940,55])).
% 73.89/18.61 thf(3550,plain,(! [A:$i] : ((bob @ A) | ((bob @ (sk3 @ A @ (bob))) != (bob @ sk1)))),inference(simp,[status(thm)],[3549])).
% 73.89/18.61 thf(3557,plain,(! [A:$i] : ((bob @ A) | ((sk3 @ A @ (bob)) != sk1))),inference(simp,[status(thm)],[3550])).
% 73.89/18.61 thf(3702,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((rel @ sk2 @ (sk3 @ sk2 @ (admin))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3446,57])).
% 73.89/18.61 thf(3703,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((rel @ sk2 @ (sk3 @ sk2 @ (admin))) != (B @ A)))),inference(simp,[status(thm)],[3702])).
% 73.89/18.61 thf(3866,plain,((rel @ sk2 @ (sk3 @ (sk3 @ sk2 @ (admin)) @ (^ [A:$i]: ~ (rel @ sk2 @ A))))),inference(pre_uni,[status(thm)],[3703:[bind(A, $thf(sk3 @ sk2 @ (admin))),bind(B, $thf(rel @ sk2))]])).
% 73.89/18.61 thf(1759,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk1 @ (sk3 @ sk1 @ (admin))) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[1491,299])).
% 73.89/18.61 thf(1760,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk1 @ (sk3 @ sk1 @ (admin))) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[1759])).
% 73.89/18.61 thf(1792,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | (sk1 != A) | ((sk3 @ sk1 @ (admin)) != sk1))),inference(simp,[status(thm)],[1760])).
% 73.89/18.61 thf(1815,plain,((~ (admin @ (sk3 @ sk1 @ (^ [A:$i]: (($false)))))) | ((sk3 @ sk1 @ (admin)) != sk1)),inference(simp,[status(thm)],[1792])).
% 73.89/18.61 thf(2178,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ A @ (sk3 @ A @ (^ [C:$i]: (($false))))) != (rel @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[196,1522])).
% 73.89/18.61 thf(2179,plain,(! [B:$i,A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ A @ (sk3 @ A @ (^ [C:$i]: (($false))))) != (rel @ B @ sk1)))),inference(simp,[status(thm)],[2178])).
% 73.89/18.61 thf(2212,plain,(! [B:$i,A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | (A != B) | ((sk3 @ A @ (^ [C:$i]: (($false)))) != sk1))),inference(simp,[status(thm)],[2179])).
% 73.89/18.61 thf(2222,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((sk3 @ A @ (^ [B:$i]: (($false)))) != sk1))),inference(simp,[status(thm)],[2212])).
% 73.89/18.61 thf(141,plain,(! [A:$i] : ((rel @ A @ (sk3 @ A @ (deletefile1))) | (deletefile1 @ A))),inference(prim_subst,[status(thm)],[14:[bind(A, $thf(deletefile1))]])).
% 73.89/18.61 thf(179,plain,(! [A:$i] : ((rel @ A @ (sk3 @ A @ (deletefile1))) | (deletefile1 @ A))),inference(simp,[status(thm)],[141])).
% 73.89/18.61 thf(2170,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk1 @ (sk3 @ sk1 @ (admin))) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[1491,1522])).
% 73.89/18.61 thf(2171,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk1 @ (sk3 @ sk1 @ (admin))) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[2170])).
% 73.89/18.61 thf(2203,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | (sk1 != A) | ((sk3 @ sk1 @ (admin)) != sk1))),inference(simp,[status(thm)],[2171])).
% 73.89/18.61 thf(2236,plain,((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((sk3 @ sk1 @ (admin)) != sk1)),inference(simp,[status(thm)],[2203])).
% 73.89/18.61 thf(41,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((~ (rel @ (B @ (sk3 @ A @ (^ [D:$i]: (rel @ (B @ D) @ (C @ D))))) @ (C @ (sk3 @ A @ (^ [D:$i]: (rel @ (B @ D) @ (C @ D))))))) | (rel @ (B @ A) @ (C @ A)))),inference(prim_subst,[status(thm)],[15:[bind(A, $thf(^ [E:$i]: (rel @ (C @ E) @ (D @ E))))]])).
% 73.89/18.61 thf(61,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((~ (rel @ (B @ (sk3 @ A @ (^ [D:$i]: (rel @ (B @ D) @ (C @ D))))) @ (C @ (sk3 @ A @ (^ [D:$i]: (rel @ (B @ D) @ (C @ D))))))) | (rel @ (B @ A) @ (C @ A)))),inference(simp,[status(thm)],[41])).
% 73.89/18.61 thf(4964,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ A)) | (sk2 != sk1) | ((rel @ sk2 @ (sk3 @ sk2 @ (deletefile1))) != (rel @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[171,103])).
% 73.89/18.61 thf(4965,plain,(! [A:$i] : ((~ (admin @ A)) | (sk2 != sk1) | ((rel @ sk2 @ (sk3 @ sk2 @ (deletefile1))) != (rel @ sk1 @ A)))),inference(simp,[status(thm)],[4964])).
% 73.89/18.61 thf(4977,plain,(! [A:$i] : ((~ (admin @ A)) | (sk2 != sk1) | (sk2 != sk1) | ((sk3 @ sk2 @ (deletefile1)) != A))),inference(simp,[status(thm)],[4965])).
% 73.89/18.61 thf(4996,plain,((~ (admin @ (sk3 @ sk2 @ (deletefile1)))) | (sk2 != sk1)),inference(simp,[status(thm)],[4977])).
% 73.89/18.61 thf(4922,plain,(! [A:$i] : ((sk2 != sk1) | ~ (($true)) | (~ (admin @ A)) | (sk2 != sk1) | ((rel @ sk1 @ (sk3 @ sk1 @ (^ [B:$i]: (admin @ (sk3 @ B @ admin))))) != (rel @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[2339,103])).
% 73.89/18.61 thf(4923,plain,(! [A:$i] : ((sk2 != sk1) | (~ (admin @ A)) | ((rel @ sk1 @ (sk3 @ sk1 @ (^ [B:$i]: (admin @ (sk3 @ B @ admin))))) != (rel @ sk1 @ A)))),inference(simp,[status(thm)],[4922])).
% 73.89/18.61 thf(4924,plain,((sk2 != sk1) | (~ (admin @ (sk3 @ sk1 @ (^ [A:$i]: (admin @ (sk3 @ A @ admin))))))),inference(pattern_uni,[status(thm)],[4923:[bind(A, $thf(sk3 @ sk1 @ (^ [B:$i]: (admin @ (sk3 @ B @ admin)))))]])).
% 73.89/18.61 thf(3857,plain,((rel @ sk2 @ (sk3 @ (sk3 @ sk2 @ (^ [A:$i]: ~ (rel @ sk2 @ (sk3 @ A @ deletefile1)))) @ (deletefile1)))),inference(pre_uni,[status(thm)],[3746:[bind(A, $thf(sk2)),bind(B, $thf(^ [C:$i]: (rel @ sk2 @ (sk3 @ C @ deletefile1))))]])).
% 73.89/18.61 thf(40,plain,(! [B:($i > $i),A:$i] : ((~ (bob @ (B @ (sk3 @ A @ (^ [C:$i]: (bob @ (B @ C))))))) | (bob @ (B @ A)))),inference(prim_subst,[status(thm)],[15:[bind(A, $thf(^ [D:$i]: (bob @ (C @ D))))]])).
% 73.89/18.61 thf(60,plain,(! [B:($i > $i),A:$i] : ((~ (bob @ (B @ (sk3 @ A @ (^ [C:$i]: (bob @ (B @ C))))))) | (bob @ (B @ A)))),inference(simp,[status(thm)],[40])).
% 73.89/18.61 thf(3484,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk2 @ (sk3 @ sk2 @ (admin))) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[3446,299])).
% 73.89/18.61 thf(3485,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk2 @ (sk3 @ sk2 @ (admin))) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[3484])).
% 73.89/18.61 thf(3523,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | (sk2 != A) | ((sk3 @ sk2 @ (admin)) != sk1))),inference(simp,[status(thm)],[3485])).
% 73.89/18.61 thf(3531,plain,((~ (admin @ (sk3 @ sk1 @ (^ [A:$i]: (($false)))))) | ((sk3 @ sk2 @ (admin)) != sk1)),inference(simp,[status(thm)],[3523])).
% 73.89/18.61 thf(3827,plain,((rel @ sk1 @ (sk3 @ (sk3 @ sk1 @ (admin)) @ (^ [A:$i]: ~ (rel @ sk1 @ A))))),inference(pre_uni,[status(thm)],[3689:[bind(A, $thf(sk3 @ sk1 @ (admin))),bind(B, $thf(rel @ sk1))]])).
% 73.89/18.61 thf(21,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk4 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[19])).
% 73.89/18.61 thf(4913,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ A)) | (sk2 != sk1) | ((rel @ sk2 @ (sk3 @ sk2 @ (admin))) != (rel @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[3446,103])).
% 73.89/18.61 thf(4914,plain,(! [A:$i] : ((~ (admin @ A)) | (sk2 != sk1) | ((rel @ sk2 @ (sk3 @ sk2 @ (admin))) != (rel @ sk1 @ A)))),inference(simp,[status(thm)],[4913])).
% 73.89/18.61 thf(4986,plain,(! [A:$i] : ((~ (admin @ A)) | (sk2 != sk1) | (sk2 != sk1) | ((sk3 @ sk2 @ (admin)) != A))),inference(simp,[status(thm)],[4914])).
% 73.89/18.61 thf(5006,plain,((~ (admin @ (sk3 @ sk2 @ (admin)))) | (sk2 != sk1)),inference(simp,[status(thm)],[4986])).
% 73.89/18.61 thf(5329,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((bob @ (sk3 @ (sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ (sk3 @ C @ (^ [D:$i]: ~ (bob @ D)))))) @ (^ [C:$i]: ~ (bob @ C)))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3996,57])).
% 73.89/18.61 thf(5330,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((bob @ (sk3 @ (sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ (sk3 @ C @ (^ [D:$i]: ~ (bob @ D)))))) @ (^ [C:$i]: ~ (bob @ C)))) != (B @ A)))),inference(simp,[status(thm)],[5329])).
% 73.89/18.61 thf(5345,plain,((bob @ (sk3 @ (sk3 @ (sk3 @ sk1 @ (^ [A:$i]: ~ (bob @ (sk3 @ A @ (^ [B:$i]: ~ (bob @ B)))))) @ (^ [A:$i]: ~ (bob @ A))) @ (^ [A:$i]: ~ (bob @ A))))),inference(pre_uni,[status(thm)],[5330:[bind(A, $thf(sk3 @ (sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ (sk3 @ C @ (^ [D:$i]: ~ (bob @ D)))))) @ (^ [C:$i]: ~ (bob @ C)))),bind(B, $thf(bob))]])).
% 73.89/18.61 thf(34,plain,(! [A:$i] : ((~ (admin @ (sk3 @ A @ (admin)))) | (admin @ A))),inference(prim_subst,[status(thm)],[15:[bind(A, $thf(admin))]])).
% 73.89/18.61 thf(53,plain,(! [A:$i] : ((~ (admin @ (sk3 @ A @ (admin)))) | (admin @ A))),inference(simp,[status(thm)],[34])).
% 73.89/18.61 thf(4943,plain,(! [B:$i,A:$i] : ((deletefile1 @ A) | ~ (($true)) | (~ (admin @ B)) | (sk2 != sk1) | ((rel @ A @ (sk3 @ A @ (deletefile1))) != (rel @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[179,103])).
% 73.89/18.61 thf(4944,plain,(! [B:$i,A:$i] : ((deletefile1 @ A) | (~ (admin @ B)) | (sk2 != sk1) | ((rel @ A @ (sk3 @ A @ (deletefile1))) != (rel @ sk1 @ B)))),inference(simp,[status(thm)],[4943])).
% 73.89/18.61 thf(4945,plain,((deletefile1 @ sk1) | (~ (admin @ (sk3 @ sk1 @ (deletefile1)))) | (sk2 != sk1)),inference(pattern_uni,[status(thm)],[4944:[bind(A, $thf(sk1)),bind(B, $thf(sk3 @ sk1 @ (deletefile1)))]])).
% 73.89/18.61 thf(5529,plain,((~ (admin @ (sk3 @ sk1 @ (deletefile1)))) | (sk2 != sk1) | ~ (($true)) | ((deletefile1 @ sk2) != (deletefile1 @ sk1))),inference(paramod_ordered,[status(thm)],[4945,11])).
% 73.89/18.61 thf(5530,plain,((~ (admin @ (sk3 @ sk1 @ (deletefile1)))) | (sk2 != sk1) | ((deletefile1 @ sk2) != (deletefile1 @ sk1))),inference(simp,[status(thm)],[5529])).
% 73.89/18.61 thf(5543,plain,((~ (admin @ (sk3 @ sk1 @ (deletefile1)))) | (sk2 != sk1) | (sk2 != sk1)),inference(simp,[status(thm)],[5530])).
% 73.89/18.61 thf(5557,plain,((~ (admin @ (sk3 @ sk1 @ (deletefile1)))) | (sk2 != sk1)),inference(simp,[status(thm)],[5543])).
% 73.89/18.61 thf(39,plain,(! [B:($i > $i),A:$i] : ((~ (admin @ (B @ (sk3 @ A @ (^ [C:$i]: (admin @ (B @ C))))))) | (admin @ (B @ A)))),inference(prim_subst,[status(thm)],[15:[bind(A, $thf(^ [D:$i]: (admin @ (C @ D))))]])).
% 73.89/18.61 thf(59,plain,(! [B:($i > $i),A:$i] : ((~ (admin @ (B @ (sk3 @ A @ (^ [C:$i]: (admin @ (B @ C))))))) | (admin @ (B @ A)))),inference(simp,[status(thm)],[39])).
% 73.89/18.61 thf(3868,plain,((rel @ sk2 @ (sk3 @ (sk3 @ sk2 @ (^ [A:$i]: ~ (rel @ sk2 @ (sk3 @ A @ admin)))) @ (admin)))),inference(pre_uni,[status(thm)],[3703:[bind(A, $thf(sk2)),bind(B, $thf(^ [C:$i]: (rel @ sk2 @ (sk3 @ C @ admin))))]])).
% 73.89/18.61 thf(6,axiom,((iclval @ (icl_says @ (icl_princ @ admin) @ (icl_says @ (icl_impl @ (icl_princ @ bob) @ (icl_princ @ admin)) @ (icl_atom @ deletefile1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2)).
% 73.89/18.61 thf(26,plain,((! [A:$i,B:$i]: ((rel @ A @ B) => ((admin @ B) | ! [C:$i]: ((rel @ B @ C) => (! [D:$i]: ((rel @ C @ D) => (~ (bob @ D) | (admin @ D))) | ! [D:$i]: ((rel @ C @ D) => (deletefile1 @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 73.89/18.61 thf(27,plain,(! [E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel @ A @ B)) | (admin @ B) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (bob @ D)) | (admin @ D) | (~ (rel @ C @ E)) | (deletefile1 @ E))),inference(cnf,[status(esa)],[26])).
% 73.89/18.61 thf(35,plain,(! [B:($i > $i),A:$i] : ((~ (prop_c @ (B @ (sk3 @ A @ (^ [C:$i]: (prop_c @ (B @ C))))))) | (prop_c @ (B @ A)))),inference(prim_subst,[status(thm)],[15:[bind(A, $thf(^ [D:$i]: (prop_c @ (C @ D))))]])).
% 73.89/18.61 thf(54,plain,(! [B:($i > $i),A:$i] : ((~ (prop_c @ (B @ (sk3 @ A @ (^ [C:$i]: (prop_c @ (B @ C))))))) | (prop_c @ (B @ A)))),inference(simp,[status(thm)],[35])).
% 73.89/18.61 thf(4121,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk1 @ (sk3 @ sk2 @ (^ [B:$i]: ~ (rel @ sk1 @ B)))) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[3861,299])).
% 73.89/18.61 thf(4122,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk1 @ (sk3 @ sk2 @ (^ [B:$i]: ~ (rel @ sk1 @ B)))) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[4121])).
% 73.89/18.61 thf(4164,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | (sk1 != A) | ((sk3 @ sk2 @ (^ [B:$i]: ~ (rel @ sk1 @ B))) != sk1))),inference(simp,[status(thm)],[4122])).
% 73.89/18.61 thf(4171,plain,((~ (admin @ (sk3 @ sk1 @ (^ [A:$i]: (($false)))))) | ((sk3 @ sk2 @ (^ [A:$i]: ~ (rel @ sk1 @ A))) != sk1)),inference(simp,[status(thm)],[4164])).
% 73.89/18.61 thf(4123,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk1 @ (sk3 @ sk2 @ (^ [B:$i]: ~ (rel @ sk1 @ B)))) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[3861,1522])).
% 73.89/18.61 thf(4124,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((rel @ sk1 @ (sk3 @ sk2 @ (^ [B:$i]: ~ (rel @ sk1 @ B)))) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[4123])).
% 73.89/18.61 thf(4162,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (admin)))) | (sk1 != A) | ((sk3 @ sk2 @ (^ [B:$i]: ~ (rel @ sk1 @ B))) != sk1))),inference(simp,[status(thm)],[4124])).
% 73.89/18.61 thf(4168,plain,((~ (admin @ (sk3 @ sk1 @ (admin)))) | ((sk3 @ sk2 @ (^ [A:$i]: ~ (rel @ sk1 @ A))) != sk1)),inference(simp,[status(thm)],[4162])).
% 73.89/18.61 thf(3829,plain,((rel @ sk1 @ (sk3 @ (sk3 @ sk1 @ (^ [A:$i]: ~ (rel @ sk1 @ (sk3 @ A @ admin)))) @ (admin)))),inference(pre_uni,[status(thm)],[3689:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (rel @ sk1 @ (sk3 @ C @ admin))))]])).
% 73.89/18.61 thf(22,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ ((sk4 @ B @ (A)) = (sk4 @ B @ ((=) @ $i @ (sk4 @ B @ A))))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ((sk4 @ B @ (A)) = D))),inference(replace_leibeq,[status(thm)],[21:[bind(A, $thf((=) @ $i @ (sk4 @ B @ A)))]])).
% 73.89/18.61 thf(23,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : (((sk4 @ B @ (A)) != (sk4 @ B @ ((=) @ $i @ (sk4 @ B @ A)))) | ((sk4 @ B @ (A)) = D) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)))),inference(lifteq,[status(thm)],[22])).
% 73.89/18.61 thf(4197,plain,((bob @ (sk3 @ (sk3 @ (sk3 @ sk1 @ (^ [A:$i]: ~ (bob @ A))) @ (^ [A:$i]: ~ (bob @ A))) @ (^ [A:$i]: ~ (bob @ A))))),inference(pre_uni,[status(thm)],[4187:[bind(A, $thf(sk3 @ (sk3 @ sk1 @ (^ [C:$i]: ~ (bob @ C))) @ (^ [C:$i]: ~ (bob @ C)))),bind(B, $thf(bob))]])).
% 73.89/18.61 thf(38,plain,(! [B:($i > $i),A:$i] : ((~ (prop_b @ (B @ (sk3 @ A @ (^ [C:$i]: (prop_b @ (B @ C))))))) | (prop_b @ (B @ A)))),inference(prim_subst,[status(thm)],[15:[bind(A, $thf(^ [D:$i]: (prop_b @ (C @ D))))]])).
% 73.89/18.61 thf(58,plain,(! [B:($i > $i),A:$i] : ((~ (prop_b @ (B @ (sk3 @ A @ (^ [C:$i]: (prop_b @ (B @ C))))))) | (prop_b @ (B @ A)))),inference(simp,[status(thm)],[38])).
% 73.89/18.61 thf(3860,plain,((rel @ (sk3 @ sk1 @ (^ [A:$i]: ~ (rel @ A @ sk2))) @ sk2)),inference(pre_uni,[status(thm)],[3699:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (rel @ C @ sk2)))]])).
% 73.89/18.61 thf(4047,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((rel @ (sk3 @ sk1 @ (^ [C:$i]: ~ (rel @ C @ sk2))) @ sk2) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3860,57])).
% 73.89/18.61 thf(4048,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((rel @ (sk3 @ sk1 @ (^ [C:$i]: ~ (rel @ C @ sk2))) @ sk2) != (B @ A)))),inference(simp,[status(thm)],[4047])).
% 73.89/18.61 thf(4074,plain,((rel @ (sk3 @ (sk3 @ sk1 @ (^ [A:$i]: ~ (rel @ A @ sk2))) @ (^ [A:$i]: ~ (rel @ A @ sk2))) @ sk2)),inference(pre_uni,[status(thm)],[4048:[bind(A, $thf(sk3 @ sk1 @ (^ [C:$i]: ~ (rel @ C @ sk2)))),bind(B, $thf(^ [C:$i]: (rel @ C @ sk2)))]])).
% 73.89/18.61 thf(4529,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((rel @ sk2 @ (sk3 @ (sk3 @ sk2 @ (admin)) @ (^ [C:$i]: ~ (rel @ sk2 @ C)))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3866,57])).
% 73.89/18.61 thf(4530,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((rel @ sk2 @ (sk3 @ (sk3 @ sk2 @ (admin)) @ (^ [C:$i]: ~ (rel @ sk2 @ C)))) != (B @ A)))),inference(simp,[status(thm)],[4529])).
% 73.89/18.61 thf(4565,plain,((rel @ sk2 @ (sk3 @ (sk3 @ (sk3 @ sk2 @ (admin)) @ (^ [A:$i]: ~ (rel @ sk2 @ A))) @ (^ [A:$i]: ~ (rel @ sk2 @ A))))),inference(pre_uni,[status(thm)],[4530:[bind(A, $thf(sk3 @ (sk3 @ sk2 @ (admin)) @ (^ [C:$i]: ~ (rel @ sk2 @ C)))),bind(B, $thf(rel @ sk2))]])).
% 73.89/18.61 thf(4438,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((rel @ sk2 @ (sk3 @ (sk3 @ sk2 @ (deletefile1)) @ (^ [C:$i]: ~ (rel @ sk2 @ C)))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3855,57])).
% 73.89/18.61 thf(4439,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((rel @ sk2 @ (sk3 @ (sk3 @ sk2 @ (deletefile1)) @ (^ [C:$i]: ~ (rel @ sk2 @ C)))) != (B @ A)))),inference(simp,[status(thm)],[4438])).
% 73.89/18.61 thf(4474,plain,((rel @ sk2 @ (sk3 @ (sk3 @ (sk3 @ sk2 @ (deletefile1)) @ (^ [A:$i]: ~ (rel @ sk2 @ A))) @ (^ [A:$i]: ~ (rel @ sk2 @ A))))),inference(pre_uni,[status(thm)],[4439:[bind(A, $thf(sk3 @ (sk3 @ sk2 @ (deletefile1)) @ (^ [C:$i]: ~ (rel @ sk2 @ C)))),bind(B, $thf(rel @ sk2))]])).
% 73.89/18.61 thf(4314,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((rel @ sk1 @ (sk3 @ (sk3 @ sk1 @ (admin)) @ (^ [C:$i]: ~ (rel @ sk1 @ C)))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3827,57])).
% 73.89/18.61 thf(4315,plain,(! [B:($i > $o),A:$i] : ((B @ (sk3 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((rel @ sk1 @ (sk3 @ (sk3 @ sk1 @ (admin)) @ (^ [C:$i]: ~ (rel @ sk1 @ C)))) != (B @ A)))),inference(simp,[status(thm)],[4314])).
% 73.89/18.61 thf(4350,plain,((rel @ sk1 @ (sk3 @ (sk3 @ (sk3 @ sk1 @ (admin)) @ (^ [A:$i]: ~ (rel @ sk1 @ A))) @ (^ [A:$i]: ~ (rel @ sk1 @ A))))),inference(pre_uni,[status(thm)],[4315:[bind(A, $thf(sk3 @ (sk3 @ sk1 @ (admin)) @ (^ [C:$i]: ~ (rel @ sk1 @ C)))),bind(B, $thf(rel @ sk1))]])).
% 73.89/18.61 thf(1782,plain,(! [A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk2 @ (sk3 @ sk2 @ (deletefile1))) != (rel @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[171,299])).
% 73.89/18.61 thf(1783,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((rel @ sk2 @ (sk3 @ sk2 @ (deletefile1))) != (rel @ A @ sk1)))),inference(simp,[status(thm)],[1782])).
% 73.89/18.61 thf(1793,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | (sk2 != A) | ((sk3 @ sk2 @ (deletefile1)) != sk1))),inference(simp,[status(thm)],[1783])).
% 73.89/18.61 thf(1816,plain,((~ (admin @ (sk3 @ sk1 @ (^ [A:$i]: (($false)))))) | ((sk3 @ sk2 @ (deletefile1)) != sk1)),inference(simp,[status(thm)],[1793])).
% 73.89/18.61 thf(1768,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (admin @ (sk3 @ sk1 @ (^ [C:$i]: (($false)))))) | ((rel @ A @ (sk3 @ A @ (^ [C:$i]: (($false))))) != (rel @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[196,299])).
% 73.89/18.61 thf(1769,plain,(! [B:$i,A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [C:$i]: (($false)))))) | ((rel @ A @ (sk3 @ A @ (^ [C:$i]: (($false))))) != (rel @ B @ sk1)))),inference(simp,[status(thm)],[1768])).
% 73.89/18.61 thf(1806,plain,(! [B:$i,A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [C:$i]: (($false)))))) | (A != B) | ((sk3 @ A @ (^ [C:$i]: (($false)))) != sk1))),inference(simp,[status(thm)],[1769])).
% 73.89/18.61 thf(1829,plain,(! [A:$i] : ((~ (admin @ (sk3 @ sk1 @ (^ [B:$i]: (($false)))))) | ((sk3 @ A @ (^ [B:$i]: (($false)))) != sk1))),inference(simp,[status(thm)],[1806])).
% 73.89/18.61 thf(3869,plain,((rel @ (sk3 @ sk2 @ (^ [A:$i]: ~ (rel @ A @ (sk3 @ sk2 @ admin)))) @ (sk3 @ sk2 @ (admin)))),inference(pre_uni,[status(thm)],[3703:[bind(A, $thf(sk2)),bind(B, $thf(^ [C:$i]: (rel @ C @ (sk3 @ sk2 @ admin))))]])).
% 73.89/18.61 thf(9388,plain,(($false)),inference(e,[status(thm)],[3830,1837,1424,17,3996,299,18,2224,4165,2940,3858,1522,4960,10,3530,3446,3994,24,4198,4948,25,52,14,2339,196,3855,20,3557,3866,29,1815,57,2222,179,2236,1858,61,4996,4924,3857,60,3531,3827,28,21,5006,5345,53,3824,5557,59,3868,27,12,54,4171,3355,103,3861,2239,4168,3829,11,26,55,171,23,8,1491,4197,58,4074,3860,51,4565,4474,94,4350,1816,1829,3869,15])).
% 73.89/18.61 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 73.89/18.61 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------