%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ047+1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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 : Thu May 9 17:37:42 EDT 2024
% Result : Theorem 0.77s 0.99s
% Output : Refutation 0.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PUZ047+1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n011.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 20:43:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.77/0.99 % Version: 1.5
% 0.77/0.99 % SZS status Theorem
% 0.77/0.99 % SZS output start CNFRefutation
% 0.77/0.99 fof(thm100,conjecture,(((((((((((((((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))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thm100)).
% 0.77/0.99 fof(c0,negated_conjecture,(~(((((((((((((((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)))),inference(assume_negation,[status(cth)],[thm100])).
% 0.77/0.99 fof(c1,negated_conjecture,(((((((((((((((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))),inference(fof_nnf,[status(thm)],[c0])).
% 0.77/0.99 fof(c3,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(((((((((((((((p(south,south,south,south,start)&(~p(south,north,south,north,X2)|p(north,north,south,north,go_alone(X2))))&(~p(north,north,south,north,X3)|p(south,north,south,north,go_alone(X3))))&(~p(south,south,north,south,X4)|p(north,south,north,south,go_alone(X4))))&(~p(north,south,north,south,X5)|p(south,south,north,south,go_alone(X5))))&(~p(south,south,south,north,X6)|p(north,north,south,north,take_wolf(X6))))&(~p(north,north,south,north,X7)|p(south,south,south,north,take_wolf(X7))))&(~p(south,south,north,south,X8)|p(north,north,north,south,take_wolf(X8))))&(~p(north,north,north,south,X9)|p(south,south,north,south,take_wolf(X9))))&(~p(south,X10,south,X11,X12)|p(north,X10,north,X11,take_goat(X12))))&(~p(north,X13,north,X14,X15)|p(south,X13,south,X14,take_goat(X15))))&(~p(south,north,south,south,X16)|p(north,north,south,north,take_cabbage(X16))))&(~p(north,north,south,north,X17)|p(south,north,south,south,take_cabbage(X17))))&(~p(south,south,north,south,X18)|p(north,south,north,north,take_cabbage(X18))))&(~p(north,south,north,north,X19)|p(south,south,north,south,take_cabbage(X19))))&~p(north,north,north,north,X20))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c2,negated_conjecture,(((((((((((((((p(south,south,south,south,start)&(![X2]:(~p(south,north,south,north,X2)|p(north,north,south,north,go_alone(X2)))))&(![X3]:(~p(north,north,south,north,X3)|p(south,north,south,north,go_alone(X3)))))&(![X4]:(~p(south,south,north,south,X4)|p(north,south,north,south,go_alone(X4)))))&(![X5]:(~p(north,south,north,south,X5)|p(south,south,north,south,go_alone(X5)))))&(![X6]:(~p(south,south,south,north,X6)|p(north,north,south,north,take_wolf(X6)))))&(![X7]:(~p(north,north,south,north,X7)|p(south,south,south,north,take_wolf(X7)))))&(![X8]:(~p(south,south,north,south,X8)|p(north,north,north,south,take_wolf(X8)))))&(![X9]:(~p(north,north,north,south,X9)|p(south,south,north,south,take_wolf(X9)))))&(![X10]:(![X11]:(![X12]:(~p(south,X10,south,X11,X12)|p(north,X10,north,X11,take_goat(X12)))))))&(![X13]:(![X14]:(![X15]:(~p(north,X13,north,X14,X15)|p(south,X13,south,X14,take_goat(X15)))))))&(![X16]:(~p(south,north,south,south,X16)|p(north,north,south,north,take_cabbage(X16)))))&(![X17]:(~p(north,north,south,north,X17)|p(south,north,south,south,take_cabbage(X17)))))&(![X18]:(~p(south,south,north,south,X18)|p(north,south,north,north,take_cabbage(X18)))))&(![X19]:(~p(north,south,north,north,X19)|p(south,south,north,south,take_cabbage(X19)))))&(![X20]:~p(north,north,north,north,X20))),inference(variable_rename,[status(thm)],[c1])).])).
% 0.77/0.99 cnf(c19,negated_conjecture,~p(north,north,north,north,X21),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.99 cnf(c13,negated_conjecture,~p(south,X24,south,X22,X23)|p(north,X24,north,X22,take_goat(X23)),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.99 cnf(c6,negated_conjecture,~p(north,north,south,north,X29)|p(south,north,south,north,go_alone(X29)),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.99 cnf(c14,negated_conjecture,~p(north,X27,north,X25,X26)|p(south,X27,south,X25,take_goat(X26)),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.99 cnf(c4,negated_conjecture,p(south,south,south,south,start),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.99 cnf(c20,plain,p(north,south,north,south,take_goat(start)),inference(resolution,[status(thm)],[c13, c4])).
% 0.77/0.99 cnf(c8,negated_conjecture,~p(north,south,north,south,X31)|p(south,south,north,south,go_alone(X31)),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.99 cnf(c27,plain,p(south,south,north,south,go_alone(take_goat(start))),inference(resolution,[status(thm)],[c8, c20])).
% 0.77/0.99 cnf(c11,negated_conjecture,~p(south,south,north,south,X34)|p(north,north,north,south,take_wolf(X34)),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.99 cnf(c41,plain,p(north,north,north,south,take_wolf(go_alone(take_goat(start)))),inference(resolution,[status(thm)],[c11, c27])).
% 0.77/0.99 cnf(c44,plain,p(south,north,south,south,take_goat(take_wolf(go_alone(take_goat(start))))),inference(resolution,[status(thm)],[c41, c14])).
% 0.77/0.99 cnf(c15,negated_conjecture,~p(south,north,south,south,X36)|p(north,north,south,north,take_cabbage(X36)),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.99 cnf(c59,plain,p(north,north,south,north,take_cabbage(take_goat(take_wolf(go_alone(take_goat(start)))))),inference(resolution,[status(thm)],[c15, c44])).
% 0.77/0.99 cnf(c61,plain,p(south,north,south,north,go_alone(take_cabbage(take_goat(take_wolf(go_alone(take_goat(start))))))),inference(resolution,[status(thm)],[c59, c6])).
% 0.77/0.99 cnf(c133,plain,p(north,north,north,north,take_goat(go_alone(take_cabbage(take_goat(take_wolf(go_alone(take_goat(start)))))))),inference(resolution,[status(thm)],[c61, c13])).
% 0.77/0.99 cnf(c266,plain,$false,inference(resolution,[status(thm)],[c133, c19])).
% 0.77/0.99 % SZS output end CNFRefutation
% 0.77/0.99
% 0.77/0.99 % Initial clauses : 16
% 0.77/0.99 % Processed clauses : 130
% 0.77/0.99 % Factors computed : 0
% 0.77/0.99 % Resolvents computed: 248
% 0.77/0.99 % Tautologies deleted: 0
% 0.77/0.99 % Forward subsumed : 0
% 0.77/0.99 % Backward subsumed : 0
% 0.77/0.99 % -------- CPU Time ---------
% 0.77/0.99 % User time : 0.613 s
% 0.77/0.99 % System time : 0.016 s
% 0.77/0.99 % Total time : 0.629 s
%------------------------------------------------------------------------------