% SZS status Theorem for NXF_Finite-Finite-Global.s.p : 1739 ms resp. 1016 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('\'$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(d_alex_type, type, d_alex: person).
thf(d_chris_type, type, d_chris: person).
thf(d_leo_type, type, d_leo: 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(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(4,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) & ! [A:person]: (('\'$exists_in_world_person\'' @ w1 @ A) => ((A = d_alex) | (A = d_chris))) & (d_alex != d_chris) & ? [A:person]: (('\'$exists_in_world_person\'' @ w1 @ A) & (A = d_alex)) & ? [A:person]: (('\'$exists_in_world_person\'' @ w1 @ A) & (A = d_chris)) & ! [A:product]: (('\'$exists_in_world_product\'' @ w1 @ A) => (A = d_leo)) & ? [A:product]: (('\'$exists_in_world_product\'' @ w1 @ A) & (A = d_leo)) & (alex = d_alex) & (chris = d_chris) & (leo = d_leo) & (work_hard @ w1 @ d_alex @ d_leo) & (work_hard @ w1 @ d_chris @ d_leo) & (gets_rich @ w1 @ d_alex) & (gets_rich @ w1 @ d_chris) & ! [A:person]: (('\'$exists_in_world_person\'' @ w2 @ A) => ((A = d_alex) | (A = d_chris))) & (d_alex != d_chris) & ? [A:person]: (('\'$exists_in_world_person\'' @ w2 @ A) & (A = d_alex)) & ? [A:person]: (('\'$exists_in_world_person\'' @ w2 @ A) & (A = d_chris)) & ! [A:product]: (('\'$exists_in_world_product\'' @ w2 @ A) => (A = d_leo)) & ? [A:product]: (('\'$exists_in_world_product\'' @ w2 @ A) & (A = d_leo)) & (alex = d_alex) & (chris = d_chris) & (leo = d_leo) & (work_hard @ w2 @ d_alex @ d_leo) & (work_hard @ w2 @ d_chris @ d_leo) & ~ (gets_rich @ w2 @ d_alex) & ~ (gets_rich @ w2 @ d_chris))),file('NXF_Finite-Finite-Global.s.p',leo_workers)).
thf(16,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) & ! [A:person]: (('\'$exists_in_world_person\'' @ w1 @ A) => ((A = d_alex) | (A = d_chris))) & ~ (d_alex = d_chris) & ? [A:person]: (('\'$exists_in_world_person\'' @ w1 @ A) & (A = d_alex)) & ? [A:person]: (('\'$exists_in_world_person\'' @ w1 @ A) & (A = d_chris)) & ! [A:product]: (('\'$exists_in_world_product\'' @ w1 @ A) => (A = d_leo)) & ? [A:product]: (('\'$exists_in_world_product\'' @ w1 @ A) & (A = d_leo)) & (alex = d_alex) & (chris = d_chris) & (leo = d_leo) & (work_hard @ w1 @ d_alex @ d_leo) & (work_hard @ w1 @ d_chris @ d_leo) & (gets_rich @ w1 @ d_alex) & (gets_rich @ w1 @ d_chris) & ! [A:person]: (('\'$exists_in_world_person\'' @ w2 @ A) => ((A = d_alex) | (A = d_chris))) & ~ (d_alex = d_chris) & ? [A:person]: (('\'$exists_in_world_person\'' @ w2 @ A) & (A = d_alex)) & ? [A:person]: (('\'$exists_in_world_person\'' @ w2 @ A) & (A = d_chris)) & ! [A:product]: (('\'$exists_in_world_product\'' @ w2 @ A) => (A = d_leo)) & ? [A:product]: (('\'$exists_in_world_product\'' @ w2 @ A) & (A = d_leo)) & (alex = d_alex) & (chris = d_chris) & (leo = d_leo) & (work_hard @ w2 @ d_alex @ d_leo) & (work_hard @ w2 @ d_chris @ d_leo) & ~ (gets_rich @ w2 @ d_alex) & ~ (gets_rich @ w2 @ d_chris))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
thf(74,plain,(($false)),inference(cvc4,[status(thm)],[4,16])).
% SZS output end Refutation for NXF_Finite-Finite-Global.s.p