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 (59ms). % [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,w3} % External prover 'cvc4' found a proof! % [INFO] Killing All external provers ... % Time passed: 827ms (effective reasoning time: 581ms) % Solved by strategy % Axioms used in derivation (3): people_worlds, people_domains, people_mappings % No. of inferences in proof: 10 % SZS status Theorem for NXF_Finite-Finite-Global.s.p : 827 ms resp. 581 ms w/o parsing % SZS output start Refutation for NXF_Finite-Finite-Global.s.p thf(child_type, type, child: $tType). thf(adult_type, type, adult: $tType). thf(child_d_type, type, child_d: $tType). thf(adult_d_type, type, adult_d: $tType). thf('$world_type', type, '$world': $tType). thf('$local_world_decl', type, '$local_world': '$world'). thf('$accessible_world_decl', type, '$accessible_world': ('$world' > ('$world' > $o))). thf(agatha_decl, type, agatha: adult). thf(charly_decl, type, charly: child). thf(quiet_decl, type, quiet: ('$world' > (child > $o))). thf(sleepy_decl, type, sleepy: ('$world' > (adult > $o))). thf(peaceful_decl, type, peaceful: ('$world' > (child > $o))). thf(serves_decl, type, serves: (adult > child)). thf(rains_decl, type, rains: ('$world' > $o)). thf(child_1_decl, type, child_1: child_d). thf(adult_1_decl, type, adult_1: adult_d). thf(d2child_decl, type, d2child: (child_d > child)). thf(d2adult_decl, type, d2adult: (adult_d > adult)). thf(w1_decl, type, w1: '$world'). thf(w2_decl, type, w2: '$world'). thf(w3_decl, type, w3: '$world'). thf('$exists_in_world_adult_decl', type, '$exists_in_world_adult': ('$world' > (adult > $o))). thf('$exists_in_world_adult_d_decl', type, '$exists_in_world_adult_d': ('$world' > (adult_d > $o))). thf('$exists_in_world_child_d_decl', type, '$exists_in_world_child_d': ('$world' > (child_d > $o))). thf('$exists_in_world_child_decl', type, '$exists_in_world_child': ('$world' > (child > $o))). thf(1,conjecture,((! [A:'$world',B:child]: (('$exists_in_world_child' @ A @ B) => (~ (~ (quiet @ A @ B) & ? [C:adult]: (('$exists_in_world_adult' @ A @ C) & (sleepy @ A @ C))))) & ! [A:'$world']: (((rains @ A) & ? [B:child]: (('$exists_in_world_child' @ A @ B) & (quiet @ A @ B))) => (! [B:child]: (('$exists_in_world_child' @ A @ B) => (~ (peaceful @ A @ B))))) & ! [A:'$world']: ((peaceful @ A @ charly) | (~ (quiet @ A @ charly) & (quiet @ A @ (serves @ agatha)))) & ! [A:'$world']: ((~ (quiet @ A @ charly)) => (! [B:child]: (('$exists_in_world_child' @ A @ B) => (~ (quiet @ A @ B))))) & ! [A:'$world',B:'$world']: (('$accessible_world' @ A @ B) => ((peaceful @ B @ charly) => (rains @ B))) & ~ (? [A:'$world']: (('$accessible_world' @ '$local_world' @ A) & ~ (rains @ A))))),file('NXF_Finite-Finite-Global.s.p','a1+a2+a3+a4+a5+c')). thf(2,negated_conjecture,((~ (! [A:'$world',B:child]: (('$exists_in_world_child' @ A @ B) => (~ (~ (quiet @ A @ B) & ? [C:adult]: (('$exists_in_world_adult' @ A @ C) & (sleepy @ A @ C))))) & ! [A:'$world']: (((rains @ A) & ? [B:child]: (('$exists_in_world_child' @ A @ B) & (quiet @ A @ B))) => (! [B:child]: (('$exists_in_world_child' @ A @ B) => (~ (peaceful @ A @ B))))) & ! [A:'$world']: ((peaceful @ A @ charly) | (~ (quiet @ A @ charly) & (quiet @ A @ (serves @ agatha)))) & ! [A:'$world']: ((~ (quiet @ A @ charly)) => (! [B:child]: (('$exists_in_world_child' @ A @ B) => (~ (quiet @ A @ B))))) & ! [A:'$world',B:'$world']: (('$accessible_world' @ A @ B) => ((peaceful @ B @ charly) => (rains @ B))) & ~ (? [A:'$world']: (('$accessible_world' @ '$local_world' @ A) & ~ (rains @ A)))))),inference(neg_conjecture,[status(cth)],[1])). thf(6,plain,((~ (! [A:'$world',B:child]: (('$exists_in_world_child' @ A @ B) => (~ (~ (quiet @ A @ B) & ? [C:adult]: (('$exists_in_world_adult' @ A @ C) & (sleepy @ A @ C))))) & ! [A:'$world']: (((rains @ A) & ? [B:child]: (('$exists_in_world_child' @ A @ B) & (quiet @ A @ B))) => (! [B:child]: (('$exists_in_world_child' @ A @ B) => (~ (peaceful @ A @ B))))) & ! [A:'$world']: ((peaceful @ A @ charly) | (~ (quiet @ A @ charly) & (quiet @ A @ (serves @ agatha)))) & ! [A:'$world']: ((~ (quiet @ A @ charly)) => (! [B:child]: (('$exists_in_world_child' @ A @ B) => (~ (quiet @ A @ B))))) & ! [A:'$world',B:'$world']: (('$accessible_world' @ A @ B) => ((peaceful @ B @ charly) => (rains @ B))) & ~ (? [A:'$world']: (('$accessible_world' @ '$local_world' @ A) & ~ (rains @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])). thf(3,axiom,((! [A:'$world']: ((A = w1) | (A = w2) | (A = w3)) & (w1 != w2) & (w1 != w3) & (w2 != w3) & ('$local_world' = w1) & ('$accessible_world' @ w1 @ w1) & ('$accessible_world' @ w2 @ w2) & ('$accessible_world' @ w1 @ w2) & ('$accessible_world' @ w2 @ w3) & ('$accessible_world' @ w3 @ w1) & ~ ('$accessible_world' @ w1 @ w3) & ~ ('$accessible_world' @ w2 @ w1) & ~ ('$accessible_world' @ w3 @ w2) & ~ ('$accessible_world' @ w3 @ w3))),file('NXF_Finite-Finite-Global.s.p',people_worlds)). thf(38,plain,((! [A:'$world']: ((A = w1) | (A = w2) | (A = w3)) & ~ (w1 = w2) & ~ (w1 = w3) & ~ (w2 = w3) & ('$local_world' = w1) & ('$accessible_world' @ w1 @ w1) & ('$accessible_world' @ w2 @ w2) & ('$accessible_world' @ w1 @ w2) & ('$accessible_world' @ w2 @ w3) & ('$accessible_world' @ w3 @ w1) & ~ ('$accessible_world' @ w1 @ w3) & ~ ('$accessible_world' @ w2 @ w1) & ~ ('$accessible_world' @ w3 @ w2) & ~ ('$accessible_world' @ w3 @ w3))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])). thf(4,axiom,((! [A:child]: (('$exists_in_world_child' @ w1 @ A) => (? [B:child_d]: (('$exists_in_world_child_d' @ w1 @ B) & (A = (d2child @ B))))) & ! [A:child_d]: (('$exists_in_world_child_d' @ w1 @ A) => (A = child_1)) & ! [A:child_d,B:child_d]: ((('$exists_in_world_child_d' @ w1 @ A) & ('$exists_in_world_child_d' @ w1 @ B)) => (((d2child @ A) = (d2child @ B)) => (A = B))) & ! [A:adult]: (('$exists_in_world_adult' @ w1 @ A) => (? [B:adult_d]: (('$exists_in_world_adult_d' @ w1 @ B) & (A = (d2adult @ B))))) & ! [A:adult_d]: (('$exists_in_world_adult_d' @ w1 @ A) => (A = adult_1)) & ! [A:adult_d,B:adult_d]: ((('$exists_in_world_adult_d' @ w1 @ A) & ('$exists_in_world_adult_d' @ w1 @ B)) => (((d2adult @ A) = (d2adult @ B)) => (A = B))) & ! [A:child]: (('$exists_in_world_child' @ w2 @ A) => (? [B:child_d]: (('$exists_in_world_child_d' @ w2 @ B) & (A = (d2child @ B))))) & ! [A:child_d]: (('$exists_in_world_child_d' @ w2 @ A) => (A = child_1)) & ! [A:child_d,B:child_d]: ((('$exists_in_world_child_d' @ w2 @ A) & ('$exists_in_world_child_d' @ w2 @ B)) => (((d2child @ A) = (d2child @ B)) => (A = B))) & ! [A:adult]: (('$exists_in_world_adult' @ w2 @ A) => (? [B:adult_d]: (('$exists_in_world_adult_d' @ w2 @ B) & (A = (d2adult @ B))))) & ! [A:adult_d]: (('$exists_in_world_adult_d' @ w2 @ A) => (A = adult_1)) & ! [A:adult_d,B:adult_d]: ((('$exists_in_world_adult_d' @ w2 @ A) & ('$exists_in_world_adult_d' @ w2 @ B)) => (((d2adult @ A) = (d2adult @ B)) => (A = B))) & ! [A:child]: (('$exists_in_world_child' @ w3 @ A) => (? [B:child_d]: (('$exists_in_world_child_d' @ w3 @ B) & (A = (d2child @ B))))) & ! [A:child_d]: (('$exists_in_world_child_d' @ w3 @ A) => (A = child_1)) & ! [A:child_d,B:child_d]: ((('$exists_in_world_child_d' @ w3 @ A) & ('$exists_in_world_child_d' @ w3 @ B)) => (((d2child @ A) = (d2child @ B)) => (A = B))) & ! [A:adult]: (('$exists_in_world_adult' @ w3 @ A) => (? [B:adult_d]: (('$exists_in_world_adult_d' @ w3 @ B) & (A = (d2adult @ B))))) & ! [A:adult_d]: (('$exists_in_world_adult_d' @ w3 @ A) => (A = adult_1)) & ! [A:adult_d,B:adult_d]: ((('$exists_in_world_adult_d' @ w3 @ A) & ('$exists_in_world_adult_d' @ w3 @ B)) => (((d2adult @ A) = (d2adult @ B)) => (A = B))))),file('NXF_Finite-Finite-Global.s.p',people_domains)). thf(59,plain,((! [A:child]: (('$exists_in_world_child' @ w1 @ A) => (? [B:child_d]: (('$exists_in_world_child_d' @ w1 @ B) & (A = (d2child @ B))))) & ! [A:child_d]: (('$exists_in_world_child_d' @ w1 @ A) => (A = child_1)) & ! [A:child_d,B:child_d]: ((('$exists_in_world_child_d' @ w1 @ A) & ('$exists_in_world_child_d' @ w1 @ B)) => (((d2child @ A) = (d2child @ B)) => (A = B))) & ! [A:adult]: (('$exists_in_world_adult' @ w1 @ A) => (? [B:adult_d]: (('$exists_in_world_adult_d' @ w1 @ B) & (A = (d2adult @ B))))) & ! [A:adult_d]: (('$exists_in_world_adult_d' @ w1 @ A) => (A = adult_1)) & ! [A:adult_d,B:adult_d]: ((('$exists_in_world_adult_d' @ w1 @ A) & ('$exists_in_world_adult_d' @ w1 @ B)) => (((d2adult @ A) = (d2adult @ B)) => (A = B))) & ! [A:child]: (('$exists_in_world_child' @ w2 @ A) => (? [B:child_d]: (('$exists_in_world_child_d' @ w2 @ B) & (A = (d2child @ B))))) & ! [A:child_d]: (('$exists_in_world_child_d' @ w2 @ A) => (A = child_1)) & ! [A:child_d,B:child_d]: ((('$exists_in_world_child_d' @ w2 @ A) & ('$exists_in_world_child_d' @ w2 @ B)) => (((d2child @ A) = (d2child @ B)) => (A = B))) & ! [A:adult]: (('$exists_in_world_adult' @ w2 @ A) => (? [B:adult_d]: (('$exists_in_world_adult_d' @ w2 @ B) & (A = (d2adult @ B))))) & ! [A:adult_d]: (('$exists_in_world_adult_d' @ w2 @ A) => (A = adult_1)) & ! [A:adult_d,B:adult_d]: ((('$exists_in_world_adult_d' @ w2 @ A) & ('$exists_in_world_adult_d' @ w2 @ B)) => (((d2adult @ A) = (d2adult @ B)) => (A = B))) & ! [A:child]: (('$exists_in_world_child' @ w3 @ A) => (? [B:child_d]: (('$exists_in_world_child_d' @ w3 @ B) & (A = (d2child @ B))))) & ! [A:child_d]: (('$exists_in_world_child_d' @ w3 @ A) => (A = child_1)) & ! [A:child_d,B:child_d]: ((('$exists_in_world_child_d' @ w3 @ A) & ('$exists_in_world_child_d' @ w3 @ B)) => (((d2child @ A) = (d2child @ B)) => (A = B))) & ! [A:adult]: (('$exists_in_world_adult' @ w3 @ A) => (? [B:adult_d]: (('$exists_in_world_adult_d' @ w3 @ B) & (A = (d2adult @ B))))) & ! [A:adult_d]: (('$exists_in_world_adult_d' @ w3 @ A) => (A = adult_1)) & ! [A:adult_d,B:adult_d]: ((('$exists_in_world_adult_d' @ w3 @ A) & ('$exists_in_world_adult_d' @ w3 @ B)) => (((d2adult @ A) = (d2adult @ B)) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])). thf(5,axiom,(((charly = (d2child @ child_1)) & (agatha = (d2adult @ adult_1)) & ((serves @ (d2adult @ adult_1)) = (d2child @ child_1)) & ~ (quiet @ w1 @ (d2child @ child_1)) & ~ (sleepy @ w1 @ (d2adult @ adult_1)) & (peaceful @ w1 @ (d2child @ child_1)) & (rains @ w1) & (charly = (d2child @ child_1)) & (agatha = (d2adult @ adult_1)) & ((serves @ (d2adult @ adult_1)) = (d2child @ child_1)) & ~ (quiet @ w2 @ (d2child @ child_1)) & ~ (sleepy @ w2 @ (d2adult @ adult_1)) & (peaceful @ w2 @ (d2child @ child_1)) & (rains @ w2) & (charly = (d2child @ child_1)) & (agatha = (d2adult @ adult_1)) & ((serves @ (d2adult @ adult_1)) = (d2child @ child_1)) & ~ (quiet @ w3 @ (d2child @ child_1)) & ~ (sleepy @ w3 @ (d2adult @ adult_1)) & (peaceful @ w3 @ (d2child @ child_1)) & (rains @ w3))),file('NXF_Finite-Finite-Global.s.p',people_mappings)). thf(125,plain,(((charly = (d2child @ child_1)) & (agatha = (d2adult @ adult_1)) & ((serves @ (d2adult @ adult_1)) = (d2child @ child_1)) & ~ (quiet @ w1 @ (d2child @ child_1)) & ~ (sleepy @ w1 @ (d2adult @ adult_1)) & (peaceful @ w1 @ (d2child @ child_1)) & (rains @ w1) & (charly = (d2child @ child_1)) & (agatha = (d2adult @ adult_1)) & ((serves @ (d2adult @ adult_1)) = (d2child @ child_1)) & ~ (quiet @ w2 @ (d2child @ child_1)) & ~ (sleepy @ w2 @ (d2adult @ adult_1)) & (peaceful @ w2 @ (d2child @ child_1)) & (rains @ w2) & (charly = (d2child @ child_1)) & (agatha = (d2adult @ adult_1)) & ((serves @ (d2adult @ adult_1)) = (d2child @ child_1)) & ~ (quiet @ w3 @ (d2child @ child_1)) & ~ (sleepy @ w3 @ (d2adult @ adult_1)) & (peaceful @ w3 @ (d2child @ child_1)) & (rains @ w3))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])). thf(166,plain,(($false)),inference(cvc4,[status(thm)],[6,38,59,125])). % 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 = 3.26 WC = 0.97 OUTPUT: NXF_Finite-Finite-Global.s - Leo-III---1.7.20 says Refutation - CPU = 3.26 WC = 0.99