%------------------------------------------------------------------------------ % File : hopCoP---0.1 % Problem : PUZ002-1 : TPTP v9.0.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n031.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Jul 25 01:24:23 PM UTC 2025 % Result : Unsatisfiable 0.12s 0.34s % Output : CNFRefutation 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PUZ002-1 : TPTP v9.0.0. Released v1.0.0. % 0.03/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.33 % Computer : n031.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Jul 21 15:46:49 EDT 2025 % 0.12/0.33 % CPUTime : % 0.12/0.34 % launching worker at depth: 3 % 0.12/0.34 % launching worker at depth: 2 % 0.12/0.34 % launching worker at depth: 4 % 0.12/0.34 % launching worker at depth: 7 % 0.12/0.34 % launching worker at depth: 5 % 0.12/0.34 % launching worker at depth: 6 % 0.12/0.34 % launching worker at depth: 1 % 0.12/0.34 % launching worker at depth: 8 % 0.12/0.34 % launching worker at depth: 9 % 0.12/0.34 % launching worker at depth: 10 % 0.12/0.34 % launching worker at depth: 11 % 0.12/0.34 % launching worker at depth: 12 % 0.12/0.34 % launching worker at depth: 13 % 0.12/0.34 % launching worker at depth: 14 % 0.12/0.34 % launching worker at depth: 15 % 0.12/0.34 % launching worker at depth: 16 % 0.12/0.34 % SZS status Theorem for theBenchmark % 0.12/0.34 % SZS output start CNFRefutation % 0.12/0.34 cnf(11, plain, ~avoided(the_kangaroo), inference(cnf, [status(esa)], [avoid_kangaroo])). % 0.12/0.34 cnf(l0, plain, ~avoided(the_kangaroo), inference(instantiation, [status(thm)], [11])). % 0.12/0.34 cnf(2, plain, ~detested(X0) | avoided(X0), inference(cnf, [status(esa)], [avoid_detested])). % 0.12/0.34 cnf(l1, plain, ~detested(the_kangaroo) | avoided(the_kangaroo), inference(instantiation, [status(thm)], [2])). % 0.12/0.34 cnf(8, plain, takes_to_me(X0) | detested(X0), inference(cnf, [status(esa)], [takes_to_me_or_detested])). % 0.12/0.34 cnf(l2, plain, takes_to_me(the_kangaroo) | detested(the_kangaroo), inference(instantiation, [status(thm)], [8])). % 0.12/0.34 cnf(5, plain, ~takes_to_me(X0) | in_house(X0), inference(cnf, [status(esa)], [in_house_if_takes_to_me])). % 0.12/0.34 cnf(l3, plain, ~takes_to_me(the_kangaroo) | in_house(the_kangaroo), inference(instantiation, [status(thm)], [5])). % 0.12/0.34 cnf(0, plain, ~in_house(X0) | cat(X0), inference(cnf, [status(esa)], [only_cats_in_house])). % 0.12/0.34 cnf(l4, plain, ~in_house(the_kangaroo) | cat(the_kangaroo), inference(instantiation, [status(thm)], [0])). % 0.12/0.34 cnf(4, plain, ~cat(X0) | mouse_killer(X0), inference(cnf, [status(esa)], [cats_are_mice_killers])). % 0.12/0.34 cnf(l5, plain, ~cat(the_kangaroo) | mouse_killer(the_kangaroo), inference(instantiation, [status(thm)], [4])). % 0.12/0.34 % launching worker at depth: cnf(7, plain, ~mouse_killer(X0) | carnivore(X0), inference(cnf, [status(esa)], [mouse_killers_are_carnivores])). % 0.12/0.34 17 % 0.12/0.34 cnf(l6, plain, ~mouse_killer(the_kangaroo) | carnivore(the_kangaroo), inference(instantiation, [status(thm)], [7])). % 0.12/0.34 cnf(3, plain, ~carnivore(X0) | prowler(X0), inference(cnf, [status(esa)], [carnivores_are_prowlers])). % 0.12/0.34 cnf(l7, plain, ~carnivore(the_kangaroo) | prowler(the_kangaroo), inference(instantiation, [status(thm)], [3])). % 0.12/0.34 cnf(9, plain, ~prowler(X0) | gazer(X0), inference(cnf, [status(esa)], [prowlers_are_gazers])). % 0.12/0.34 cnf(l8, plain, ~prowler(the_kangaroo) | gazer(the_kangaroo), inference(instantiation, [status(thm)], [9])). % 0.12/0.34 cnf(1, plain, ~gazer(X0) | suitable_pet(X0), inference(cnf, [status(esa)], [gazers_are_suitable_pets])). % 0.12/0.34 cnf(l9, plain, ~gazer(the_kangaroo) | suitable_pet(the_kangaroo), inference(instantiation, [status(thm)], [1])). % 0.12/0.34 cnf(6, plain, ~suitable_pet(X0) | ~kangaroo(X0), inference(cnf, [status(esa)], [kangaroos_are_not_pets])). % 0.12/0.34 cnf(l10, plain, ~suitable_pet(the_kangaroo) | ~kangaroo(the_kangaroo), inference(instantiation, [status(thm)], [6])). % 0.12/0.34 cnf(10, plain, kangaroo(the_kangaroo), inference(cnf, [status(esa)], [kangaroo_is_a_kangaroo])). % 0.12/0.34 cnf(l11, plain, kangaroo(the_kangaroo), inference(instantiation, [status(thm)], [10])). % 0.12/0.34 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11])). % 0.12/0.34 % SZS output end CNFRefutation %------------------------------------------------------------------------------