%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN072-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:47:17 EDT 2024
% Result : Unsatisfiable 0.61s 0.77s
% Output : Refutation 0.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 8
% Syntax : Number of clauses : 32 ( 10 unt; 17 nHn; 22 RR)
% Number of literals : 61 ( 33 equ; 14 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 21 ( 3 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_this,negated_conjecture,
~ big_p(e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
cnf(c0,axiom,
( X8 != X7
| ~ big_p(X8)
| big_p(X7) ),
theory(equality) ).
cnf(symmetry,axiom,
( X4 != X5
| X5 = X4 ),
theory(equality) ).
cnf(clause_1,axiom,
( X3 = c
| X3 = d ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
cnf(c1,plain,
( c = X10
| X10 = d ),
inference(resolution,[status(thm)],[symmetry,clause_1]) ).
cnf(c9,plain,
( c = X19
| d = X19 ),
inference(resolution,[status(thm)],[c1,symmetry]) ).
cnf(c25,plain,
( d = X40
| ~ big_p(c)
| big_p(X40) ),
inference(resolution,[status(thm)],[c9,c0]) ).
cnf(clause_4,axiom,
a != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
cnf(clause_3,axiom,
big_p(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
cnf(c4,plain,
( ~ big_p(X20)
| big_p(c)
| X20 = d ),
inference(resolution,[status(thm)],[c0,clause_1]) ).
cnf(c30,plain,
( big_p(c)
| b = d ),
inference(resolution,[status(thm)],[c4,clause_3]) ).
cnf(transitivity,axiom,
( X12 != X13
| X13 != X11
| X12 = X11 ),
theory(equality) ).
cnf(clause_2,axiom,
big_p(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
cnf(c29,plain,
( big_p(c)
| a = d ),
inference(resolution,[status(thm)],[c4,clause_2]) ).
cnf(c32,plain,
( big_p(c)
| d = a ),
inference(resolution,[status(thm)],[c29,symmetry]) ).
cnf(c46,plain,
( big_p(c)
| X88 != d
| X88 = a ),
inference(resolution,[status(thm)],[c32,transitivity]) ).
cnf(c416,plain,
( big_p(c)
| b = a ),
inference(resolution,[status(thm)],[c46,c30]) ).
cnf(c424,plain,
( big_p(c)
| a = b ),
inference(resolution,[status(thm)],[c416,symmetry]) ).
cnf(c443,plain,
big_p(c),
inference(resolution,[status(thm)],[c424,clause_4]) ).
cnf(c446,plain,
( d = X89
| big_p(X89) ),
inference(resolution,[status(thm)],[c443,c25]) ).
cnf(c456,plain,
( big_p(X90)
| ~ big_p(d) ),
inference(resolution,[status(thm)],[c446,c0]) ).
cnf(c14,plain,
( X42 != c
| X42 = X43
| X43 = d ),
inference(resolution,[status(thm)],[transitivity,c1]) ).
cnf(c5,plain,
( ~ big_p(X25)
| big_p(d)
| X25 = c ),
inference(resolution,[status(thm)],[c0,clause_1]) ).
cnf(c36,plain,
( big_p(d)
| a = c ),
inference(resolution,[status(thm)],[c5,clause_2]) ).
cnf(c484,plain,
( big_p(X96)
| a = c ),
inference(resolution,[status(thm)],[c456,c36]) ).
cnf(c510,plain,
a = c,
inference(resolution,[status(thm)],[c484,prove_this]) ).
cnf(c525,plain,
( a = X123
| X123 = d ),
inference(resolution,[status(thm)],[c510,c14]) ).
cnf(c688,plain,
b = d,
inference(resolution,[status(thm)],[c525,clause_4]) ).
cnf(c709,plain,
( ~ big_p(b)
| big_p(d) ),
inference(resolution,[status(thm)],[c688,c0]) ).
cnf(c739,plain,
big_p(d),
inference(resolution,[status(thm)],[c709,clause_3]) ).
cnf(c743,plain,
big_p(X125),
inference(resolution,[status(thm)],[c739,c456]) ).
cnf(c744,plain,
$false,
inference(resolution,[status(thm)],[c743,prove_this]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SYN072-1 : TPTP v8.1.2. Released v1.0.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 20:25:07 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.61/0.77 % Version: 1.5
% 0.61/0.77 % SZS status Unsatisfiable
% 0.61/0.77 % SZS output start CNFRefutation
% See solution above
% 0.61/0.78
% 0.61/0.78 % Initial clauses : 9
% 0.61/0.78 % Processed clauses : 79
% 0.61/0.78 % Factors computed : 5
% 0.61/0.78 % Resolvents computed: 739
% 0.61/0.78 % Tautologies deleted: 10
% 0.61/0.78 % Forward subsumed : 131
% 0.61/0.78 % Backward subsumed : 46
% 0.61/0.78 % -------- CPU Time ---------
% 0.61/0.78 % User time : 0.416 s
% 0.61/0.78 % System time : 0.012 s
% 0.61/0.78 % Total time : 0.428 s
%------------------------------------------------------------------------------