Leo-III run on the at.alkalam.org runner container $ java -jar /opt/leo3.jar --version Leo-III 1.7.18 command per file: java -Xmx1024m -jar /opt/leo3.jar -t 50 -p $ shasum -a 256 *.p c14128f23990fa7ccdbf7b636c0b604f2b37dd3c722a2c9b491e4b04b529478d imkan_a_1_case_split.p 42edd0b0900c198aec4fa4fa9b12888a30ce9739b1646725099bf63296dd4c89 imkan_a_2a_member_case.p 21e7b878138c357afb0099e02a06f4c2d7d54084290bfbcdf8630296a43705a7 imkan_a_2b_only_aggregate_case.p e153e774ff4d96578022dd2ef7df08ff5ff5bf60e5fdcadb067b0c7f9eadc810 imkan_a_assembly_abstract.p 24f3dce6851f30de9c7fcfdeb62c1a93b15789a13f5ad5d0f589940667fe90ab imkan_a_assembly.p 972c9822a8bbf1aaf9bb2259f02f7152db407f347c997360629d939e82bf0878 imkan_b_short.p =================== imkan_a_1_case_split.p % [INFO] Parsing problem /tmp/xc.p ... % [INFO] Parsing done (137ms). % [INFO] Running in sequential loop mode. % [INFO] Scanning for conjecture ... % [INFO] Found a conjecture (or negated_conjecture) and 3 axioms. Running axiom selection ... % [INFO] Axiom selection finished. Selected 3 axioms (removed 0 axioms). % [INFO] Problem is higher-order (TPTP THF). % [INFO] Type checking passed. % [CONFIG] Using configuration: timeout(50) with strategy. Searching for refutation ... % Time passed: 1330ms (effective reasoning time: 799ms) % Solved by strategy % Axioms used in derivation (2): sp001, possible_case % No. of inferences in proof: 25 % SZS status Theorem for /tmp/xc.p : 1330 ms resp. 799 ms w/o parsing % SZS output start Refutation for /tmp/xc.p thf(ex_type, type, ex: ($i > $o)). thf(ess_type, type, ess: ($i > $o)). thf(nec_type, type, nec: ($i > $o)). thf(poss_type, type, poss: ($i > $o)). thf(sk1_type, type, sk1: $i). thf(sk2_type, type, sk2: $i). thf(nec_def, definition, (nec = (^ [A:$i]: ((ex @ A) & (ess @ A))))). thf(poss_def, definition, (poss = (^ [A:$i]: ((ex @ A) & ~ (ess @ A))))). thf(5,axiom,((? [A:$i]: (ex @ A))),file('/tmp/xc.p',sp001)). thf(17,plain,((? [A:$i]: (ex @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])). thf(18,plain,((ex @ sk2)),inference(cnf,[status(esa)],[17])). thf(4,axiom,(((? [A:$i]: (poss @ A)) => (? [A:$i]: (nec @ A)))),file('/tmp/xc.p',possible_case)). thf(14,plain,(((? [A:$i]: ((ex @ A) & ~ (ess @ A))) => (? [A:$i]: ((ex @ A) & (ess @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])). thf(16,plain,(! [A:$i] : ((~ (ex @ A)) | (ess @ A) | (ess @ sk1))),inference(cnf,[status(esa)],[14])). thf(15,plain,(! [A:$i] : ((~ (ex @ A)) | (ess @ A) | (ex @ sk1))),inference(cnf,[status(esa)],[14])). thf(1,conjecture,((? [A:$i]: (nec @ A))),file('/tmp/xc.p',conclusion)). thf(2,negated_conjecture,((~ (? [A:$i]: (nec @ A)))),inference(neg_conjecture,[status(cth)],[1])). thf(6,plain,((~ (? [A:$i]: ((ex @ A) & (ess @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(7,plain,(! [A:$i] : ((~ (ex @ A)) | (~ (ess @ A)))),inference(cnf,[status(esa)],[6])). thf(19,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ sk2) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[18,7])). thf(20,plain,((~ (ess @ sk2))),inference(pattern_uni,[status(thm)],[19:[bind(A, $thf(sk2))]])). thf(23,plain,(! [A:$i] : ((~ (ex @ A)) | (ex @ sk1) | ((ess @ A) != (ess @ sk2)))),inference(paramod_ordered,[status(thm)],[15,20])). thf(24,plain,((~ (ex @ sk2)) | (ex @ sk1)),inference(pattern_uni,[status(thm)],[23:[bind(A, $thf(sk2))]])). thf(28,plain,(~ (($true)) | (ex @ sk1)),inference(rewrite,[status(thm)],[24,18])). thf(29,plain,((ex @ sk1)),inference(simp,[status(thm)],[28])). thf(30,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ sk1) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[29,7])). thf(31,plain,((~ (ess @ sk1))),inference(pattern_uni,[status(thm)],[30:[bind(A, $thf(sk1))]])). thf(35,plain,(! [A:$i] : ((~ (ex @ A)) | (ess @ A) | ($false))),inference(rewrite,[status(thm)],[16,31])). thf(36,plain,(! [A:$i] : ((~ (ex @ A)) | (ess @ A))),inference(simp,[status(thm)],[35])). thf(39,plain,(! [A:$i] : ((ess @ A) | ((ex @ sk2) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[18,36])). thf(40,plain,((ess @ sk2)),inference(pattern_uni,[status(thm)],[39:[bind(A, $thf(sk2))]])). thf(48,plain,(($false)),inference(rewrite,[status(thm)],[40,20])). thf(49,plain,(($false)),inference(simp,[status(thm)],[48])). % SZS output end Refutation for /tmp/xc.p =================== imkan_a_2a_member_case.p % [INFO] Parsing problem /tmp/xc.p ... % [INFO] Parsing done (148ms). % [INFO] Running in sequential loop mode. % [INFO] Scanning for conjecture ... % [INFO] Found a conjecture (or negated_conjecture) and 5 axioms. Running axiom selection ... % [INFO] Axiom selection finished. Selected 5 axioms (removed 0 axioms). % [INFO] Problem is higher-order (TPTP THF). % [INFO] Type checking passed. % [CONFIG] Using configuration: timeout(50) with strategy. Searching for refutation ... % Time passed: 1584ms (effective reasoning time: 1051ms) % Solved by strategy % Axioms used in derivation (3): case_agg, step3, step11 % No. of inferences in proof: 31 % SZS status Theorem for /tmp/xc.p : 1584 ms resp. 1051 ms w/o parsing % SZS output start Refutation for /tmp/xc.p thf(ex_type, type, ex: ($i > $o)). thf(ess_type, type, ess: ($i > $o)). thf(gives_type, type, gives: ($i > ($i > $o))). thf(nec_type, type, nec: ($i > $o)). thf(poss_type, type, poss: ($i > $o)). thf(through_another_type, type, through_another: ($i > $o)). thf(agg_type, type, agg: ($i > $o)). thf(a_type, type, a: $i). thf(sk1_type, type, sk1: ($i > $i)). thf(nec_def, definition, (nec = (^ [A:$i]: ((ex @ A) & (ess @ A))))). thf(poss_def, definition, (poss = (^ [A:$i]: ((ex @ A) & ~ (ess @ A))))). thf(through_another_def, definition, (through_another = (^ [A:$i]: ? [B:$i]: (gives @ B @ A)))). thf(6,axiom,(((agg @ a) & (ex @ a))),file('/tmp/xc.p',case_agg)). thf(20,plain,(((agg @ a) & (ex @ a))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])). thf(21,plain,((ex @ a)),inference(cnf,[status(esa)],[20])). thf(3,axiom,((! [A:$i]: ((poss @ A) => (through_another @ A)))),file('/tmp/xc.p',step3)). thf(10,plain,((! [A:$i]: (((ex @ A) & ~ (ess @ A)) => (? [B:$i]: (gives @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])). thf(11,plain,(! [A:$i] : ((~ (ex @ A)) | (ess @ A) | (gives @ (sk1 @ A) @ A))),inference(cnf,[status(esa)],[10])). thf(32,plain,(! [A:$i] : ((ess @ A) | (gives @ (sk1 @ A) @ A) | ((ex @ a) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[21,11])). thf(33,plain,((ess @ a) | (gives @ (sk1 @ a) @ a)),inference(pattern_uni,[status(thm)],[32:[bind(A, $thf(a))]])). thf(1,conjecture,((? [A:$i]: (nec @ A))),file('/tmp/xc.p',conclusion)). thf(2,negated_conjecture,((~ (? [A:$i]: (nec @ A)))),inference(neg_conjecture,[status(cth)],[1])). thf(8,plain,((~ (? [A:$i]: ((ex @ A) & (ess @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(9,plain,(! [A:$i] : ((~ (ex @ A)) | (~ (ess @ A)))),inference(cnf,[status(esa)],[8])). thf(28,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ a) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[21,9])). thf(29,plain,((~ (ess @ a))),inference(pattern_uni,[status(thm)],[28:[bind(A, $thf(a))]])). thf(36,plain,(($false) | (gives @ (sk1 @ a) @ a)),inference(rewrite,[status(thm)],[33,29])). thf(37,plain,((gives @ (sk1 @ a) @ a)),inference(simp,[status(thm)],[36])). thf(5,axiom,((! [A:$i,B:$i]: (((agg @ A) & (gives @ B @ A)) => (nec @ B)))),file('/tmp/xc.p',step11)). thf(17,plain,((! [A:$i,B:$i]: (((agg @ A) & (gives @ B @ A)) => ((ex @ B) & (ess @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])). thf(19,plain,(! [B:$i,A:$i] : ((~ (agg @ A)) | (~ (gives @ B @ A)) | (ess @ B))),inference(cnf,[status(esa)],[17])). thf(74,plain,(! [B:$i,A:$i] : ((~ (agg @ A)) | (ess @ B) | ((gives @ (sk1 @ a) @ a) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[37,19])). thf(75,plain,((~ (agg @ a)) | (ess @ (sk1 @ a))),inference(pattern_uni,[status(thm)],[74:[bind(A, $thf(a)),bind(B, $thf(sk1 @ a))]])). thf(22,plain,((agg @ a)),inference(cnf,[status(esa)],[20])). thf(18,plain,(! [B:$i,A:$i] : ((~ (agg @ A)) | (~ (gives @ B @ A)) | (ex @ B))),inference(cnf,[status(esa)],[17])). thf(44,plain,(! [B:$i,A:$i] : ((~ (agg @ A)) | (ex @ B) | ((gives @ (sk1 @ a) @ a) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[37,18])). thf(45,plain,((~ (agg @ a)) | (ex @ (sk1 @ a))),inference(pattern_uni,[status(thm)],[44:[bind(A, $thf(a)),bind(B, $thf(sk1 @ a))]])). thf(56,plain,(~ (($true)) | (ex @ (sk1 @ a))),inference(rewrite,[status(thm)],[45,22])). thf(57,plain,((ex @ (sk1 @ a))),inference(simp,[status(thm)],[56])). thf(58,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ (sk1 @ a)) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[57,9])). thf(59,plain,((~ (ess @ (sk1 @ a)))),inference(pattern_uni,[status(thm)],[58:[bind(A, $thf(sk1 @ a))]])). thf(94,plain,(~ (($true)) | ($false)),inference(rewrite,[status(thm)],[75,22,59])). thf(95,plain,(($false)),inference(simp,[status(thm)],[94])). % SZS output end Refutation for /tmp/xc.p =================== imkan_a_2b_only_aggregate_case.p % [INFO] Parsing problem /tmp/xc.p ... % [INFO] Parsing done (184ms). % [INFO] Running in sequential loop mode. % [INFO] Scanning for conjecture ... % [INFO] Found a conjecture (or negated_conjecture) and 10 axioms. Running axiom selection ... % [INFO] Axiom selection finished. Selected 10 axioms (removed 0 axioms). % [INFO] Problem is higher-order (TPTP THF). % [INFO] Type checking passed. % [CONFIG] Using configuration: timeout(50) with strategy. Searching for refutation ... % Time passed: 3170ms (effective reasoning time: 2661ms) % Solved by strategy % Axioms used in derivation (6): case_only, step4, case_possible, mp012, step3, case_agg % No. of inferences in proof: 56 % SZS status Theorem for /tmp/xc.p : 3170 ms resp. 2661 ms w/o parsing % SZS output start Refutation for /tmp/xc.p thf(ex_type, type, ex: ($i > $o)). thf(ess_type, type, ess: ($i > $o)). thf(gives_type, type, gives: ($i > ($i > $o))). thf(nec_type, type, nec: ($i > $o)). thf(poss_type, type, poss: ($i > $o)). thf(through_another_type, type, through_another: ($i > $o)). thf(mem_type, type, mem: ($i > ($i > $o))). thf(agg_type, type, agg: ($i > $o)). thf(a_type, type, a: $i). thf(p_type, type, p: $i). thf(sk1_type, type, sk1: ($i > $i)). thf(nec_def, definition, (nec = (^ [A:$i]: ((ex @ A) & (ess @ A))))). thf(poss_def, definition, (poss = (^ [A:$i]: ((ex @ A) & ~ (ess @ A))))). thf(through_another_def, definition, (through_another = (^ [A:$i]: ? [B:$i]: (gives @ B @ A)))). thf(agg_def, definition, (agg = (^ [A:$i]: (! [B:$i]: ((B != A) => ((mem @ B @ A) = (poss @ B))) & ~ (mem @ A @ A))))). thf(10,axiom,(((agg @ a) & (ex @ a))),file('/tmp/xc.p',case_agg)). thf(52,plain,((! [A:$i]: ((~ (A = a)) => ((mem @ A @ a) = ((ex @ A) & ~ (ess @ A)))) & ~ (mem @ a @ a) & (ex @ a))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])). thf(53,plain,((ex @ a)),inference(cnf,[status(esa)],[52])). thf(4,axiom,((! [A:$i]: ((poss @ A) => (through_another @ A)))),file('/tmp/xc.p',step3)). thf(21,plain,((! [A:$i]: (((ex @ A) & ~ (ess @ A)) => (? [B:$i]: (gives @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])). thf(22,plain,(! [A:$i] : ((~ (ex @ A)) | (ess @ A) | (gives @ (sk1 @ A) @ A))),inference(cnf,[status(esa)],[21])). thf(105,plain,(! [A:$i] : ((ess @ A) | (gives @ (sk1 @ A) @ A) | ((ex @ a) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[53,22])). thf(106,plain,((ess @ a) | (gives @ (sk1 @ a) @ a)),inference(pattern_uni,[status(thm)],[105:[bind(A, $thf(a))]])). thf(1,conjecture,((? [A:$i]: (nec @ A))),file('/tmp/xc.p',conclusion)). thf(2,negated_conjecture,((~ (? [A:$i]: (nec @ A)))),inference(neg_conjecture,[status(cth)],[1])). thf(13,plain,((~ (? [A:$i]: ((ex @ A) & (ess @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(14,plain,(! [A:$i] : ((~ (ex @ A)) | (~ (ess @ A)))),inference(cnf,[status(esa)],[13])). thf(64,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ a) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[53,14])). thf(65,plain,((~ (ess @ a))),inference(pattern_uni,[status(thm)],[64:[bind(A, $thf(a))]])). thf(112,plain,(($false) | (gives @ (sk1 @ a) @ a)),inference(rewrite,[status(thm)],[106,65])). thf(113,plain,((gives @ (sk1 @ a) @ a)),inference(simp,[status(thm)],[112])). thf(9,axiom,((! [A:$i,B:$i]: ((gives @ A @ B) => (ex @ A)))),file('/tmp/xc.p',mp012)). thf(49,plain,((! [A:$i,B:$i]: ((gives @ A @ B) => (ex @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])). thf(50,plain,((! [A:$i]: ((? [B:$i]: (gives @ A @ B)) => (ex @ A)))),inference(miniscope,[status(thm)],[49])). thf(51,plain,(! [B:$i,A:$i] : ((~ (gives @ A @ B)) | (ex @ A))),inference(cnf,[status(esa)],[50])). thf(521,plain,(! [B:$i,A:$i] : ((ex @ A) | ((gives @ (sk1 @ a) @ a) != (gives @ A @ B)))),inference(paramod_ordered,[status(thm)],[113,51])). thf(522,plain,((ex @ (sk1 @ a))),inference(pattern_uni,[status(thm)],[521:[bind(A, $thf(sk1 @ a)),bind(B, $thf(a))]])). thf(538,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ (sk1 @ a)) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[522,14])). thf(539,plain,((~ (ess @ (sk1 @ a)))),inference(pattern_uni,[status(thm)],[538:[bind(A, $thf(sk1 @ a))]])). thf(11,axiom,((poss @ p)),file('/tmp/xc.p',case_possible)). thf(57,plain,(((ex @ p) & ~ (ess @ p))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])). thf(59,plain,((ex @ p)),inference(cnf,[status(esa)],[57])). thf(107,plain,(! [A:$i] : ((ess @ A) | (gives @ (sk1 @ A) @ A) | ((ex @ p) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[59,22])). thf(108,plain,((ess @ p) | (gives @ (sk1 @ p) @ p)),inference(pattern_uni,[status(thm)],[107:[bind(A, $thf(p))]])). thf(58,plain,((~ (ess @ p))),inference(cnf,[status(esa)],[57])). thf(156,plain,(($false) | (gives @ (sk1 @ p) @ p)),inference(rewrite,[status(thm)],[108,58])). thf(157,plain,((gives @ (sk1 @ p) @ p)),inference(simp,[status(thm)],[156])). thf(525,plain,(! [B:$i,A:$i] : ((ex @ A) | ((gives @ (sk1 @ p) @ p) != (gives @ A @ B)))),inference(paramod_ordered,[status(thm)],[157,51])). thf(526,plain,((ex @ (sk1 @ p))),inference(pattern_uni,[status(thm)],[525:[bind(A, $thf(sk1 @ p)),bind(B, $thf(p))]])). thf(12,axiom,((~ (? [A:$i]: ((A != a) & (poss @ A))))),file('/tmp/xc.p',case_only)). thf(60,plain,((~ (? [A:$i]: (~ (A = a) & (ex @ A) & ~ (ess @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])). thf(61,plain,((~ (? [A:$i]: (~ (A = a) & (ex @ A) & ~ (ess @ A))))),inference(polarity_switch,[status(thm)],[60])). thf(62,plain,(! [A:$i] : ((A = a) | (~ (ex @ A)) | (ess @ A))),inference(cnf,[status(esa)],[61])). thf(63,plain,(! [A:$i] : ((A = a) | (~ (ex @ A)) | (ess @ A))),inference(lifteq,[status(thm)],[62])). thf(1269,plain,(! [A:$i] : ((A = a) | (ess @ A) | ((ex @ (sk1 @ p)) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[526,63])). thf(1270,plain,(((sk1 @ p) = a) | (ess @ (sk1 @ p))),inference(pattern_uni,[status(thm)],[1269:[bind(A, $thf(sk1 @ p))]])). thf(1291,plain,(! [A:$i] : ((A = a) | (~ (ex @ A)) | ((ess @ A) != (ess @ p)))),inference(paramod_ordered,[status(thm)],[63,58])). thf(1292,plain,((p = a) | (~ (ex @ p))),inference(pattern_uni,[status(thm)],[1291:[bind(A, $thf(p))]])). thf(1591,plain,((p = a) | ~ (($true))),inference(rewrite,[status(thm)],[1292,59])). thf(1592,plain,((p = a)),inference(simp,[status(thm)],[1591])). thf(1643,plain,(((sk1 @ a) = a) | (ess @ (sk1 @ a))),inference(rewrite,[status(thm)],[1270,1592])). thf(5,axiom,((! [A:$i]: ~ (gives @ A @ A))),file('/tmp/xc.p',step4)). thf(23,plain,((! [A:$i]: ~ (gives @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])). thf(24,plain,((~ (? [A:$i]: (gives @ A @ A)))),inference(miniscope,[status(thm)],[23])). thf(25,plain,(! [A:$i] : ((~ (gives @ A @ A)))),inference(cnf,[status(esa)],[24])). thf(124,plain,(! [A:$i] : (((gives @ (sk1 @ a) @ a) != (gives @ A @ A)))),inference(paramod_ordered,[status(thm)],[113,25])). thf(125,plain,(! [A:$i] : (((sk1 @ a) != A) | (a != A))),inference(simp,[status(thm)],[124])). thf(126,plain,(((sk1 @ a) != a)),inference(simp,[status(thm)],[125])). thf(1644,plain,((ess @ (sk1 @ a))),inference(simplifyReflect,[status(thm)],[1643,126])). thf(1645,plain,(~ (($true))),inference(rewrite,[status(thm)],[539,1644])). thf(1646,plain,(($false)),inference(simp,[status(thm)],[1645])). % SZS output end Refutation for /tmp/xc.p =================== imkan_a_assembly_abstract.p % [INFO] Parsing problem /tmp/xc.p ... % [INFO] Parsing done (125ms). % [INFO] Running in sequential loop mode. % [INFO] Scanning for conjecture ... % [INFO] Found a conjecture (or negated_conjecture) and 8 axioms. Running axiom selection ... % [INFO] Axiom selection finished. Selected 8 axioms (removed 0 axioms). % [INFO] Problem is higher-order (TPTP THF). % [INFO] Type checking passed. % [CONFIG] Using configuration: timeout(50) with strategy. Searching for refutation ... % Time passed: 1572ms (effective reasoning time: 1137ms) % Solved by strategy % Axioms used in derivation (5): sp001, step11, mp012, mp009, step3 % No. of inferences in proof: 49 % SZS status Theorem for /tmp/xc.p : 1572 ms resp. 1137 ms w/o parsing % SZS output start Refutation for /tmp/xc.p thf(ex_type, type, ex: ($i > $o)). thf(ess_type, type, ess: ($i > $o)). thf(gives_type, type, gives: ($i > ($i > $o))). thf(nec_type, type, nec: ($i > $o)). thf(poss_type, type, poss: ($i > $o)). thf(through_another_type, type, through_another: ($i > $o)). thf(agg_type, type, agg: ($i > $o)). thf(sk1_type, type, sk1: ($i > $i)). thf(sk2_type, type, sk2: $i). thf(sk3_type, type, sk3: $i). thf(nec_def, definition, (nec = (^ [A:$i]: ((ex @ A) & (ess @ A))))). thf(poss_def, definition, (poss = (^ [A:$i]: ((ex @ A) & ~ (ess @ A))))). thf(through_another_def, definition, (through_another = (^ [A:$i]: ? [B:$i]: (gives @ B @ A)))). thf(6,axiom,(((? [A:$i]: (poss @ A)) => (? [A:$i]: ((agg @ A) & (ex @ A))))),file('/tmp/xc.p',mp009)). thf(24,plain,(((? [A:$i]: ((ex @ A) & ~ (ess @ A))) => (? [A:$i]: ((agg @ A) & (ex @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])). thf(26,plain,(! [A:$i] : ((~ (ex @ A)) | (ess @ A) | (ex @ sk2))),inference(cnf,[status(esa)],[24])). thf(10,axiom,((? [A:$i]: (ex @ A))),file('/tmp/xc.p',sp001)). thf(38,plain,((? [A:$i]: (ex @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])). thf(39,plain,((ex @ sk3)),inference(cnf,[status(esa)],[38])). thf(1,conjecture,((? [A:$i]: (nec @ A))),file('/tmp/xc.p',conclusion)). thf(2,negated_conjecture,((~ (? [A:$i]: (nec @ A)))),inference(neg_conjecture,[status(cth)],[1])). thf(11,plain,((~ (? [A:$i]: ((ex @ A) & (ess @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(12,plain,(! [A:$i] : ((~ (ex @ A)) | (~ (ess @ A)))),inference(cnf,[status(esa)],[11])). thf(40,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ sk3) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[39,12])). thf(41,plain,((~ (ess @ sk3))),inference(pattern_uni,[status(thm)],[40:[bind(A, $thf(sk3))]])). thf(123,plain,(! [A:$i] : ((~ (ex @ A)) | (ex @ sk2) | ((ess @ A) != (ess @ sk3)))),inference(paramod_ordered,[status(thm)],[26,41])). thf(124,plain,((~ (ex @ sk3)) | (ex @ sk2)),inference(pattern_uni,[status(thm)],[123:[bind(A, $thf(sk3))]])). thf(134,plain,(~ (($true)) | (ex @ sk2)),inference(rewrite,[status(thm)],[124,39])). thf(135,plain,((ex @ sk2)),inference(simp,[status(thm)],[134])). thf(4,axiom,((! [A:$i]: ((poss @ A) => (through_another @ A)))),file('/tmp/xc.p',step3)). thf(19,plain,((! [A:$i]: (((ex @ A) & ~ (ess @ A)) => (? [B:$i]: (gives @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])). thf(20,plain,(! [A:$i] : ((~ (ex @ A)) | (ess @ A) | (gives @ (sk1 @ A) @ A))),inference(cnf,[status(esa)],[19])). thf(136,plain,(! [A:$i] : ((ess @ A) | (gives @ (sk1 @ A) @ A) | ((ex @ sk2) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[135,20])). thf(137,plain,((ess @ sk2) | (gives @ (sk1 @ sk2) @ sk2)),inference(pattern_uni,[status(thm)],[136:[bind(A, $thf(sk2))]])). thf(138,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ sk2) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[135,12])). thf(139,plain,((~ (ess @ sk2))),inference(pattern_uni,[status(thm)],[138:[bind(A, $thf(sk2))]])). thf(156,plain,(($false) | (gives @ (sk1 @ sk2) @ sk2)),inference(rewrite,[status(thm)],[137,139])). thf(157,plain,((gives @ (sk1 @ sk2) @ sk2)),inference(simp,[status(thm)],[156])). thf(9,axiom,((! [A:$i,B:$i]: ((gives @ A @ B) => (ex @ A)))),file('/tmp/xc.p',mp012)). thf(35,plain,((! [A:$i,B:$i]: ((gives @ A @ B) => (ex @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])). thf(36,plain,((! [A:$i]: ((? [B:$i]: (gives @ A @ B)) => (ex @ A)))),inference(miniscope,[status(thm)],[35])). thf(37,plain,(! [B:$i,A:$i] : ((~ (gives @ A @ B)) | (ex @ A))),inference(cnf,[status(esa)],[36])). thf(182,plain,(! [B:$i,A:$i] : ((ex @ A) | ((gives @ (sk1 @ sk2) @ sk2) != (gives @ A @ B)))),inference(paramod_ordered,[status(thm)],[157,37])). thf(183,plain,((ex @ (sk1 @ sk2))),inference(pattern_uni,[status(thm)],[182:[bind(A, $thf(sk1 @ sk2)),bind(B, $thf(sk2))]])). thf(25,plain,(! [A:$i] : ((~ (ex @ A)) | (ess @ A) | (agg @ sk2))),inference(cnf,[status(esa)],[24])). thf(47,plain,(! [B:$i,A:$i] : ((~ (ex @ A)) | (agg @ sk2) | (~ (ex @ B)) | ((ess @ A) != (ess @ B)))),inference(paramod_ordered,[status(thm)],[25,12])). thf(48,plain,(! [A:$i] : ((~ (ex @ A)) | (agg @ sk2) | (~ (ex @ A)))),inference(pattern_uni,[status(thm)],[47:[bind(A, $thf(A)),bind(B, $thf(A))]])). thf(51,plain,(! [A:$i] : ((~ (ex @ A)) | (agg @ sk2))),inference(simp,[status(thm)],[48])). thf(58,plain,(! [A:$i] : ((agg @ sk2) | ((ex @ sk3) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[39,51])). thf(59,plain,((agg @ sk2)),inference(pattern_uni,[status(thm)],[58:[bind(A, $thf(sk3))]])). thf(8,axiom,((! [A:$i,B:$i]: (((agg @ A) & (gives @ B @ A)) => (nec @ B)))),file('/tmp/xc.p',step11)). thf(32,plain,((! [A:$i,B:$i]: (((agg @ A) & (gives @ B @ A)) => ((ex @ B) & (ess @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])). thf(34,plain,(! [B:$i,A:$i] : ((~ (agg @ A)) | (~ (gives @ B @ A)) | (ess @ B))),inference(cnf,[status(esa)],[32])). thf(64,plain,(! [B:$i,A:$i] : ((~ (gives @ B @ A)) | (ess @ B) | ((agg @ sk2) != (agg @ A)))),inference(paramod_ordered,[status(thm)],[59,34])). thf(65,plain,(! [A:$i] : ((~ (gives @ A @ sk2)) | (ess @ A))),inference(pattern_uni,[status(thm)],[64:[bind(A, $thf(sk2))]])). thf(66,plain,(! [A:$i] : ((~ (gives @ A @ sk2)) | (ess @ A))),inference(simp,[status(thm)],[65])). thf(162,plain,(! [A:$i] : ((ess @ A) | ((gives @ (sk1 @ sk2) @ sk2) != (gives @ A @ sk2)))),inference(paramod_ordered,[status(thm)],[157,66])). thf(163,plain,((ess @ (sk1 @ sk2))),inference(pattern_uni,[status(thm)],[162:[bind(A, $thf(sk1 @ sk2))]])). thf(168,plain,(! [A:$i] : ((~ (ex @ A)) | ((ess @ (sk1 @ sk2)) != (ess @ A)))),inference(paramod_ordered,[status(thm)],[163,12])). thf(169,plain,((~ (ex @ (sk1 @ sk2)))),inference(pattern_uni,[status(thm)],[168:[bind(A, $thf(sk1 @ sk2))]])). thf(189,plain,(($false)),inference(rewrite,[status(thm)],[183,169])). thf(190,plain,(($false)),inference(simp,[status(thm)],[189])). % SZS output end Refutation for /tmp/xc.p =================== imkan_a_assembly.p % [INFO] Parsing problem /tmp/xc.p ... % [INFO] Parsing done (116ms). % [INFO] Running in sequential loop mode. % [INFO] Scanning for conjecture ... % [INFO] Found a conjecture (or negated_conjecture) and 8 axioms. Running axiom selection ... % [INFO] Axiom selection finished. Selected 8 axioms (removed 0 axioms). % [INFO] Problem is higher-order (TPTP THF). % [INFO] Type checking passed. % [CONFIG] Using configuration: timeout(50) with strategy. Searching for refutation ... % Time passed: 50803ms (effective reasoning time: 50359ms) % SZS status Timeout for /tmp/xc.p : 50803 ms resp. 50359 ms w/o parsing =================== imkan_b_short.p % [INFO] Parsing problem /tmp/xc.p ... % [INFO] Parsing done (148ms). % [INFO] Running in sequential loop mode. % [INFO] Scanning for conjecture ... % [INFO] Found a conjecture (or negated_conjecture) and 3 axioms. Running axiom selection ... % [INFO] Axiom selection finished. Selected 3 axioms (removed 0 axioms). % [INFO] Problem is higher-order (TPTP THF). % [INFO] Type checking passed. % [CONFIG] Using configuration: timeout(50) with strategy. Searching for refutation ... % Time passed: 1513ms (effective reasoning time: 1023ms) % Solved by strategy % Axioms used in derivation (3): sp001, mp008, op001 % No. of inferences in proof: 31 % SZS status Theorem for /tmp/xc.p : 1513 ms resp. 1023 ms w/o parsing % SZS output start Refutation for /tmp/xc.p thf(ex_type, type, ex: ($i > $o)). thf(ess_type, type, ess: ($i > $o)). thf(gives_type, type, gives: ($i > ($i > $o))). thf(nec_type, type, nec: ($i > $o)). thf(through_another_type, type, through_another: ($i > $o)). thf(sk1_type, type, sk1: ($i > $i)). thf(sk2_type, type, sk2: $i). thf(nec_def, definition, (nec = (^ [A:$i]: ((ex @ A) & (ess @ A))))). thf(through_another_def, definition, (through_another = (^ [A:$i]: ? [B:$i]: (gives @ B @ A)))). thf(5,axiom,((? [A:$i]: (ex @ A))),file('/tmp/xc.p',sp001)). thf(13,plain,((? [A:$i]: (ex @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])). thf(14,plain,((ex @ sk2)),inference(cnf,[status(esa)],[13])). thf(4,axiom,((! [A:$i]: (((ex @ A) & ~ (through_another @ A)) => (ess @ A)))),file('/tmp/xc.p',mp008)). thf(11,plain,((! [A:$i]: (((ex @ A) & ~ (? [B:$i]: (gives @ B @ A))) => (ess @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])). thf(12,plain,(! [A:$i] : ((~ (ex @ A)) | (gives @ (sk1 @ A) @ A) | (ess @ A))),inference(cnf,[status(esa)],[11])). thf(24,plain,(! [A:$i] : ((gives @ (sk1 @ A) @ A) | (ess @ A) | ((ex @ sk2) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[14,12])). thf(25,plain,((gives @ (sk1 @ sk2) @ sk2) | (ess @ sk2)),inference(pattern_uni,[status(thm)],[24:[bind(A, $thf(sk2))]])). thf(1,conjecture,((? [A:$i]: (nec @ A))),file('/tmp/xc.p',conclusion)). thf(2,negated_conjecture,((~ (? [A:$i]: (nec @ A)))),inference(neg_conjecture,[status(cth)],[1])). thf(6,plain,((~ (? [A:$i]: ((ex @ A) & (ess @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(7,plain,(! [A:$i] : ((~ (ex @ A)) | (~ (ess @ A)))),inference(cnf,[status(esa)],[6])). thf(15,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ sk2) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[14,7])). thf(16,plain,((~ (ess @ sk2))),inference(pattern_uni,[status(thm)],[15:[bind(A, $thf(sk2))]])). thf(34,plain,((gives @ (sk1 @ sk2) @ sk2) | ($false)),inference(rewrite,[status(thm)],[25,16])). thf(35,plain,((gives @ (sk1 @ sk2) @ sk2)),inference(simp,[status(thm)],[34])). thf(3,axiom,((! [A:$i,B:$i]: ((gives @ B @ A) => ((ex @ B) & ~ (through_another @ B))))),file('/tmp/xc.p',op001)). thf(8,plain,((! [A:$i,B:$i]: ((gives @ B @ A) => ((ex @ B) & ~ (? [C:$i]: (gives @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])). thf(9,plain,(! [B:$i,A:$i] : ((~ (gives @ B @ A)) | (ex @ B))),inference(cnf,[status(esa)],[8])). thf(40,plain,(! [B:$i,A:$i] : ((ex @ B) | ((gives @ (sk1 @ sk2) @ sk2) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[35,9])). thf(41,plain,((ex @ (sk1 @ sk2))),inference(pattern_uni,[status(thm)],[40:[bind(A, $thf(sk2)),bind(B, $thf(sk1 @ sk2))]])). thf(46,plain,(! [A:$i] : ((gives @ (sk1 @ A) @ A) | (ess @ A) | ((ex @ (sk1 @ sk2)) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[41,12])). thf(47,plain,((gives @ (sk1 @ (sk1 @ sk2)) @ (sk1 @ sk2)) | (ess @ (sk1 @ sk2))),inference(pattern_uni,[status(thm)],[46:[bind(A, $thf(sk1 @ sk2))]])). thf(48,plain,(! [A:$i] : ((~ (ess @ A)) | ((ex @ (sk1 @ sk2)) != (ex @ A)))),inference(paramod_ordered,[status(thm)],[41,7])). thf(49,plain,((~ (ess @ (sk1 @ sk2)))),inference(pattern_uni,[status(thm)],[48:[bind(A, $thf(sk1 @ sk2))]])). thf(10,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ B @ A)) | (~ (gives @ C @ B)))),inference(cnf,[status(esa)],[8])). thf(36,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ C @ B)) | ((gives @ (sk1 @ sk2) @ sk2) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[35,10])). thf(37,plain,(! [A:$i] : ((~ (gives @ A @ (sk1 @ sk2))))),inference(pattern_uni,[status(thm)],[36:[bind(A, $thf(sk2)),bind(B, $thf(sk1 @ sk2)),bind(C, $thf(C))]])). thf(44,plain,(! [A:$i] : ((~ (gives @ A @ (sk1 @ sk2))))),inference(simp,[status(thm)],[37])). thf(75,plain,(($false) | ($false)),inference(rewrite,[status(thm)],[47,49,44])). thf(76,plain,(($false)),inference(simp,[status(thm)],[75])). % SZS output end Refutation for /tmp/xc.p checked: 2026-09-30