Leo-III run on the at.alkalam.org runner container (alkalam-prover-runner) $ java -jar /opt/leo3.jar --version Leo-III 1.7.18 command per file: java -Xmx1024m -jar /opt/leo3.jar -t 50 -p (the workbench's own settings) $ shasum -a 256 *.p 1924d6b33250d95cfe96515e6e455a9430ab7565544e421f075d2146c7cc9026 assembly.p 6e0a3d5b6beb90a22975a6a4c8e5207f4d787b8467fffcf1007f4f7f98db9168 direct.p 13aa6176b9e94e2cc3f0de235df3a66f0f673e90778a99008b323017ac061def p1_exhaustive.p 8aec076da7c9def6befd191bbd1178759e8adb2415619a3b4f1ec6333e5a03d2 p2_no_self_creation.p 8bba28e34dd75d14780d3aba84768afecd3164f8d1c759ae201bddb2f62caeae p3_no_circle.p ea465e466e0c59058ef98260a60e8cdc8e955f11e6d810c7ffddbbfd8ac4eb5c p4_no_regress.p =================== p1_exhaustive.p % [INFO] Parsing problem /tmp/kal_p1_exhaustive.p ... % [INFO] Parsing done (136ms). % [INFO] Running in sequential loop mode. % [INFO] Scanning for conjecture ... % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ... % [INFO] Axiom selection finished. Selected 0 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: 50404ms (effective reasoning time: 49918ms) % SZS status Timeout for /tmp/kal_p1_exhaustive.p : 50404 ms resp. 49918 ms w/o parsing =================== p2_no_self_creation.p % [INFO] Parsing problem /tmp/kal_p2_no_self_creation.p ... % [INFO] Parsing done (146ms). % [INFO] Running in sequential loop mode. % [INFO] Scanning for conjecture ... % [INFO] Found a conjecture (or negated_conjecture) and 2 axioms. Running axiom selection ... % [INFO] Axiom selection finished. Selected 2 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: 1288ms (effective reasoning time: 790ms) % Solved by strategy % Axioms used in derivation (2): mp002, mp001 % No. of inferences in proof: 17 % SZS status Theorem for /tmp/kal_p2_no_self_creation.p : 1288 ms resp. 790 ms w/o parsing % SZS output start Refutation for /tmp/kal_p2_no_self_creation.p thf(gives_type, type, gives: ($i > ($i > $o))). thf(through_type, type, through: ($i > ($i > $o))). thf(sk1_type, type, sk1: $i). thf(4,axiom,((! [A:$i,B:$i]: ((gives @ B @ A) => (through @ A @ B)))),file('/tmp/kal_p2_no_self_creation.p',mp002)). thf(10,plain,((! [A:$i,B:$i]: ((gives @ B @ A) => (through @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])). thf(11,plain,(! [B:$i,A:$i] : ((~ (gives @ B @ A)) | (through @ A @ B))),inference(cnf,[status(esa)],[10])). thf(1,conjecture,((! [A:$i]: ~ (gives @ A @ A))),file('/tmp/kal_p2_no_self_creation.p',premise2)). thf(2,negated_conjecture,((~ (! [A:$i]: ~ (gives @ A @ A)))),inference(neg_conjecture,[status(cth)],[1])). thf(5,plain,((~ (! [A:$i]: ~ (gives @ A @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(6,plain,((~ (~ (? [A:$i]: (gives @ A @ A))))),inference(miniscope,[status(thm)],[5])). thf(7,plain,((gives @ sk1 @ sk1)),inference(cnf,[status(esa)],[6])). thf(3,axiom,((! [A:$i,B:$i]: ((gives @ B @ A) => (~ (through @ B @ A))))),file('/tmp/kal_p2_no_self_creation.p',mp001)). thf(8,plain,((! [A:$i,B:$i]: ((gives @ B @ A) => (~ (through @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])). thf(9,plain,(! [B:$i,A:$i] : ((~ (gives @ B @ A)) | (~ (through @ B @ A)))),inference(cnf,[status(esa)],[8])). thf(12,plain,(! [B:$i,A:$i] : ((~ (through @ B @ A)) | ((gives @ sk1 @ sk1) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[7,9])). thf(13,plain,((~ (through @ sk1 @ sk1))),inference(pattern_uni,[status(thm)],[12:[bind(A, $thf(sk1)),bind(B, $thf(sk1))]])). thf(18,plain,(! [B:$i,A:$i] : ((~ (gives @ B @ A)) | ((through @ A @ B) != (through @ sk1 @ sk1)))),inference(paramod_ordered,[status(thm)],[11,13])). thf(19,plain,((~ (gives @ sk1 @ sk1))),inference(pattern_uni,[status(thm)],[18:[bind(A, $thf(sk1)),bind(B, $thf(sk1))]])). thf(20,plain,(~ (($true))),inference(rewrite,[status(thm)],[19,7])). thf(21,plain,(($false)),inference(simp,[status(thm)],[20])). % SZS output end Refutation for /tmp/kal_p2_no_self_creation.p =================== p3_no_circle.p % [INFO] Parsing problem /tmp/kal_p3_no_circle.p ... % [INFO] Parsing done (132ms). % [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 ... % SZS status Forced for /tmp/kal_p3_no_circle.p : Leo-III stopped externally. =================== p4_no_regress.p % [INFO] Parsing problem /tmp/kal_p4_no_regress.p ... % [INFO] Parsing done (156ms). % [INFO] Running in sequential loop mode. % [INFO] Scanning for conjecture ... % [INFO] Found a conjecture (or negated_conjecture) and 1 axioms. Running axiom selection ... % [INFO] Axiom selection finished. Selected 1 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: 1352ms (effective reasoning time: 791ms) % Solved by strategy % Axioms used in derivation (1): op001 % No. of inferences in proof: 13 % SZS status Theorem for /tmp/kal_p4_no_regress.p : 1352 ms resp. 791 ms w/o parsing % SZS output start Refutation for /tmp/kal_p4_no_regress.p thf(gives_type, type, gives: ($i > ($i > $o))). thf(ex_type, type, ex: ($i > $o)). thf(through_another_type, type, through_another: ($i > $o)). thf(of_itself_type, type, of_itself: ($i > $o)). thf(sk1_type, type, sk1: $i). thf(sk2_type, type, sk2: $i). thf(sk3_type, type, sk3: $i). thf(of_itself_def, definition, (of_itself = (^ [A:$i]: ((ex @ A) & ~ (through_another @ A))))). thf(1,conjecture,((! [A:$i,B:$i,C:$i]: ((gives @ B @ A) => (~ (gives @ C @ B))))),file('/tmp/kal_p4_no_regress.p',premise4)). thf(2,negated_conjecture,((~ (! [A:$i,B:$i,C:$i]: ((gives @ B @ A) => (~ (gives @ C @ B)))))),inference(neg_conjecture,[status(cth)],[1])). thf(4,plain,((~ (! [A:$i,B:$i,C:$i]: ((gives @ B @ A) => (~ (gives @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(5,plain,((~ (! [A:$i,B:$i]: ((gives @ B @ A) => (~ (? [C:$i]: (gives @ C @ B))))))),inference(miniscope,[status(thm)],[4])). thf(7,plain,((gives @ sk2 @ sk1)),inference(cnf,[status(esa)],[5])). thf(6,plain,((gives @ sk3 @ sk2)),inference(cnf,[status(esa)],[5])). thf(3,axiom,((! [A:$i,B:$i]: ((gives @ B @ A) => (of_itself @ B)))),file('/tmp/kal_p4_no_regress.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(10,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ B @ A)) | (~ (gives @ C @ B)))),inference(cnf,[status(esa)],[8])). thf(17,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ B @ A)) | ((gives @ sk3 @ sk2) != (gives @ C @ B)))),inference(paramod_ordered,[status(thm)],[6,10])). thf(18,plain,(! [A:$i] : ((~ (gives @ sk2 @ A)))),inference(pattern_uni,[status(thm)],[17:[bind(A, $thf(A)),bind(B, $thf(sk2)),bind(C, $thf(sk3))]])). thf(28,plain,(($false)),inference(rewrite,[status(thm)],[7,18])). thf(29,plain,(($false)),inference(simp,[status(thm)],[28])). % SZS output end Refutation for /tmp/kal_p4_no_regress.p =================== assembly.p % [INFO] Parsing problem /tmp/kal_assembly.p ... % [INFO] Parsing done (186ms). % [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: 1991ms (effective reasoning time: 1385ms) % Solved by strategy % Axioms used in derivation (2): antecedent, premise4 % No. of inferences in proof: 23 % SZS status Theorem for /tmp/kal_assembly.p : 1991 ms resp. 1385 ms w/o parsing % SZS output start Refutation for /tmp/kal_assembly.p thf(gives_type, type, gives: ($i > ($i > $o))). thf(u_type, type, u: $i). thf(dep_type, type, dep: ($i > ($i > $o))). thf(independent_type, type, independent: ($i > $o)). thf(reach_type, type, reach: ($i > ($i > $o))). thf(through_another_type, type, through_another: ($i > $o)). thf(sk1_type, type, sk1: ($i > ($i > ($i > $o)))). thf(sk2_type, type, sk2: ($i > $i)). thf(sk32_type, type, sk32: $i). thf(independent_def, definition, (independent = (^ [A:$i]: ! [B:$i]: ~ (dep @ A @ B)))). thf(reach_def, definition, (reach = (^ [A:$i,B:$i]: ! [C:($i > ($i > $o))]: ((! [D:$i,E:$i]: ((dep @ D @ E) => (C @ D @ E)) & ! [D:$i,E:$i,F:$i]: (((C @ D @ E) & (C @ E @ F)) => (C @ D @ F))) => (C @ A @ B))))). thf(through_another_def, definition, (through_another = (^ [A:$i]: ? [B:$i]: (gives @ B @ A)))). thf(1,conjecture,((? [A:$i]: ((reach @ u @ A) & (independent @ A)))),file('/tmp/kal_assembly.p',conclusion)). thf(2,negated_conjecture,((~ (? [A:$i]: ((reach @ u @ A) & (independent @ A))))),inference(neg_conjecture,[status(cth)],[1])). thf(8,plain,((~ (? [A:$i]: (! [B:($i > ($i > $o))]: ((! [C:$i,D:$i]: ((gives @ D @ C) => (B @ C @ D)) & ! [C:$i,D:$i,E:$i]: (((B @ C @ D) & (B @ D @ E)) => (B @ C @ E))) => (B @ u @ A)) & ! [B:$i]: ~ (gives @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(9,plain,((~ (? [A:$i]: (! [B:($i > ($i > $o))]: ((! [C:$i,D:$i]: ((gives @ D @ C) => (B @ C @ D)) & ! [C:$i,D:$i,E:$i]: (((B @ C @ D) & (B @ D @ E)) => (B @ C @ E))) => (B @ u @ A)) & ~ (? [B:$i]: (gives @ B @ A)))))),inference(miniscope,[status(thm)],[8])). thf(10,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ C @ B)) | (sk1 @ A @ B @ C) | (gives @ (sk2 @ A) @ A))),inference(cnf,[status(esa)],[9])). thf(12,plain,(! [A:$i] : ((~ (sk1 @ A @ u @ A)) | (gives @ (sk2 @ A) @ A))),inference(cnf,[status(esa)],[9])). thf(111,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (gives @ C @ B)) | (gives @ (sk2 @ A) @ A) | (gives @ (sk2 @ D) @ D) | ((sk1 @ A @ B @ C) != (sk1 @ D @ u @ D)))),inference(paramod_ordered,[status(thm)],[10,12])). thf(112,plain,(! [A:$i] : ((~ (gives @ A @ u)) | (gives @ (sk2 @ A) @ A) | (gives @ (sk2 @ A) @ A))),inference(pattern_uni,[status(thm)],[111:[bind(A, $thf(C)),bind(B, $thf(u)),bind(C, $thf(C)),bind(D, $thf(C))]])). thf(113,plain,(! [A:$i] : ((~ (gives @ A @ u)) | (gives @ (sk2 @ A) @ A))),inference(simp,[status(thm)],[112])). thf(7,axiom,((through_another @ u)),file('/tmp/kal_assembly.p',antecedent)). thf(91,plain,((? [A:$i]: (gives @ A @ u))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])). thf(92,plain,((gives @ sk32 @ u)),inference(cnf,[status(esa)],[91])). thf(6,axiom,((! [A:$i,B:$i,C:$i]: ((gives @ B @ A) => (~ (gives @ C @ B))))),file('/tmp/kal_assembly.p',premise4)). thf(88,plain,((! [A:$i,B:$i,C:$i]: ((gives @ B @ A) => (~ (gives @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])). thf(89,plain,((! [A:$i,B:$i]: ((gives @ B @ A) => (~ (? [C:$i]: (gives @ C @ B)))))),inference(miniscope,[status(thm)],[88])). thf(90,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ B @ A)) | (~ (gives @ C @ B)))),inference(cnf,[status(esa)],[89])). thf(96,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ C @ B)) | ((gives @ sk32 @ u) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[92,90])). thf(97,plain,(! [A:$i] : ((~ (gives @ A @ sk32)))),inference(pattern_uni,[status(thm)],[96:[bind(A, $thf(u)),bind(B, $thf(sk32))]])). thf(102,plain,(! [A:$i] : ((~ (gives @ A @ sk32)))),inference(simp,[status(thm)],[97])). thf(137,plain,(! [B:$i,A:$i] : ((~ (gives @ A @ u)) | ((gives @ (sk2 @ A) @ A) != (gives @ B @ sk32)))),inference(paramod_ordered,[status(thm)],[113,102])). thf(138,plain,((~ (gives @ sk32 @ u))),inference(pattern_uni,[status(thm)],[137:[bind(A, $thf(sk32)),bind(B, $thf(sk2 @ sk32))]])). thf(156,plain,(~ (($true))),inference(rewrite,[status(thm)],[138,92])). thf(157,plain,(($false)),inference(simp,[status(thm)],[156])). % SZS output end Refutation for /tmp/kal_assembly.p =================== direct.p % [INFO] Parsing problem /tmp/kal_direct.p ... % [INFO] Parsing done (162ms). % [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: 1675ms (effective reasoning time: 1139ms) % Solved by strategy % Axioms used in derivation (2): antecedent, op001 % No. of inferences in proof: 24 % SZS status Theorem for /tmp/kal_direct.p : 1675 ms resp. 1139 ms w/o parsing % SZS output start Refutation for /tmp/kal_direct.p thf(gives_type, type, gives: ($i > ($i > $o))). thf(ex_type, type, ex: ($i > $o)). thf(u_type, type, u: $i). thf(dep_type, type, dep: ($i > ($i > $o))). thf(independent_type, type, independent: ($i > $o)). thf(through_another_type, type, through_another: ($i > $o)). thf(of_itself_type, type, of_itself: ($i > $o)). thf(sk1_type, type, sk1: ($i > $i)). thf(sk2_type, type, sk2: ($i > $i)). thf(sk3_type, type, sk3: $i). thf(independent_def, definition, (independent = (^ [A:$i]: ! [B:$i]: ~ (dep @ A @ B)))). thf(through_another_def, definition, (through_another = (^ [A:$i]: ? [B:$i]: (gives @ B @ A)))). thf(of_itself_def, definition, (of_itself = (^ [A:$i]: ((ex @ A) & ~ (through_another @ A))))). thf(7,axiom,((through_another @ u)),file('/tmp/kal_direct.p',antecedent)). thf(21,plain,((? [A:$i]: (gives @ A @ u))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])). thf(22,plain,((gives @ sk3 @ u)),inference(cnf,[status(esa)],[21])). thf(1,conjecture,((? [A:$i]: ((gives @ A @ u) & (ex @ A) & (of_itself @ A) & (independent @ A)))),file('/tmp/kal_direct.p',conclusion)). thf(2,negated_conjecture,((~ (? [A:$i]: ((gives @ A @ u) & (ex @ A) & (of_itself @ A) & (independent @ A))))),inference(neg_conjecture,[status(cth)],[1])). thf(8,plain,((~ (? [A:$i]: ((gives @ A @ u) & (ex @ A) & (ex @ A) & ~ (? [B:$i]: (gives @ B @ A)) & ! [B:$i]: ~ (gives @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(9,plain,((~ (? [A:$i]: ((gives @ A @ u) & (ex @ A) & (ex @ A) & ~ (? [B:$i]: (gives @ B @ A)) & ~ (? [B:$i]: (gives @ B @ A)))))),inference(miniscope,[status(thm)],[8])). thf(10,plain,(! [A:$i] : ((~ (gives @ A @ u)) | (~ (ex @ A)) | (~ (ex @ A)) | (gives @ (sk1 @ A) @ A) | (gives @ (sk2 @ A) @ A))),inference(cnf,[status(esa)],[9])). thf(11,plain,(! [A:$i] : ((~ (gives @ A @ u)) | (~ (ex @ A)) | (gives @ (sk1 @ A) @ A) | (gives @ (sk2 @ A) @ A))),inference(simp,[status(thm)],[10])). thf(49,plain,(! [A:$i] : ((~ (ex @ A)) | (gives @ (sk1 @ A) @ A) | (gives @ (sk2 @ A) @ A) | ((gives @ sk3 @ u) != (gives @ A @ u)))),inference(paramod_ordered,[status(thm)],[22,11])). thf(50,plain,((~ (ex @ sk3)) | (gives @ (sk1 @ sk3) @ sk3) | (gives @ (sk2 @ sk3) @ sk3)),inference(pattern_uni,[status(thm)],[49:[bind(A, $thf(sk3))]])). thf(6,axiom,((! [A:$i,B:$i]: ((gives @ B @ A) => (of_itself @ B)))),file('/tmp/kal_direct.p',op001)). thf(18,plain,((! [A:$i,B:$i]: ((gives @ B @ A) => ((ex @ B) & ~ (? [C:$i]: (gives @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])). thf(19,plain,(! [B:$i,A:$i] : ((~ (gives @ B @ A)) | (ex @ B))),inference(cnf,[status(esa)],[18])). thf(23,plain,(! [B:$i,A:$i] : ((ex @ B) | ((gives @ sk3 @ u) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[22,19])). thf(24,plain,((ex @ sk3)),inference(pattern_uni,[status(thm)],[23:[bind(A, $thf(u)),bind(B, $thf(sk3))]])). thf(66,plain,(~ (($true)) | (gives @ (sk1 @ sk3) @ sk3) | (gives @ (sk2 @ sk3) @ sk3)),inference(rewrite,[status(thm)],[50,24])). thf(67,plain,((gives @ (sk1 @ sk3) @ sk3) | (gives @ (sk2 @ sk3) @ sk3)),inference(simp,[status(thm)],[66])). thf(20,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ B @ A)) | (~ (gives @ C @ B)))),inference(cnf,[status(esa)],[18])). thf(27,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ C @ B)) | ((gives @ sk3 @ u) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[22,20])). thf(28,plain,(! [A:$i] : ((~ (gives @ A @ sk3)))),inference(pattern_uni,[status(thm)],[27:[bind(A, $thf(u)),bind(B, $thf(sk3))]])). thf(34,plain,(! [A:$i] : ((~ (gives @ A @ sk3)))),inference(simp,[status(thm)],[28])). thf(134,plain,(($false) | ($false)),inference(rewrite,[status(thm)],[67,34])). thf(135,plain,(($false)),inference(simp,[status(thm)],[134])). % SZS output end Refutation for /tmp/kal_direct.p note: p3_no_circle ran past its 50 s limit for over 6 minutes and was stopped externally (status Forced). It is recorded as no result, not as a proof or a refutation. checked: 2026-09-29 =================== unconditional_assembly.p (added 2026-09-30, Leo-III Leo-III 1.7.18) bd92683c41719f3619558bc12f772b134acdb253d0c15f0b9920ccce26775947 unconditional_assembly.p % [INFO] Parsing problem /tmp/xc.p ... % [INFO] Parsing done (155ms). % [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: 3831ms (effective reasoning time: 3304ms) % Solved by strategy % Axioms used in derivation (3): pr011, kalima, mp008 % No. of inferences in proof: 53 % SZS status Theorem for /tmp/xc.p : 3831 ms resp. 3304 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(part_type, type, part: ($i > ($i > $o))). thf(u_type, type, u: $i). thf(independent_type, type, independent: ($i > $o)). thf(sk1_type, type, sk1: ($i > ($i > $i))). thf(sk2_type, type, sk2: ($i > $i)). thf(sk3_type, type, sk3: $i). thf(sk4_type, type, sk4: $i). thf(sk5_type, type, sk5: ($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(independent_def, definition, (independent = (^ [A:$i]: ! [B:$i]: ~ (gives @ B @ A)))). thf(4,axiom,((? [A:$i]: (((A = u) | (part @ A @ u)) & (poss @ A) & (through_another @ A)))),file('/tmp/xc.p',pr011)). thf(19,plain,((? [A:$i]: (((A = u) | (part @ A @ u)) & (ex @ A) & ~ (ess @ A) & ? [B:$i]: (gives @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])). thf(20,plain,((gives @ sk4 @ sk3)),inference(cnf,[status(esa)],[19])). thf(3,axiom,((! [A:$i]: ((through_another @ A) => (? [B:$i]: ((gives @ B @ A) & (ex @ B) & ~ (through_another @ B) & (independent @ B)))))),file('/tmp/xc.p',kalima)). thf(12,plain,((! [A:$i]: ((? [B:$i]: (gives @ B @ A)) => (? [B:$i]: ((gives @ B @ A) & (ex @ B) & ~ (? [C:$i]: (gives @ C @ B)) & ! [C:$i]: ~ (gives @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])). thf(13,plain,((! [A:$i]: ((? [B:$i]: (gives @ B @ A)) => (? [B:$i]: ((gives @ B @ A) & (ex @ B) & ~ (? [C:$i]: (gives @ C @ B)) & ~ (? [C:$i]: (gives @ C @ B))))))),inference(miniscope,[status(thm)],[12])). thf(14,plain,(! [B:$i,A:$i] : ((~ (gives @ B @ A)) | (gives @ (sk2 @ A) @ A))),inference(cnf,[status(esa)],[13])). thf(157,plain,(! [B:$i,A:$i] : ((gives @ (sk2 @ A) @ A) | ((gives @ sk4 @ sk3) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[20,14])). thf(158,plain,((gives @ (sk2 @ sk3) @ sk3)),inference(pattern_uni,[status(thm)],[157:[bind(A, $thf(sk3)),bind(B, $thf(sk4))]])). thf(1,conjecture,((? [A:$i,B:$i]: (((A = u) | (part @ A @ u)) & (gives @ B @ A) & (nec @ B) & (independent @ B)))),file('/tmp/xc.p',conclusion)). thf(2,negated_conjecture,((~ (? [A:$i,B:$i]: (((A = u) | (part @ A @ u)) & (gives @ B @ A) & (nec @ B) & (independent @ B))))),inference(neg_conjecture,[status(cth)],[1])). thf(6,plain,((~ (? [A:$i,B:$i]: (((A = u) | (part @ A @ u)) & (gives @ B @ A) & (ex @ B) & (ess @ B) & ! [C:$i]: ~ (gives @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(7,plain,((~ (? [A:$i]: (((A = u) | (part @ A @ u)) & ? [B:$i]: ((gives @ B @ A) & (ex @ B) & (ess @ B) & ~ (? [C:$i]: (gives @ C @ B))))))),inference(miniscope,[status(thm)],[6])). thf(9,plain,(! [B:$i,A:$i] : ((~ (part @ A @ u)) | (~ (gives @ B @ A)) | (~ (ex @ B)) | (~ (ess @ B)) | (gives @ (sk1 @ B @ A) @ B))),inference(cnf,[status(esa)],[7])). thf(16,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ B @ A)) | (~ (gives @ C @ (sk2 @ A))))),inference(cnf,[status(esa)],[13])). thf(35,plain,(! [C:$i,B:$i,A:$i] : ((~ (gives @ C @ (sk2 @ A))) | ((gives @ sk4 @ sk3) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[20,16])). thf(36,plain,(! [A:$i] : ((~ (gives @ A @ (sk2 @ sk3))))),inference(pattern_uni,[status(thm)],[35:[bind(A, $thf(sk3)),bind(B, $thf(sk4))]])). thf(42,plain,(! [A:$i] : ((~ (gives @ A @ (sk2 @ sk3))))),inference(simp,[status(thm)],[36])). thf(84,plain,(! [C:$i,B:$i,A:$i] : ((~ (part @ A @ u)) | (~ (gives @ B @ A)) | (~ (ex @ B)) | (~ (ess @ B)) | ((gives @ (sk1 @ B @ A) @ B) != (gives @ C @ (sk2 @ sk3))))),inference(paramod_ordered,[status(thm)],[9,42])). thf(85,plain,(! [A:$i] : ((~ (part @ A @ u)) | (~ (gives @ (sk2 @ sk3) @ A)) | (~ (ex @ (sk2 @ sk3))) | (~ (ess @ (sk2 @ sk3))))),inference(pattern_uni,[status(thm)],[84:[bind(A, $thf(E)),bind(B, $thf(sk2 @ sk3)),bind(C, $thf(sk1 @ (sk2 @ sk3) @ E))]])). thf(90,plain,(! [A:$i] : ((~ (part @ A @ u)) | (~ (gives @ (sk2 @ sk3) @ A)) | (~ (ex @ (sk2 @ sk3))) | (~ (ess @ (sk2 @ sk3))))),inference(simp,[status(thm)],[85])). thf(5,axiom,((! [A:$i]: (((ex @ A) & ~ (through_another @ A)) => (ess @ A)))),file('/tmp/xc.p',mp008)). thf(25,plain,((! [A:$i]: (((ex @ A) & ~ (? [B:$i]: (gives @ B @ A))) => (ess @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])). thf(26,plain,(! [A:$i] : ((~ (ex @ A)) | (gives @ (sk5 @ A) @ A) | (ess @ A))),inference(cnf,[status(esa)],[25])). thf(408,plain,(! [B:$i,A:$i] : ((~ (ex @ A)) | (ess @ A) | ((gives @ (sk5 @ A) @ A) != (gives @ B @ (sk2 @ sk3))))),inference(paramod_ordered,[status(thm)],[26,42])). thf(409,plain,((~ (ex @ (sk2 @ sk3))) | (ess @ (sk2 @ sk3))),inference(pattern_uni,[status(thm)],[408:[bind(A, $thf(sk2 @ sk3)),bind(B, $thf(sk5 @ (sk2 @ sk3)))]])). thf(15,plain,(! [B:$i,A:$i] : ((~ (gives @ B @ A)) | (ex @ (sk2 @ A)))),inference(cnf,[status(esa)],[13])). thf(266,plain,(! [B:$i,A:$i] : ((ex @ (sk2 @ A)) | ((gives @ sk4 @ sk3) != (gives @ B @ A)))),inference(paramod_ordered,[status(thm)],[20,15])). thf(267,plain,((ex @ (sk2 @ sk3))),inference(pattern_uni,[status(thm)],[266:[bind(A, $thf(sk3)),bind(B, $thf(sk4))]])). thf(472,plain,(~ (($true)) | (ess @ (sk2 @ sk3))),inference(rewrite,[status(thm)],[409,267])). thf(473,plain,((ess @ (sk2 @ sk3))),inference(simp,[status(thm)],[472])). thf(1811,plain,(! [A:$i] : ((~ (part @ A @ u)) | (~ (gives @ (sk2 @ sk3) @ A)) | ~ (($true)) | ~ (($true)))),inference(rewrite,[status(thm)],[90,473,267])). thf(1812,plain,(! [A:$i] : ((~ (part @ A @ u)) | (~ (gives @ (sk2 @ sk3) @ A)))),inference(simp,[status(thm)],[1811])). thf(1827,plain,(! [A:$i] : ((~ (part @ A @ u)) | ((gives @ (sk2 @ sk3) @ sk3) != (gives @ (sk2 @ sk3) @ A)))),inference(paramod_ordered,[status(thm)],[158,1812])). thf(1828,plain,((~ (part @ sk3 @ u))),inference(pattern_uni,[status(thm)],[1827:[bind(A, $thf(sk3))]])). thf(23,plain,((sk3 = u) | (part @ sk3 @ u)),inference(cnf,[status(esa)],[19])). thf(24,plain,((sk3 = u) | (part @ sk3 @ u)),inference(lifteq,[status(thm)],[23])). thf(8,plain,(! [B:$i,A:$i] : ((~ (A = u)) | (~ (gives @ B @ A)) | (~ (ex @ B)) | (~ (ess @ B)) | (gives @ (sk1 @ B @ A) @ B))),inference(cnf,[status(esa)],[7])). thf(10,plain,(! [B:$i,A:$i] : ((A != u) | (~ (gives @ B @ A)) | (~ (ex @ B)) | (~ (ess @ B)) | (gives @ (sk1 @ B @ A) @ B))),inference(lifteq,[status(thm)],[8])). thf(11,plain,(! [A:$i] : ((~ (gives @ A @ u)) | (~ (ex @ A)) | (~ (ess @ A)) | (gives @ (sk1 @ A @ u) @ A))),inference(simp,[status(thm)],[10])). thf(61,plain,(! [B:$i,A:$i] : ((~ (gives @ A @ u)) | (~ (ex @ A)) | (~ (ess @ A)) | ((gives @ (sk1 @ A @ u) @ A) != (gives @ B @ (sk2 @ sk3))))),inference(paramod_ordered,[status(thm)],[11,42])). thf(62,plain,((~ (gives @ (sk2 @ sk3) @ u)) | (~ (ex @ (sk2 @ sk3))) | (~ (ess @ (sk2 @ sk3)))),inference(pattern_uni,[status(thm)],[61:[bind(A, $thf(sk2 @ sk3)),bind(B, $thf(sk1 @ (sk2 @ sk3) @ u))]])). thf(194,plain,((~ (ex @ (sk2 @ sk3))) | (~ (ess @ (sk2 @ sk3))) | ((gives @ (sk2 @ sk3) @ sk3) != (gives @ (sk2 @ sk3) @ u))),inference(paramod_ordered,[status(thm)],[158,62])). thf(202,plain,((~ (ex @ (sk2 @ sk3))) | (~ (ess @ (sk2 @ sk3))) | ((sk2 @ sk3) != (sk2 @ sk3)) | (sk3 != u)),inference(simp,[status(thm)],[194])). thf(206,plain,((~ (ex @ (sk2 @ sk3))) | (~ (ess @ (sk2 @ sk3))) | (sk3 != u)),inference(simp,[status(thm)],[202])). thf(246,plain,((part @ sk3 @ u) | (~ (ex @ (sk2 @ sk3))) | (~ (ess @ (sk2 @ sk3))) | (sk3 != sk3)),inference(paramod_ordered,[status(thm)],[24,206])). thf(247,plain,((part @ sk3 @ u) | (~ (ex @ (sk2 @ sk3))) | (~ (ess @ (sk2 @ sk3)))),inference(pattern_uni,[status(thm)],[246:[]])). thf(279,plain,((part @ sk3 @ u) | ~ (($true)) | (~ (ess @ (sk2 @ sk3)))),inference(rewrite,[status(thm)],[247,267])). thf(280,plain,((part @ sk3 @ u) | (~ (ess @ (sk2 @ sk3)))),inference(simp,[status(thm)],[279])). thf(474,plain,((part @ sk3 @ u) | ~ (($true))),inference(rewrite,[status(thm)],[280,473])). thf(475,plain,((part @ sk3 @ u)),inference(simp,[status(thm)],[474])). thf(1849,plain,(~ (($true))),inference(rewrite,[status(thm)],[1828,475])). thf(1850,plain,(($false)),inference(simp,[status(thm)],[1849])). % SZS output end Refutation for /tmp/xc.p