%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : PLA002-2 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 12:46:16 PM UTC 2025
% Result : Unsatisfiable 37.08s 5.00s
% Output : CNFRefutation 37.08s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named prove_you_can_get_to_a_in_a_situation)
% Comments :
%------------------------------------------------------------------------------
cnf(22,plain,
( ~ situation(X0)
| ~ at(a,X0) ),
inference(cnf,[status(esa)],[prove_you_can_get_to_a_in_a_situation]) ).
cnf(l0,plain,
( ~ situation(walk(a,drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))))))
| ~ at(a,walk(a,drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))))) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(16,plain,
( ~ situation(X0)
| situation(walk(X1,X0)) ),
inference(cnf,[status(esa)],[walk_situation]) ).
cnf(l1,plain,
( ~ situation(drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))))
| situation(walk(a,drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))))) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(3,plain,
( ~ situation(X0)
| ~ at(b,X0)
| at(a,walk(a,X0)) ),
inference(cnf,[status(esa)],[walk_b_to_a]) ).
cnf(l2,plain,
( ~ situation(drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))))
| ~ at(b,drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))))
| at(a,walk(a,drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(17,plain,
( ~ situation(X0)
| situation(drive(X1,X0)) ),
inference(cnf,[status(esa)],[drive_situation]) ).
cnf(l9,plain,
( ~ situation(walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))))
| situation(drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))))) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l4,plain,
( ~ situation(walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))))
| situation(drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))))) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l42,plain,
( ~ situation(climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))
| situation(walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(2,plain,
( ~ situation(X0)
| ~ at(a,X0)
| at(b,drive(b,X0)) ),
inference(cnf,[status(esa)],[drive_a_to_b]) ).
cnf(l3,plain,
( ~ situation(walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))))
| ~ at(a,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))))
| at(b,drive(b,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l12,plain,
( ~ situation(climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))
| situation(walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7,plain,
( ~ situation(climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))
| ~ at(b,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))
| at(a,walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(18,plain,
( ~ situation(X0)
| situation(climb(X1,X0)) ),
inference(cnf,[status(esa)],[climb_situation]) ).
cnf(l51,plain,
( ~ situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))
| situation(climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l5,plain,
( ~ situation(climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))
| situation(walk(a,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))))) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l16,plain,
( ~ situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))
| situation(climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l55,plain,
( ~ situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))
| situation(climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(20,plain,
( ~ situation(X0)
| situation(go(X1,X0)) ),
inference(cnf,[status(esa)],[go_situation]) ).
cnf(l79,plain,
( ~ situation(go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))
| situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l32,plain,
( ~ situation(go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))
| situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l13,plain,
( ~ situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))
| situation(climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l15,plain,
( ~ situation(go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))
| situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l137,plain,
( ~ situation(go(e,go(c,go(e,go(c,go(d,s0))))))
| situation(go(c,go(e,go(c,go(e,go(c,go(d,s0))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l64,plain,
( ~ situation(go(e,go(c,go(e,go(c,go(d,s0))))))
| situation(go(c,go(e,go(c,go(e,go(c,go(d,s0))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l72,plain,
( ~ situation(go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))
| situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(8,plain,
( ~ warm(X0)
| ~ situation(X0)
| ~ at(d,X0)
| at(b,climb(b,X0)) ),
inference(cnf,[status(esa)],[climb_mountain_d_to_b]) ).
cnf(l517,plain,
( ~ warm(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))
| ~ situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))
| ~ at(d,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))
| at(b,climb(b,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(9,plain,
( ~ situation(X0)
| ~ at(c,X0)
| at(d,go(d,X0)) ),
inference(cnf,[status(esa)],[go_c_to_d]) ).
cnf(l523,plain,
( ~ situation(go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))
| ~ at(c,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))
| at(d,go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(0,plain,
( ~ situation(X0)
| ~ situation(X1)
| warm(X0)
| cold(X1) ),
inference(cnf,[status(esa)],[warm_or_cold]) ).
cnf(l518,plain,
( ~ situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))
| ~ situation(go(c,go(d,s0)))
| warm(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))))
| cold(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l19,plain,
( ~ situation(go(e,go(c,go(e,go(c,go(d,s0))))))
| situation(go(c,go(e,go(c,go(e,go(c,go(d,s0))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l88,plain,
( ~ situation(go(e,go(c,go(e,go(c,go(d,s0))))))
| situation(go(c,go(e,go(c,go(e,go(c,go(d,s0))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l521,plain,
( ~ situation(go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))
| situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l522,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l178,plain,
( ~ situation(go(c,go(e,go(c,go(d,s0)))))
| situation(go(e,go(c,go(e,go(c,go(d,s0)))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l30,plain,
( ~ situation(go(c,go(e,go(c,go(d,s0)))))
| situation(go(e,go(c,go(e,go(c,go(d,s0)))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l543,plain,
( ~ situation(go(e,go(c,go(e,go(c,go(d,s0))))))
| situation(go(c,go(e,go(c,go(e,go(c,go(d,s0))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l530,plain,
( ~ situation(go(e,go(c,go(e,go(c,go(d,s0))))))
| situation(go(c,go(e,go(c,go(e,go(c,go(d,s0))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l564,plain,
( ~ situation(go(c,go(e,go(c,go(d,s0)))))
| situation(go(e,go(c,go(e,go(c,go(d,s0)))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(12,plain,
( ~ situation(X0)
| ~ at(e,X0)
| at(c,go(c,X0)) ),
inference(cnf,[status(esa)],[go_e_to_c]) ).
cnf(l528,plain,
( ~ situation(go(e,go(c,go(e,go(c,go(d,s0))))))
| ~ at(e,go(e,go(c,go(e,go(c,go(d,s0))))))
| at(c,go(c,go(e,go(c,go(e,go(c,go(d,s0))))))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l203,plain,
( ~ situation(go(c,go(e,go(c,go(d,s0)))))
| situation(go(e,go(c,go(e,go(c,go(d,s0)))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l531,plain,
( ~ situation(go(c,go(e,go(c,go(d,s0)))))
| situation(go(e,go(c,go(e,go(c,go(d,s0)))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l150,plain,
( ~ situation(go(c,go(e,go(c,go(d,s0)))))
| situation(go(e,go(c,go(e,go(c,go(d,s0)))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l547,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(15,plain,
situation(s0),
inference(cnf,[status(esa)],[initial_situation]) ).
cnf(l553,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(11,plain,
( ~ situation(X0)
| ~ at(c,X0)
| at(e,go(e,X0)) ),
inference(cnf,[status(esa)],[go_c_to_e]) ).
cnf(l542,plain,
( ~ situation(go(c,go(e,go(c,go(d,s0)))))
| ~ at(c,go(c,go(e,go(c,go(d,s0)))))
| at(e,go(e,go(c,go(e,go(c,go(d,s0)))))) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l524,plain,
( ~ situation(go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))
| situation(go(d,go(c,go(e,go(c,go(e,go(c,go(d,s0)))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l666,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| ~ at(e,go(e,go(c,go(d,s0))))
| at(c,go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l540,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| situation(go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(6,plain,
( ~ cold(X0)
| ~ situation(X0)
| ~ at(c,X0)
| at(b,skate(b,X0)) ),
inference(cnf,[status(esa)],[cross_river_c_to_b]) ).
cnf(l519,plain,
( ~ cold(go(c,go(d,s0)))
| ~ situation(go(c,go(d,s0)))
| ~ at(c,go(c,go(d,s0)))
| at(b,skate(b,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l269,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| situation(go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l532,plain,
( ~ situation(go(c,go(e,go(c,go(d,s0)))))
| situation(go(e,go(c,go(e,go(c,go(d,s0)))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(10,plain,
( ~ situation(X0)
| ~ at(d,X0)
| at(c,go(c,X0)) ),
inference(cnf,[status(esa)],[go_d_to_c]) ).
cnf(l525,plain,
( ~ situation(go(d,s0))
| ~ at(d,go(d,s0))
| at(c,go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l678,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l683,plain,
( ~ situation(go(c,go(d,s0)))
| ~ at(c,go(c,go(d,s0)))
| at(e,go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l668,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l537,plain,
( ~ situation(skate(b,go(c,go(d,s0))))
| ~ at(b,skate(b,go(c,go(d,s0))))
| at(a,walk(a,skate(b,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l526,plain,
( ~ situation(go(e,go(c,go(e,go(c,go(d,s0))))))
| situation(go(c,go(e,go(c,go(e,go(c,go(d,s0))))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l534,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| situation(go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l628,plain,
( ~ situation(walk(a,skate(b,go(c,go(d,s0)))))
| ~ at(a,walk(a,skate(b,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l541,plain,
( ~ situation(go(c,go(e,go(c,go(d,s0)))))
| situation(go(e,go(c,go(e,go(c,go(d,s0)))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l592,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(14,plain,
( ~ situation(X0)
| ~ at(f,X0)
| at(d,go(d,X0)) ),
inference(cnf,[status(esa)],[go_f_to_d]) ).
cnf(l536,plain,
( ~ situation(s0)
| ~ at(f,s0)
| at(d,go(d,s0)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l631,plain,
( ~ situation(skate(b,go(c,go(d,s0))))
| situation(walk(a,skate(b,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(21,plain,
at(f,s0),
inference(cnf,[status(esa)],[initial]) ).
cnf(l629,plain,
at(f,s0),
inference(instantiation,[status(thm)],[21]) ).
cnf(l669,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l529,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l82,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| situation(go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l533,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l672,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l546,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| situation(go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l589,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| situation(go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l195,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| situation(go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l676,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| situation(go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l210,plain,
( ~ situation(go(e,go(c,go(d,s0))))
| situation(go(c,go(e,go(c,go(d,s0))))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l686,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l549,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l344,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l113,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l226,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l597,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(19,plain,
( ~ situation(X0)
| situation(skate(X1,X0)) ),
inference(cnf,[status(esa)],[skate_situation]) ).
cnf(l560,plain,
( ~ situation(go(c,go(d,s0)))
| situation(skate(b,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l610,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l539,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l670,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l633,plain,
( ~ situation(go(c,go(d,s0)))
| situation(skate(b,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l677,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l300,plain,
( ~ situation(go(c,go(d,s0)))
| situation(go(e,go(c,go(d,s0)))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l241,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l651,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l554,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l400,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l559,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l574,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l520,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l712,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l401,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l303,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l699,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l690,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l544,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l757,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l545,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l785,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l624,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l698,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l768,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l952,plain,
( ~ situation(go(d,s0))
| ~ at(d,go(d,s0))
| at(c,go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l691,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l653,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l644,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l673,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l238,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l953,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l370,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l722,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l667,plain,
( ~ situation(go(d,s0))
| situation(go(c,go(d,s0))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l753,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l744,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l345,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l380,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l242,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l381,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l674,plain,
( ~ situation(s0)
| situation(go(d,s0)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l347,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l285,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l954,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l675,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l961,plain,
( ~ situation(s0)
| ~ at(f,s0)
| at(d,go(d,s0)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l975,plain,
situation(s0),
inference(instantiation,[status(thm)],[15]) ).
cnf(l995,plain,
at(f,s0),
inference(instantiation,[status(thm)],[21]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l9,l4,l42,l3,l12,l7,l51,l5,l16,l55,l79,l32,l13,l15,l137,l64,l72,l517,l523,l518,l19,l88,l521,l522,l178,l30,l543,l530,l564,l528,l203,l531,l150,l547,l553,l542,l524,l666,l540,l519,l269,l532,l525,l678,l683,l668,l537,l526,l534,l628,l541,l592,l536,l631,l629,l669,l529,l82,l533,l672,l546,l589,l195,l676,l210,l686,l549,l344,l113,l226,l597,l560,l610,l539,l670,l633,l677,l300,l241,l651,l554,l400,l559,l574,l520,l712,l401,l303,l699,l690,l544,l757,l545,l785,l624,l698,l768,l952,l691,l653,l644,l673,l238,l953,l370,l722,l667,l753,l744,l345,l380,l242,l381,l674,l347,l285,l954,l675,l961,l975,l995]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : PLA002-2 : TPTP v9.0.0. Released v1.0.0.
% 0.08/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.34 % Computer : n026.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Jul 21 15:07:19 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 3
% 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: 8
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.12/0.35 % launching worker at depth: 11
% 0.12/0.35 % launching worker at depth: 12
% 0.19/0.40 % launching worker at depth: 13
% 0.19/0.40 % launching worker at depth: 14
% 1.58/0.53 % launching worker at depth: 15
% 7.13/1.26 % launching worker at depth: 16
% 19.61/2.87 % launching worker at depth: 17
% 37.08/5.00 % SZS status Theorem for theBenchmark
% 37.08/5.00 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------