%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN013-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:46:55 EDT 2024
% Result : Unsatisfiable 37.62s 37.79s
% Output : Refutation 37.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 20
% Syntax : Number of clauses : 67 ( 13 unt; 46 nHn; 63 RR)
% Number of literals : 177 ( 103 equ; 39 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-1 aty)
% Number of variables : 34 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(c_3,negated_conjecture,
k != m,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_3) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(c_2,negated_conjecture,
n != k,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_2) ).
cnf(c_1,negated_conjecture,
m != n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_1) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c_14,negated_conjecture,
( X20 = k
| X20 != m
| element(X20,k) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_14) ).
cnf(c8,plain,
( m = k
| element(m,k) ),
inference(resolution,[status(thm)],[c_14,reflexivity]) ).
cnf(c11,plain,
( element(m,k)
| k = m ),
inference(resolution,[status(thm)],[c8,symmetry]) ).
cnf(c15,plain,
element(m,k),
inference(resolution,[status(thm)],[c11,c_3]) ).
cnf(c_13,negated_conjecture,
( X41 = n
| ~ element(X41,n)
| X40 = n
| X40 = X41
| ~ element(X41,X40)
| ~ element(X40,X41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_13) ).
cnf(c87,plain,
( k = n
| ~ element(k,n)
| m = n
| m = k
| ~ element(k,m) ),
inference(resolution,[status(thm)],[c_13,c15]) ).
cnf(c_15,negated_conjecture,
( X22 = k
| X22 != n
| element(X22,k) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_15) ).
cnf(c19,plain,
( n = k
| element(n,k) ),
inference(resolution,[status(thm)],[c_15,reflexivity]) ).
cnf(c24,plain,
element(n,k),
inference(resolution,[status(thm)],[c19,c_2]) ).
cnf(c_8,negated_conjecture,
( X27 = m
| element(X27,m)
| X26 = m
| X26 = X27
| ~ element(X27,X26)
| ~ element(X26,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_8) ).
cnf(c38,plain,
( k = m
| element(k,m)
| n = m
| n = k
| ~ element(k,n) ),
inference(resolution,[status(thm)],[c_8,c24]) ).
cnf(c2,axiom,
( X31 != X29
| X32 != X30
| ~ element(X31,X32)
| element(X29,X30) ),
theory(equality) ).
cnf(c_11,negated_conjecture,
( X25 = n
| element(X25,n)
| element(X25,g(X25)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_11) ).
cnf(c30,plain,
( element(X46,n)
| element(X46,g(X46))
| n = X46 ),
inference(resolution,[status(thm)],[c_11,symmetry]) ).
cnf(c108,plain,
( element(k,n)
| element(k,g(k)) ),
inference(resolution,[status(thm)],[c30,c_2]) ).
cnf(c112,plain,
( element(k,n)
| k != X104
| g(k) != X103
| element(X104,X103) ),
inference(resolution,[status(thm)],[c108,c2]) ).
cnf(c_9,negated_conjecture,
( X36 = n
| element(X36,n)
| g(X36) != n ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_9) ).
cnf(c_10,negated_conjecture,
( X24 = n
| element(X24,n)
| g(X24) != X24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_10) ).
cnf(c_12,negated_conjecture,
( X28 = n
| element(X28,n)
| element(g(X28),X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_12) ).
cnf(c_16,negated_conjecture,
( X43 = k
| X43 = m
| X43 = n
| ~ element(X43,k) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_16) ).
cnf(c94,plain,
( g(k) = k
| g(k) = m
| g(k) = n
| k = n
| element(k,n) ),
inference(resolution,[status(thm)],[c_16,c_12]) ).
cnf(c1158,plain,
( g(k) = m
| g(k) = n
| k = n
| element(k,n) ),
inference(resolution,[status(thm)],[c94,c_10]) ).
cnf(c5599,plain,
( g(k) = m
| k = n
| element(k,n) ),
inference(resolution,[status(thm)],[c1158,c_9]) ).
cnf(c5748,plain,
( g(k) = m
| element(k,n)
| n = k ),
inference(resolution,[status(thm)],[c5599,symmetry]) ).
cnf(c5952,plain,
( g(k) = m
| element(k,n) ),
inference(resolution,[status(thm)],[c5748,c_2]) ).
cnf(c6039,plain,
( element(k,n)
| k != X658
| element(X658,m) ),
inference(resolution,[status(thm)],[c5952,c112]) ).
cnf(c6135,plain,
( element(k,n)
| element(k,m) ),
inference(resolution,[status(thm)],[c6039,reflexivity]) ).
cnf(c6141,plain,
( element(k,m)
| k = m
| n = m
| n = k ),
inference(resolution,[status(thm)],[c6135,c38]) ).
cnf(c8389,plain,
( element(k,m)
| n = m
| n = k ),
inference(resolution,[status(thm)],[c6141,c_3]) ).
cnf(c8642,plain,
( element(k,m)
| n = m ),
inference(resolution,[status(thm)],[c8389,c_2]) ).
cnf(c8733,plain,
( element(k,m)
| m = n ),
inference(resolution,[status(thm)],[c8642,symmetry]) ).
cnf(c8776,plain,
( m = n
| k = n
| ~ element(k,n)
| m = k ),
inference(resolution,[status(thm)],[c8733,c87]) ).
cnf(c8781,plain,
element(k,m),
inference(resolution,[status(thm)],[c8733,c_1]) ).
cnf(c_4,negated_conjecture,
( X5 = m
| ~ element(X5,m)
| f(X5) != m ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_4) ).
cnf(c8833,plain,
( k != X741
| m != X740
| element(X741,X740) ),
inference(resolution,[status(thm)],[c8781,c2]) ).
cnf(c8845,plain,
( k != X742
| element(X742,m) ),
inference(resolution,[status(thm)],[c8833,reflexivity]) ).
cnf(c_6,negated_conjecture,
( X21 = m
| ~ element(X21,m)
| element(X21,f(X21)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_6) ).
cnf(c8838,plain,
( k = m
| element(k,f(k)) ),
inference(resolution,[status(thm)],[c8781,c_6]) ).
cnf(c8995,plain,
element(k,f(k)),
inference(resolution,[status(thm)],[c8838,c_3]) ).
cnf(c9047,plain,
( k != X755
| f(k) != X754
| element(X755,X754) ),
inference(resolution,[status(thm)],[c8995,c2]) ).
cnf(c_7,negated_conjecture,
( X23 = m
| ~ element(X23,m)
| element(f(X23),X23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_7) ).
cnf(c8836,plain,
( k = m
| element(f(k),k) ),
inference(resolution,[status(thm)],[c8781,c_7]) ).
cnf(c8928,plain,
element(f(k),k),
inference(resolution,[status(thm)],[c8836,c_3]) ).
cnf(c8985,plain,
( f(k) = k
| f(k) = m
| f(k) = n ),
inference(resolution,[status(thm)],[c8928,c_16]) ).
cnf(c11249,plain,
( f(k) = k
| f(k) = m
| k != X1188
| element(X1188,n) ),
inference(resolution,[status(thm)],[c8985,c9047]) ).
cnf(c31337,plain,
( f(k) = k
| f(k) = m
| element(k,n) ),
inference(resolution,[status(thm)],[c11249,reflexivity]) ).
cnf(c31372,plain,
( f(k) = m
| element(k,n)
| k = f(k) ),
inference(resolution,[status(thm)],[c31337,symmetry]) ).
cnf(c31547,plain,
( f(k) = m
| element(k,n)
| element(f(k),m) ),
inference(resolution,[status(thm)],[c31372,c8845]) ).
cnf(c_5,negated_conjecture,
( X15 = m
| ~ element(X15,m)
| f(X15) != X15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_5) ).
cnf(c0,axiom,
( X14 != X13
| f(X14) = f(X13) ),
theory(equality) ).
cnf(c31380,plain,
( f(k) = m
| element(k,n)
| f(f(k)) = f(k) ),
inference(resolution,[status(thm)],[c31337,c0]) ).
cnf(c43956,plain,
( f(k) = m
| element(k,n)
| ~ element(f(k),m) ),
inference(resolution,[status(thm)],[c31380,c_5]) ).
cnf(c43968,plain,
( f(k) = m
| element(k,n) ),
inference(resolution,[status(thm)],[c43956,c31547]) ).
cnf(c43984,plain,
( element(k,n)
| k = m
| ~ element(k,m) ),
inference(resolution,[status(thm)],[c43968,c_4]) ).
cnf(c44242,plain,
( element(k,n)
| k = m ),
inference(resolution,[status(thm)],[c43984,c8781]) ).
cnf(c44260,plain,
element(k,n),
inference(resolution,[status(thm)],[c44242,c_3]) ).
cnf(c44328,plain,
( m = n
| k = n
| m = k ),
inference(resolution,[status(thm)],[c44260,c8776]) ).
cnf(c44984,plain,
( k = n
| m = k ),
inference(resolution,[status(thm)],[c44328,c_1]) ).
cnf(c45233,plain,
( m = k
| n = k ),
inference(resolution,[status(thm)],[c44984,symmetry]) ).
cnf(c45570,plain,
m = k,
inference(resolution,[status(thm)],[c45233,c_2]) ).
cnf(c45678,plain,
k = m,
inference(resolution,[status(thm)],[c45570,symmetry]) ).
cnf(c45728,plain,
$false,
inference(resolution,[status(thm)],[c45678,c_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SYN013-1 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n014.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 19:57:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 37.62/37.79 % Version: 1.5
% 37.62/37.79 % SZS status Unsatisfiable
% 37.62/37.79 % SZS output start CNFRefutation
% See solution above
% 37.62/37.79
% 37.62/37.79 % Initial clauses : 22
% 37.62/37.79 % Processed clauses : 803
% 37.62/37.79 % Factors computed : 132
% 37.62/37.79 % Resolvents computed: 45654
% 37.62/37.79 % Tautologies deleted: 20
% 37.62/37.79 % Forward subsumed : 2195
% 37.62/37.79 % Backward subsumed : 267
% 37.62/37.79 % -------- CPU Time ---------
% 37.62/37.79 % User time : 37.272 s
% 37.62/37.79 % System time : 0.154 s
% 37.62/37.79 % Total time : 37.426 s
%------------------------------------------------------------------------------