%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ003-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:33 EDT 2024
% Result : Unsatisfiable 0.16s 0.46s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 8
% Syntax : Number of clauses : 19 ( 11 unt; 0 nHn; 19 RR)
% Number of literals : 32 ( 0 equ; 14 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 6 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_petruchio_has_shaved_lorenzo,negated_conjecture,
~ shaved(petruchio,lorenzo),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_petruchio_has_shaved_lorenzo) ).
cnf(petruchio,plain,
member(petruchio),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',petruchio) ).
cnf(all_shaved_then_one_shaved,axiom,
( ~ shaved(members,X4)
| ~ member(X5)
| shaved(X5,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',all_shaved_then_one_shaved) ).
cnf(lorenzo,plain,
member(lorenzo),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lorenzo) ).
cnf(guido,plain,
member(guido),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guido) ).
cnf(one_shaved_then_all_shaved,axiom,
( ~ member(X2)
| ~ member(X3)
| ~ shaved(X2,X3)
| shaved(members,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',one_shaved_then_all_shaved) ).
cnf(cesare,plain,
member(cesare),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cesare) ).
cnf(guido_has_shaved_cesare,plain,
shaved(guido,cesare),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guido_has_shaved_cesare) ).
cnf(c0,plain,
( ~ member(guido)
| ~ member(cesare)
| shaved(members,guido) ),
inference(resolution,[status(thm)],[one_shaved_then_all_shaved,guido_has_shaved_cesare]) ).
cnf(c1,plain,
( ~ member(guido)
| shaved(members,guido) ),
inference(resolution,[status(thm)],[c0,cesare]) ).
cnf(c2,plain,
shaved(members,guido),
inference(resolution,[status(thm)],[c1,guido]) ).
cnf(c3,plain,
( ~ member(X6)
| shaved(X6,guido) ),
inference(resolution,[status(thm)],[c2,all_shaved_then_one_shaved]) ).
cnf(c7,plain,
shaved(lorenzo,guido),
inference(resolution,[status(thm)],[c3,lorenzo]) ).
cnf(c11,plain,
( ~ member(lorenzo)
| ~ member(guido)
| shaved(members,lorenzo) ),
inference(resolution,[status(thm)],[c7,one_shaved_then_all_shaved]) ).
cnf(c22,plain,
( ~ member(lorenzo)
| shaved(members,lorenzo) ),
inference(resolution,[status(thm)],[c11,guido]) ).
cnf(c26,plain,
shaved(members,lorenzo),
inference(resolution,[status(thm)],[c22,lorenzo]) ).
cnf(c28,plain,
( ~ member(X8)
| shaved(X8,lorenzo) ),
inference(resolution,[status(thm)],[c26,all_shaved_then_one_shaved]) ).
cnf(c33,plain,
shaved(petruchio,lorenzo),
inference(resolution,[status(thm)],[c28,petruchio]) ).
cnf(c37,plain,
$false,
inference(resolution,[status(thm)],[c33,prove_petruchio_has_shaved_lorenzo]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : PUZ003-1 : TPTP v8.1.2. Released v1.0.0.
% 0.00/0.11 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.30 % Computer : n032.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 300
% 0.11/0.30 % DateTime : Wed May 8 20:42:07 EDT 2024
% 0.11/0.31 % CPUTime :
% 0.16/0.46 % Version: 1.5
% 0.16/0.46 % SZS status Unsatisfiable
% 0.16/0.46 % SZS output start CNFRefutation
% See solution above
% 0.16/0.46
% 0.16/0.46 % Initial clauses : 8
% 0.16/0.46 % Processed clauses : 34
% 0.16/0.46 % Factors computed : 0
% 0.16/0.46 % Resolvents computed: 39
% 0.16/0.46 % Tautologies deleted: 0
% 0.16/0.46 % Forward subsumed : 3
% 0.16/0.46 % Backward subsumed : 7
% 0.16/0.46 % -------- CPU Time ---------
% 0.16/0.46 % User time : 0.139 s
% 0.16/0.46 % System time : 0.014 s
% 0.16/0.46 % Total time : 0.153 s
%------------------------------------------------------------------------------