%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LDA007-3 : 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:32:53 EDT 2024
% Result : Unsatisfiable 2.72s 2.94s
% Output : Refutation 2.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of clauses : 46 ( 31 unt; 0 nHn; 34 RR)
% Number of literals : 63 ( 62 equ; 18 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 50 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_equation,negated_conjecture,
f(t,tsk) != f(tt_ts,tk),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_equation) ).
cnf(a1,axiom,
f(X8,f(X6,X7)) = f(f(X8,X6),f(X8,X7)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
cnf(transitivity,axiom,
( X11 != X9
| X9 != X10
| X11 = X10 ),
theory(equality) ).
cnf(c22,plain,
( X32 != f(X34,f(X31,X33))
| X32 = f(f(X34,X31),f(X34,X33)) ),
inference(resolution,[status(thm)],[transitivity,a1]) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(clause_5,axiom,
tsk = f(ts,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5) ).
cnf(c7,plain,
f(ts,k) = tsk,
inference(resolution,[status(thm)],[clause_5,symmetry]) ).
cnf(c0,axiom,
( X15 != X16
| X17 != X18
| f(X15,X17) = f(X16,X18) ),
theory(equality) ).
cnf(c32,plain,
( X60 != X61
| f(X60,f(ts,k)) = f(X61,tsk) ),
inference(resolution,[status(thm)],[c0,c7]) ).
cnf(c264,plain,
f(X85,f(ts,k)) = f(X85,tsk),
inference(resolution,[status(thm)],[c32,reflexivity]) ).
cnf(c456,plain,
f(X98,tsk) = f(X98,f(ts,k)),
inference(resolution,[status(thm)],[c264,symmetry]) ).
cnf(c613,plain,
f(X161,tsk) = f(f(X161,ts),f(X161,k)),
inference(resolution,[status(thm)],[c456,c22]) ).
cnf(clause_4,axiom,
tk = f(t,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4) ).
cnf(c6,plain,
f(t,k) = tk,
inference(resolution,[status(thm)],[clause_4,symmetry]) ).
cnf(c28,plain,
( X46 != X47
| f(X46,f(t,k)) = f(X47,tk) ),
inference(resolution,[status(thm)],[c0,c6]) ).
cnf(c106,plain,
f(X65,f(t,k)) = f(X65,tk),
inference(resolution,[status(thm)],[c28,reflexivity]) ).
cnf(c326,plain,
( X241 != f(X240,f(t,k))
| X241 = f(X240,tk) ),
inference(resolution,[status(thm)],[c106,transitivity]) ).
cnf(c2523,plain,
f(t,tsk) = f(f(t,ts),tk),
inference(resolution,[status(thm)],[c326,c613]) ).
cnf(c29,plain,
( X41 != X43
| f(X41,X42) = f(X43,X42) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(clause_2,axiom,
ts = f(t,s),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2) ).
cnf(c31,plain,
( X57 != X58
| f(X57,ts) = f(X58,f(t,s)) ),
inference(resolution,[status(thm)],[c0,clause_2]) ).
cnf(c204,plain,
f(X78,ts) = f(X78,f(t,s)),
inference(resolution,[status(thm)],[c31,reflexivity]) ).
cnf(c4,plain,
f(f(X23,X21),f(X23,X22)) = f(X23,f(X21,X22)),
inference(resolution,[status(thm)],[a1,symmetry]) ).
cnf(c45,plain,
( X122 != f(f(X121,X123),f(X121,X120))
| X122 = f(X121,f(X123,X120)) ),
inference(resolution,[status(thm)],[c4,transitivity]) ).
cnf(c3,plain,
f(t,s) = ts,
inference(resolution,[status(thm)],[clause_2,symmetry]) ).
cnf(c33,plain,
( X66 != X67
| f(X66,f(t,s)) = f(X67,ts) ),
inference(resolution,[status(thm)],[c0,c3]) ).
cnf(c332,plain,
f(X92,f(t,s)) = f(X92,ts),
inference(resolution,[status(thm)],[c33,reflexivity]) ).
cnf(clause_3,axiom,
tt_ts = f(tt,ts),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3) ).
cnf(c5,plain,
f(tt,ts) = tt_ts,
inference(resolution,[status(thm)],[clause_3,symmetry]) ).
cnf(c17,plain,
( X24 != f(tt,ts)
| X24 = tt_ts ),
inference(resolution,[status(thm)],[transitivity,c5]) ).
cnf(clause_1,axiom,
tt = f(t,t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1) ).
cnf(c2,plain,
f(t,t) = tt,
inference(resolution,[status(thm)],[clause_1,symmetry]) ).
cnf(c98,plain,
f(f(t,t),X59) = f(tt,X59),
inference(resolution,[status(thm)],[c29,c2]) ).
cnf(c237,plain,
f(f(t,t),ts) = tt_ts,
inference(resolution,[status(thm)],[c98,c17]) ).
cnf(c250,plain,
( X119 != f(f(t,t),ts)
| X119 = tt_ts ),
inference(resolution,[status(thm)],[c237,transitivity]) ).
cnf(c720,plain,
f(f(t,t),f(t,s)) = tt_ts,
inference(resolution,[status(thm)],[c250,c332]) ).
cnf(c802,plain,
tt_ts = f(f(t,t),f(t,s)),
inference(resolution,[status(thm)],[c720,symmetry]) ).
cnf(c859,plain,
tt_ts = f(t,f(t,s)),
inference(resolution,[status(thm)],[c802,c45]) ).
cnf(c878,plain,
f(t,f(t,s)) = tt_ts,
inference(resolution,[status(thm)],[c859,symmetry]) ).
cnf(c890,plain,
( X140 != f(t,f(t,s))
| X140 = tt_ts ),
inference(resolution,[status(thm)],[c878,transitivity]) ).
cnf(c980,plain,
f(t,ts) = tt_ts,
inference(resolution,[status(thm)],[c890,c204]) ).
cnf(c1010,plain,
f(f(t,ts),X143) = f(tt_ts,X143),
inference(resolution,[status(thm)],[c980,c29]) ).
cnf(c1144,plain,
( X347 != f(f(t,ts),X348)
| X347 = f(tt_ts,X348) ),
inference(resolution,[status(thm)],[c1010,transitivity]) ).
cnf(c5217,plain,
f(t,tsk) = f(tt_ts,tk),
inference(resolution,[status(thm)],[c1144,c2523]) ).
cnf(c5265,plain,
$false,
inference(resolution,[status(thm)],[c5217,prove_equation]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.09 % Problem : LDA007-3 : TPTP v8.1.2. Released v1.0.0.
% 0.03/0.10 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Wed May 8 21:08:22 EDT 2024
% 0.10/0.29 % CPUTime :
% 2.72/2.94 % Version: 1.5
% 2.72/2.94 % SZS status Unsatisfiable
% 2.72/2.94 % SZS output start CNFRefutation
% See solution above
% 2.72/2.94
% 2.72/2.94 % Initial clauses : 11
% 2.72/2.94 % Processed clauses : 265
% 2.72/2.94 % Factors computed : 2
% 2.72/2.94 % Resolvents computed: 5274
% 2.72/2.94 % Tautologies deleted: 2
% 2.72/2.94 % Forward subsumed : 292
% 2.72/2.94 % Backward subsumed : 0
% 2.72/2.94 % -------- CPU Time ---------
% 2.72/2.94 % User time : 2.614 s
% 2.72/2.94 % System time : 0.027 s
% 2.72/2.94 % Total time : 2.641 s
%------------------------------------------------------------------------------