Leo-III---1.7.20 system information being retrieved Leo-III---1.7.20's non-default parameters being retrieved Leo-III---1.7.20's NXF_Finite-Finite-Global.s does not need preparation Leo-III---1.7.20 being executed on NXF_Finite-Finite-Global.s using /home/tptp/Systems/Leo-III---1.7.20/run_Leo-III 'NXF_Finite-Finite-Global.s.p' 120 THM % START OF SYSTEM OUTPUT % [INFO] Parsing problem NXF_Finite-Finite-Global.s.p ... % [INFO] Parsing done (69ms). % [INFO] Input problem is non-classical (logic $$fomlModel). Running HOL transformation from semantics specification contained in the problem file ... % [INFO] Running in sequential loop mode. % [INFO] eprover registered as external prover. % [INFO] cvc4 registered as external prover. % [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 typed first-order (TPTP TFF). % [INFO] Type checking passed. % [CONFIG] Using configuration: timeout(120) with strategy. Searching for refutation ... % [INFO] [Domain constraints] Detected constraint on '$world' % [INFO] [Domain constraints] dom('$world') ⊆ {w1,w2} % External prover 'cvc4' found a proof! % [INFO] Killing All external provers ... % Time passed: 810ms (effective reasoning time: 541ms) % Solved by strategy % Axioms used in derivation (3): leo_workers_worlds, leo_workers_domains, leo_workers_mappings % No. of inferences in proof: 10 % SZS status Theorem for NXF_Finite-Finite-Global.s.p : 810 ms resp. 541 ms w/o parsing % SZS output start Refutation for NXF_Finite-Finite-Global.s.p thf(person_type, type, person: $tType). thf(product_type, type, product: $tType). thf(d_person_type, type, d_person: $tType). thf(d_product_type, type, d_product: $tType). thf('\'$world\'_type', type, '\'$world\'': $tType). thf('\'$local_world\'_type', type, '\'$local_world\'': '\'$world\''). thf('\'$accessible_world\'_type', type, '\'$accessible_world\'': ('\'$world\'' > ('\'$world\'' > $o))). thf(alex_type, type, alex: person). thf(chris_type, type, chris: person). thf(leo_type, type, leo: product). thf(work_hard_type, type, work_hard: ('\'$world\'' > (person > (product > $o)))). thf(gets_rich_type, type, gets_rich: ('\'$world\'' > (person > $o))). thf(d2person_type, type, d2person: (d_person > person)). thf(d_alex_type, type, d_alex: d_person). thf(d_chris_type, type, d_chris: d_person). thf(d2product_type, type, d2product: (d_product > product)). thf(d_leo_type, type, d_leo: d_product). thf(w1_type, type, w1: '\'$world\''). thf(w2_type, type, w2: '\'$world\''). thf('\'$exists_in_world_product\'_type', type, '\'$exists_in_world_product\'': ('\'$world\'' > (product > $o))). thf('\'$exists_in_world_person\'_type', type, '\'$exists_in_world_person\'': ('\'$world\'' > (person > $o))). thf('\'$exists_in_world_d_person\'_type', type, '\'$exists_in_world_d_person\'': ('\'$world\'' > (d_person > $o))). thf('\'$exists_in_world_d_product\'_type', type, '\'$exists_in_world_d_product\'': ('\'$world\'' > (d_product > $o))). thf(1,conjecture,((! [A:'\'$world\'',B:person]: (('\'$exists_in_world_person\'' @ A @ B) => ((? [C:product]: (('\'$exists_in_world_product\'' @ A @ C) & (work_hard @ A @ B @ C))) => (? [C:'\'$world\'']: (('\'$accessible_world\'' @ A @ C) & (gets_rich @ C @ B))))) & ! [A:'\'$world\'']: ~ (? [B:person]: (('\'$exists_in_world_person\'' @ A @ B) & ! [C:'\'$world\'']: (('\'$accessible_world\'' @ A @ C) => (gets_rich @ C @ B)))) & ! [A:'\'$world\'']: (work_hard @ A @ alex @ leo) & ! [A:'\'$world\'']: (work_hard @ A @ chris @ leo) & ~ (? [A:'\'$world\'']: (('\'$accessible_world\'' @ '\'$local_world\'' @ A) & (gets_rich @ A @ alex) & ~ (gets_rich @ A @ chris))))),file('NXF_Finite-Finite-Global.s.p','work_hard_to_get_rich+not_all_get_rich+alex_works_on_leo+chris_works_on_leo+only_alex_gets_rich')). thf(2,negated_conjecture,((~ (! [A:'\'$world\'',B:person]: (('\'$exists_in_world_person\'' @ A @ B) => ((? [C:product]: (('\'$exists_in_world_product\'' @ A @ C) & (work_hard @ A @ B @ C))) => (? [C:'\'$world\'']: (('\'$accessible_world\'' @ A @ C) & (gets_rich @ C @ B))))) & ! [A:'\'$world\'']: ~ (? [B:person]: (('\'$exists_in_world_person\'' @ A @ B) & ! [C:'\'$world\'']: (('\'$accessible_world\'' @ A @ C) => (gets_rich @ C @ B)))) & ! [A:'\'$world\'']: (work_hard @ A @ alex @ leo) & ! [A:'\'$world\'']: (work_hard @ A @ chris @ leo) & ~ (? [A:'\'$world\'']: (('\'$accessible_world\'' @ '\'$local_world\'' @ A) & (gets_rich @ A @ alex) & ~ (gets_rich @ A @ chris)))))),inference(neg_conjecture,[status(cth)],[1])). thf(6,plain,((~ (! [A:'\'$world\'',B:person]: (('\'$exists_in_world_person\'' @ A @ B) => ((? [C:product]: (('\'$exists_in_world_product\'' @ A @ C) & (work_hard @ A @ B @ C))) => (? [C:'\'$world\'']: (('\'$accessible_world\'' @ A @ C) & (gets_rich @ C @ B))))) & ! [A:'\'$world\'']: ~ (? [B:person]: (('\'$exists_in_world_person\'' @ A @ B) & ! [C:'\'$world\'']: (('\'$accessible_world\'' @ A @ C) => (gets_rich @ C @ B)))) & ! [A:'\'$world\'']: (work_hard @ A @ alex @ leo) & ! [A:'\'$world\'']: (work_hard @ A @ chris @ leo) & ~ (? [A:'\'$world\'']: (('\'$accessible_world\'' @ '\'$local_world\'' @ A) & (gets_rich @ A @ alex) & ~ (gets_rich @ A @ chris)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(3,axiom,((! [A:'\'$world\'']: ((A = w1) | (A = w2)) & (w1 != w2) & ('\'$local_world\'' = w2) & ('\'$accessible_world\'' @ w1 @ w1) & ('\'$accessible_world\'' @ w2 @ w2) & ('\'$accessible_world\'' @ w1 @ w2) & ('\'$accessible_world\'' @ w2 @ w1))),file('NXF_Finite-Finite-Global.s.p',leo_workers_worlds)). thf(18,plain,((! [A:'\'$world\'']: ((A = w1) | (A = w2)) & ~ (w1 = w2) & ('\'$local_world\'' = w2) & ('\'$accessible_world\'' @ w1 @ w1) & ('\'$accessible_world\'' @ w2 @ w2) & ('\'$accessible_world\'' @ w1 @ w2) & ('\'$accessible_world\'' @ w2 @ w1))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])). thf(4,axiom,((! [A:person]: (('\'$exists_in_world_person\'' @ w1 @ A) => (? [B:d_person]: (('\'$exists_in_world_d_person\'' @ w1 @ B) & (A = (d2person @ B))))) & ! [A:d_person]: (('\'$exists_in_world_d_person\'' @ w1 @ A) => ((A = d_alex) | (A = d_chris))) & (d_alex != d_chris) & ? [A:d_person]: (('\'$exists_in_world_d_person\'' @ w1 @ A) & (A = d_alex)) & ? [A:d_person]: (('\'$exists_in_world_d_person\'' @ w1 @ A) & (A = d_chris)) & ! [A:d_person,B:d_person]: ((('\'$exists_in_world_d_person\'' @ w1 @ A) & ('\'$exists_in_world_d_person\'' @ w1 @ B)) => (((d2person @ A) = (d2person @ B)) => (A = B))) & ! [A:product]: (('\'$exists_in_world_product\'' @ w1 @ A) => (? [B:d_product]: (('\'$exists_in_world_d_product\'' @ w1 @ B) & (A = (d2product @ B))))) & ! [A:d_product]: (('\'$exists_in_world_d_product\'' @ w1 @ A) => (A = d_leo)) & ? [A:d_product]: (('\'$exists_in_world_d_product\'' @ w1 @ A) & (A = d_leo)) & ! [A:d_product,B:d_product]: ((('\'$exists_in_world_d_product\'' @ w1 @ A) & ('\'$exists_in_world_d_product\'' @ w1 @ B)) => (((d2product @ A) = (d2product @ B)) => (A = B))) & ! [A:person]: (('\'$exists_in_world_person\'' @ w2 @ A) => (? [B:d_person]: (('\'$exists_in_world_d_person\'' @ w2 @ B) & (A = (d2person @ B))))) & ! [A:d_person]: (('\'$exists_in_world_d_person\'' @ w2 @ A) => ((A = d_alex) | (A = d_chris))) & (d_alex != d_chris) & ? [A:d_person]: (('\'$exists_in_world_d_person\'' @ w2 @ A) & (A = d_alex)) & ? [A:d_person]: (('\'$exists_in_world_d_person\'' @ w2 @ A) & (A = d_chris)) & ! [A:d_person,B:d_person]: ((('\'$exists_in_world_d_person\'' @ w2 @ A) & ('\'$exists_in_world_d_person\'' @ w2 @ B)) => (((d2person @ A) = (d2person @ B)) => (A = B))) & ! [A:product]: (('\'$exists_in_world_product\'' @ w2 @ A) => (? [B:d_product]: (('\'$exists_in_world_d_product\'' @ w2 @ B) & (A = (d2product @ B))))) & ! [A:d_product]: (('\'$exists_in_world_d_product\'' @ w2 @ A) => (A = d_leo)) & ? [A:d_product]: (('\'$exists_in_world_d_product\'' @ w2 @ A) & (A = d_leo)) & ! [A:d_product,B:d_product]: ((('\'$exists_in_world_d_product\'' @ w2 @ A) & ('\'$exists_in_world_d_product\'' @ w2 @ B)) => (((d2product @ A) = (d2product @ B)) => (A = B))))),file('NXF_Finite-Finite-Global.s.p',leo_workers_domains)). thf(29,plain,((! [A:person]: (('\'$exists_in_world_person\'' @ w1 @ A) => (? [B:d_person]: (('\'$exists_in_world_d_person\'' @ w1 @ B) & (A = (d2person @ B))))) & ! [A:d_person]: (('\'$exists_in_world_d_person\'' @ w1 @ A) => ((A = d_alex) | (A = d_chris))) & ~ (d_alex = d_chris) & ? [A:d_person]: (('\'$exists_in_world_d_person\'' @ w1 @ A) & (A = d_alex)) & ? [A:d_person]: (('\'$exists_in_world_d_person\'' @ w1 @ A) & (A = d_chris)) & ! [A:d_person,B:d_person]: ((('\'$exists_in_world_d_person\'' @ w1 @ A) & ('\'$exists_in_world_d_person\'' @ w1 @ B)) => (((d2person @ A) = (d2person @ B)) => (A = B))) & ! [A:product]: (('\'$exists_in_world_product\'' @ w1 @ A) => (? [B:d_product]: (('\'$exists_in_world_d_product\'' @ w1 @ B) & (A = (d2product @ B))))) & ! [A:d_product]: (('\'$exists_in_world_d_product\'' @ w1 @ A) => (A = d_leo)) & ? [A:d_product]: (('\'$exists_in_world_d_product\'' @ w1 @ A) & (A = d_leo)) & ! [A:d_product,B:d_product]: ((('\'$exists_in_world_d_product\'' @ w1 @ A) & ('\'$exists_in_world_d_product\'' @ w1 @ B)) => (((d2product @ A) = (d2product @ B)) => (A = B))) & ! [A:person]: (('\'$exists_in_world_person\'' @ w2 @ A) => (? [B:d_person]: (('\'$exists_in_world_d_person\'' @ w2 @ B) & (A = (d2person @ B))))) & ! [A:d_person]: (('\'$exists_in_world_d_person\'' @ w2 @ A) => ((A = d_alex) | (A = d_chris))) & ~ (d_alex = d_chris) & ? [A:d_person]: (('\'$exists_in_world_d_person\'' @ w2 @ A) & (A = d_alex)) & ? [A:d_person]: (('\'$exists_in_world_d_person\'' @ w2 @ A) & (A = d_chris)) & ! [A:d_person,B:d_person]: ((('\'$exists_in_world_d_person\'' @ w2 @ A) & ('\'$exists_in_world_d_person\'' @ w2 @ B)) => (((d2person @ A) = (d2person @ B)) => (A = B))) & ! [A:product]: (('\'$exists_in_world_product\'' @ w2 @ A) => (? [B:d_product]: (('\'$exists_in_world_d_product\'' @ w2 @ B) & (A = (d2product @ B))))) & ! [A:d_product]: (('\'$exists_in_world_d_product\'' @ w2 @ A) => (A = d_leo)) & ? [A:d_product]: (('\'$exists_in_world_d_product\'' @ w2 @ A) & (A = d_leo)) & ! [A:d_product,B:d_product]: ((('\'$exists_in_world_d_product\'' @ w2 @ A) & ('\'$exists_in_world_d_product\'' @ w2 @ B)) => (((d2product @ A) = (d2product @ B)) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])). thf(5,axiom,(((alex = (d2person @ d_alex)) & (chris = (d2person @ d_chris)) & (leo = (d2product @ d_leo)) & (work_hard @ w1 @ (d2person @ d_alex) @ (d2product @ d_leo)) & (work_hard @ w1 @ (d2person @ d_chris) @ (d2product @ d_leo)) & (gets_rich @ w1 @ (d2person @ d_alex)) & (gets_rich @ w1 @ (d2person @ d_chris)) & (alex = (d2person @ d_alex)) & (chris = (d2person @ d_chris)) & (leo = (d2product @ d_leo)) & (work_hard @ w2 @ (d2person @ d_alex) @ (d2product @ d_leo)) & (work_hard @ w2 @ (d2person @ d_chris) @ (d2product @ d_leo)) & ~ (gets_rich @ w2 @ (d2person @ d_alex)) & ~ (gets_rich @ w2 @ (d2person @ d_chris)))),file('NXF_Finite-Finite-Global.s.p',leo_workers_mappings)). thf(92,plain,(((alex = (d2person @ d_alex)) & (chris = (d2person @ d_chris)) & (leo = (d2product @ d_leo)) & (work_hard @ w1 @ (d2person @ d_alex) @ (d2product @ d_leo)) & (work_hard @ w1 @ (d2person @ d_chris) @ (d2product @ d_leo)) & (gets_rich @ w1 @ (d2person @ d_alex)) & (gets_rich @ w1 @ (d2person @ d_chris)) & (alex = (d2person @ d_alex)) & (chris = (d2person @ d_chris)) & (leo = (d2product @ d_leo)) & (work_hard @ w2 @ (d2person @ d_alex) @ (d2product @ d_leo)) & (work_hard @ w2 @ (d2person @ d_chris) @ (d2product @ d_leo)) & ~ (gets_rich @ w2 @ (d2person @ d_alex)) & ~ (gets_rich @ w2 @ (d2person @ d_chris)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])). thf(130,plain,(($false)),inference(cvc4,[status(thm)],[6,18,29,92])). % SZS output end Refutation for NXF_Finite-Finite-Global.s.p % [INFO] Killing All external provers ... % END OF SYSTEM OUTPUT RESULT: NXF_Finite-Finite-Global.s - Leo-III---1.7.20 says Theorem - CPU = 2.74 WC = 0.96 OUTPUT: NXF_Finite-Finite-Global.s - Leo-III---1.7.20 says Refutation - CPU = 3.15 WC = 0.98