%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ047+1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:00:21 PM UTC 2026
% Result : Theorem 0.08s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ047+1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 03:42:13 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.39 % Refutation found
% 0.08/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.39 fof(f1,conjecture,(
% 0.08/0.39 ( ( p(south,south,south,south,start)& (! [T] :( p(south,north,south,north,T)=> p(north,north,south,north,go_alone(T)) ))& (! [T1] :( p(north,north,south,north,T1)=> p(south,north,south,north,go_alone(T1)) ))& (! [T2] :( p(south,south,north,south,T2)=> p(north,south,north,south,go_alone(T2)) ))& (! [T3] :( p(north,south,north,south,T3)=> p(south,south,north,south,go_alone(T3)) ))& (! [T4] :( p(south,south,south,north,T4)=> p(north,north,south,north,take_wolf(T4)) ))& (! [T5] :( p(north,north,south,north,T5)=> p(south,south,south,north,take_wolf(T5)) ))& (! [T6] :( p(south,south,north,south,T6)=> p(north,north,north,south,take_wolf(T6)) ))& (! [T7] :( p(north,north,north,south,T7)=> p(south,south,north,south,take_wolf(T7)) ))& (! [X,Y,U] :( p(south,X,south,Y,U)=> p(north,X,north,Y,take_goat(U)) ))& (! [X1,Y1,V] :( p(north,X1,north,Y1,V)=> p(south,X1,south,Y1,take_goat(V)) ))& (! [T8] :( p(south,north,south,south,T8)=> p(north,north,south,north,take_cabbage(T8)) ))& (! [T9] :( p(north,north,south,north,T9)=> p(south,north,south,south,take_cabbage(T9)) ))& (! [U1] :( p(south,south,north,south,U1)=> p(north,south,north,north,take_cabbage(U1)) ))& (! [V1] :( p(north,south,north,north,V1)=> p(south,south,north,south,take_cabbage(V1)) ) ))=> (? [Z] : p(north,north,north,north,Z) )) ),
% 0.08/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.39 fof(f2,negated_conjecture,(
% 0.08/0.39 ~(( ( p(south,south,south,south,start)& (! [T] :( p(south,north,south,north,T)=> p(north,north,south,north,go_alone(T)) ))& (! [T1] :( p(north,north,south,north,T1)=> p(south,north,south,north,go_alone(T1)) ))& (! [T2] :( p(south,south,north,south,T2)=> p(north,south,north,south,go_alone(T2)) ))& (! [T3] :( p(north,south,north,south,T3)=> p(south,south,north,south,go_alone(T3)) ))& (! [T4] :( p(south,south,south,north,T4)=> p(north,north,south,north,take_wolf(T4)) ))& (! [T5] :( p(north,north,south,north,T5)=> p(south,south,south,north,take_wolf(T5)) ))& (! [T6] :( p(south,south,north,south,T6)=> p(north,north,north,south,take_wolf(T6)) ))& (! [T7] :( p(north,north,north,south,T7)=> p(south,south,north,south,take_wolf(T7)) ))& (! [X,Y,U] :( p(south,X,south,Y,U)=> p(north,X,north,Y,take_goat(U)) ))& (! [X1,Y1,V] :( p(north,X1,north,Y1,V)=> p(south,X1,south,Y1,take_goat(V)) ))& (! [T8] :( p(south,north,south,south,T8)=> p(north,north,south,north,take_cabbage(T8)) ))& (! [T9] :( p(north,north,south,north,T9)=> p(south,north,south,south,take_cabbage(T9)) ))& (! [U1] :( p(south,south,north,south,U1)=> p(north,south,north,north,take_cabbage(U1)) ))& (! [V1] :( p(north,south,north,north,V1)=> p(south,south,north,south,take_cabbage(V1)) ) ))=> (? [Z] : p(north,north,north,north,Z) )) )),
% 0.08/0.39 inference(negated_conjecture,[status(cth)],[f1])).
% 0.08/0.39 fof(f3,plain,(
% 0.08/0.39 (((((((((((((((p(south,south,south,south,start)&(![T]: (~p(south,north,south,north,T)|p(north,north,south,north,go_alone(T)))))&(![T1]: (~p(north,north,south,north,T1)|p(south,north,south,north,go_alone(T1)))))&(![T2]: (~p(south,south,north,south,T2)|p(north,south,north,south,go_alone(T2)))))&(![T3]: (~p(north,south,north,south,T3)|p(south,south,north,south,go_alone(T3)))))&(![T4]: (~p(south,south,south,north,T4)|p(north,north,south,north,take_wolf(T4)))))&(![T5]: (~p(north,north,south,north,T5)|p(south,south,south,north,take_wolf(T5)))))&(![T6]: (~p(south,south,north,south,T6)|p(north,north,north,south,take_wolf(T6)))))&(![T7]: (~p(north,north,north,south,T7)|p(south,south,north,south,take_wolf(T7)))))&(![X,Y,U]: (~p(south,X,south,Y,U)|p(north,X,north,Y,take_goat(U)))))&(![X1,Y1,V]: (~p(north,X1,north,Y1,V)|p(south,X1,south,Y1,take_goat(V)))))&(![T8]: (~p(south,north,south,south,T8)|p(north,north,south,north,take_cabbage(T8)))))&(![T9]: (~p(north,north,south,north,T9)|p(south,north,south,south,take_cabbage(T9)))))&(![U1]: (~p(south,south,north,south,U1)|p(north,south,north,north,take_cabbage(U1)))))&(![V1]: (~p(north,south,north,north,V1)|p(south,south,north,south,take_cabbage(V1)))))&(![Z]: ~p(north,north,north,north,Z)))),
% 0.08/0.39 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.08/0.39 fof(f4,plain,(
% 0.08/0.39 p(south,south,south,south,start)),
% 0.08/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.39 fof(f6,plain,(
% 0.08/0.39 ![X0]: (~p(north,north,south,north,X0)|p(south,north,south,north,go_alone(X0)))),
% 0.08/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.39 fof(f8,plain,(
% 0.08/0.39 ![X0]: (~p(north,south,north,south,X0)|p(south,south,north,south,go_alone(X0)))),
% 0.08/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.39 fof(f11,plain,(
% 0.08/0.39 ![X0]: (~p(south,south,north,south,X0)|p(north,north,north,south,take_wolf(X0)))),
% 0.08/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.39 fof(f13,plain,(
% 0.08/0.39 ![X0,X1,X2]: (~p(south,X0,south,X1,X2)|p(north,X0,north,X1,take_goat(X2)))),
% 0.08/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.39 fof(f14,plain,(
% 0.08/0.39 ![X0,X1,X2]: (~p(north,X0,north,X1,X2)|p(south,X0,south,X1,take_goat(X2)))),
% 0.08/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.39 fof(f15,plain,(
% 0.08/0.39 ![X0]: (~p(south,north,south,south,X0)|p(north,north,south,north,take_cabbage(X0)))),
% 0.08/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.39 fof(f19,plain,(
% 0.08/0.39 ![X0]: (~p(north,north,north,north,X0))),
% 0.08/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.39 fof(f20,plain,(
% 0.08/0.39 ![X0]: (~p(south,north,south,north,X0))),
% 0.08/0.39 inference(resolution,[status(thm)],[f13,f19])).
% 0.08/0.39 fof(f22,plain,(
% 0.08/0.39 ![X0]: (~p(north,north,south,north,X0))),
% 0.08/0.39 inference(forward_subsumption_resolution,[status(thm)],[f6,f20])).
% 0.08/0.39 fof(f26,plain,(
% 0.08/0.39 ![X0]: (~p(south,north,south,south,X0))),
% 0.08/0.39 inference(forward_subsumption_resolution,[status(thm)],[f15,f22])).
% 0.08/0.39 fof(f27,plain,(
% 0.08/0.39 ![X0]: (~p(north,north,north,south,X0))),
% 0.08/0.39 inference(resolution,[status(thm)],[f26,f14])).
% 0.08/0.39 fof(f28,plain,(
% 0.08/0.39 ![X0]: (~p(south,south,north,south,X0))),
% 0.08/0.39 inference(backward_subsumption_resolution,[status(thm)],[f11,f27])).
% 0.08/0.39 fof(f30,plain,(
% 0.08/0.39 ![X0]: (~p(north,south,north,south,X0))),
% 0.08/0.39 inference(backward_subsumption_resolution,[status(thm)],[f8,f28])).
% 0.08/0.39 fof(f31,plain,(
% 0.08/0.39 ![X0]: (~p(south,south,south,south,X0))),
% 0.08/0.39 inference(resolution,[status(thm)],[f30,f13])).
% 0.08/0.39 fof(f33,plain,(
% 0.08/0.39 $false),
% 0.08/0.39 inference(backward_subsumption_resolution,[status(thm)],[f4,f31])).
% 0.08/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.41 % Elapsed time: 0.045801 seconds
% 0.08/0.41 % CPU time: 0.130266 seconds
% 0.08/0.41 % Total memory used: 45.697 MB
% 0.08/0.41 % Net memory used: 45.376 MB
%------------------------------------------------------------------------------