%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LDA003-1 : TPTP v8.1.2. Released v1.0.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:32:52 EDT 2024
% Result : Unsatisfiable 1.34s 1.50s
% Output : Refutation 1.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of clauses : 28 ( 17 unt; 0 nHn; 23 RR)
% Number of literals : 44 ( 36 equ; 17 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 38 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_equation,negated_conjecture,
~ left(n3,u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_equation) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(a2,axiom,
left(X4,f(X4,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2) ).
cnf(c1,axiom,
( X40 != X37
| X38 != X39
| ~ left(X40,X38)
| left(X37,X39) ),
theory(equality) ).
cnf(c41,plain,
( X74 != X73
| f(X74,X76) != X75
| left(X73,X75) ),
inference(resolution,[status(thm)],[c1,a2]) ).
cnf(transitivity,axiom,
( X17 != X16
| X16 != X15
| X17 = X15 ),
theory(equality) ).
cnf(symmetry,axiom,
( X6 != X5
| X5 = X6 ),
theory(equality) ).
cnf(a1,axiom,
f(X10,f(X9,X8)) = f(f(X10,X9),f(X10,X8)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
cnf(c3,plain,
f(f(X44,X43),f(X44,X45)) = f(X44,f(X43,X45)),
inference(resolution,[status(thm)],[a1,symmetry]) ).
cnf(c46,plain,
( X174 != f(f(X176,X175),f(X176,X173))
| X174 = f(X176,f(X175,X173)) ),
inference(resolution,[status(thm)],[c3,transitivity]) ).
cnf(clause_5,axiom,
n3 = f(n2,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
cnf(c0,axiom,
( X34 != X31
| X32 != X33
| f(X34,X32) = f(X31,X33) ),
theory(equality) ).
cnf(c26,plain,
( X60 != X61
| f(X60,X60) = f(X61,X61) ),
inference(factor,[status(thm)],[c0]) ).
cnf(c62,plain,
f(n3,n3) = f(f(n2,n1),f(n2,n1)),
inference(resolution,[status(thm)],[c26,clause_5]) ).
cnf(c545,plain,
f(n3,n3) = f(n2,f(n1,n1)),
inference(resolution,[status(thm)],[c62,c46]) ).
cnf(clause_6,axiom,
u = f(n2,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
cnf(c6,plain,
f(n2,n2) = u,
inference(resolution,[status(thm)],[clause_6,symmetry]) ).
cnf(c19,plain,
( X46 != f(n2,n2)
| X46 = u ),
inference(resolution,[status(thm)],[transitivity,c6]) ).
cnf(clause_4,axiom,
n2 = f(n1,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
cnf(c4,plain,
f(n1,n1) = n2,
inference(resolution,[status(thm)],[clause_4,symmetry]) ).
cnf(c27,plain,
( X85 != X86
| f(X85,f(n1,n1)) = f(X86,n2) ),
inference(resolution,[status(thm)],[c0,c4]) ).
cnf(c114,plain,
f(X312,f(n1,n1)) = f(X312,n2),
inference(resolution,[status(thm)],[c27,reflexivity]) ).
cnf(c691,plain,
f(n2,f(n1,n1)) = u,
inference(resolution,[status(thm)],[c114,c19]) ).
cnf(c735,plain,
( X856 != f(n2,f(n1,n1))
| X856 = u ),
inference(resolution,[status(thm)],[c691,transitivity]) ).
cnf(c2108,plain,
f(n3,n3) = u,
inference(resolution,[status(thm)],[c735,c545]) ).
cnf(c2117,plain,
( n3 != X859
| left(X859,u) ),
inference(resolution,[status(thm)],[c2108,c41]) ).
cnf(c2153,plain,
left(n3,u),
inference(resolution,[status(thm)],[c2117,reflexivity]) ).
cnf(c2161,plain,
$false,
inference(resolution,[status(thm)],[c2153,prove_equation]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : LDA003-1 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n011.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 21:10:08 EDT 2024
% 0.15/0.36 % CPUTime :
% 1.34/1.50 % Version: 1.5
% 1.34/1.50 % SZS status Unsatisfiable
% 1.34/1.50 % SZS output start CNFRefutation
% See solution above
% 1.34/1.50
% 1.34/1.50 % Initial clauses : 12
% 1.34/1.50 % Processed clauses : 255
% 1.34/1.50 % Factors computed : 3
% 1.34/1.50 % Resolvents computed: 2180
% 1.34/1.50 % Tautologies deleted: 3
% 1.34/1.50 % Forward subsumed : 252
% 1.34/1.50 % Backward subsumed : 3
% 1.34/1.50 % -------- CPU Time ---------
% 1.34/1.50 % User time : 1.114 s
% 1.34/1.50 % System time : 0.024 s
% 1.34/1.50 % Total time : 1.138 s
%------------------------------------------------------------------------------