%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HWV021-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:24:59 EDT 2024
% Result : Unsatisfiable 41.70s 41.92s
% Output : Refutation 41.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 8
% Syntax : Number of clauses : 18 ( 7 unt; 6 nHn; 16 RR)
% Number of literals : 41 ( 2 equ; 19 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 5 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(quest_3,negated_conjecture,
~ p_Reset(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
cnf(quest_2,negated_conjecture,
p_Rd(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
cnf(quest_4,negated_conjecture,
~ p_Empty(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_4) ).
cnf(axiom_15,axiom,
( X29 = n0
| gt(X29,n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_15) ).
cnf(axiom_24,axiom,
( int_level(X36) != n0
| p_Empty(X36) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_24) ).
cnf(c44,plain,
( p_Empty(X77)
| gt(int_level(X77),n0) ),
inference(resolution,[status(thm)],[axiom_24,axiom_15]) ).
cnf(c138,plain,
gt(int_level(t_139),n0),
inference(resolution,[status(thm)],[c44,quest_4]) ).
cnf(quest_1,negated_conjecture,
p_Rd_error(plus(t_139,n1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
cnf(axiom_52,axiom,
( p_Reset(X271)
| ~ p_Wr(X271)
| ~ p_Rd(X271)
| ~ gt(int_level(X271),n0)
| ~ p_Rd_error(plus(X271,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_52) ).
cnf(c769,plain,
( p_Reset(t_139)
| ~ p_Wr(t_139)
| ~ p_Rd(t_139)
| ~ gt(int_level(t_139),n0) ),
inference(resolution,[status(thm)],[axiom_52,quest_1]) ).
cnf(c25000,plain,
( p_Reset(t_139)
| ~ p_Wr(t_139)
| ~ p_Rd(t_139) ),
inference(resolution,[status(thm)],[c769,c138]) ).
cnf(c25037,plain,
( p_Reset(t_139)
| ~ p_Wr(t_139) ),
inference(resolution,[status(thm)],[c25000,quest_2]) ).
cnf(axiom_70,axiom,
( p_Reset(X392)
| p_Wr(X392)
| ~ p_Rd(X392)
| ~ gt(int_level(X392),n0)
| ~ p_Rd_error(plus(X392,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_70) ).
cnf(c1312,plain,
( p_Reset(t_139)
| p_Wr(t_139)
| ~ p_Rd(t_139)
| ~ gt(int_level(t_139),n0) ),
inference(resolution,[status(thm)],[axiom_70,quest_1]) ).
cnf(c51354,plain,
( p_Reset(t_139)
| p_Wr(t_139)
| ~ p_Rd(t_139) ),
inference(resolution,[status(thm)],[c1312,c138]) ).
cnf(c51406,plain,
( p_Reset(t_139)
| p_Wr(t_139) ),
inference(resolution,[status(thm)],[c51354,quest_2]) ).
cnf(c51469,plain,
p_Reset(t_139),
inference(resolution,[status(thm)],[c51406,c25037]) ).
cnf(c51513,plain,
$false,
inference(resolution,[status(thm)],[c51469,quest_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : HWV021-1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.37 % Computer : n013.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8042.1875MB
% 0.13/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Thu May 9 07:33:53 EDT 2024
% 0.13/0.37 % CPUTime :
% 41.70/41.92 % Version: 1.5
% 41.70/41.92 % SZS status Unsatisfiable
% 41.70/41.92 % SZS output start CNFRefutation
% See solution above
% 41.70/41.92
% 41.70/41.92 % Initial clauses : 116
% 41.70/41.92 % Processed clauses : 2450
% 41.70/41.92 % Factors computed : 23
% 41.70/41.92 % Resolvents computed: 51479
% 41.70/41.92 % Tautologies deleted: 10
% 41.70/41.92 % Forward subsumed : 1353
% 41.70/41.92 % Backward subsumed : 81
% 41.70/41.92 % -------- CPU Time ---------
% 41.70/41.92 % User time : 41.410 s
% 41.70/41.92 % System time : 0.139 s
% 41.70/41.92 % Total time : 41.549 s
%------------------------------------------------------------------------------