%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COL039-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:17:18 EDT 2024
% Result : Unsatisfiable 61.86s 62.11s
% Output : Refutation 61.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of clauses : 19 ( 12 unt; 0 nHn; 7 RR)
% Number of literals : 28 ( 27 equ; 10 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 41 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_fixed_point,negated_conjecture,
apply(X27,f(X27)) != apply(f(X27),apply(X27,f(X27))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_fixed_point) ).
cnf(transitivity,axiom,
( X14 != X13
| X13 != X12
| X14 = X12 ),
theory(equality) ).
cnf(o_definition,axiom,
apply(apply(o,X21),X20) = apply(X20,apply(X21,X20)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o_definition) ).
cnf(c17,plain,
( X86 != apply(apply(o,X88),X87)
| X86 = apply(X87,apply(X88,X87)) ),
inference(resolution,[status(thm)],[o_definition,transitivity]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X34 != X33
| X36 != X35
| apply(X34,X36) = apply(X33,X35) ),
theory(equality) ).
cnf(c36,plain,
( X41 != X40
| apply(X41,X42) = apply(X40,X42) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(b_definition,axiom,
apply(apply(apply(b,X10),X9),X8) = apply(X10,apply(X9,X8)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_definition) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(m_definition,axiom,
apply(m,X6) = apply(X6,X6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_definition) ).
cnf(c3,plain,
apply(X7,X7) = apply(m,X7),
inference(resolution,[status(thm)],[m_definition,symmetry]) ).
cnf(c34,plain,
( X106 != X105
| apply(X106,apply(X107,X107)) = apply(X105,apply(m,X107)) ),
inference(resolution,[status(thm)],[c0,c3]) ).
cnf(c166,plain,
apply(X109,apply(X108,X108)) = apply(X109,apply(m,X108)),
inference(resolution,[status(thm)],[c34,reflexivity]) ).
cnf(c177,plain,
apply(X112,apply(m,X113)) = apply(X112,apply(X113,X113)),
inference(resolution,[status(thm)],[c166,symmetry]) ).
cnf(c200,plain,
( X217 != apply(X219,apply(m,X218))
| X217 = apply(X219,apply(X218,X218)) ),
inference(resolution,[status(thm)],[c177,transitivity]) ).
cnf(c676,plain,
apply(apply(apply(b,X277),m),X278) = apply(X277,apply(X278,X278)),
inference(resolution,[status(thm)],[c200,b_definition]) ).
cnf(c962,plain,
apply(apply(apply(apply(b,X2383),m),X2385),X2384) = apply(apply(X2383,apply(X2385,X2385)),X2384),
inference(resolution,[status(thm)],[c676,c36]) ).
cnf(c24386,plain,
apply(apply(apply(apply(b,o),m),X4984),X4985) = apply(X4985,apply(apply(X4984,X4984),X4985)),
inference(resolution,[status(thm)],[c962,c17]) ).
cnf(c70091,plain,
$false,
inference(resolution,[status(thm)],[c24386,prove_fixed_point]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : COL039-1 : TPTP v8.1.2. Released v1.0.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n005.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:46:52 EDT 2024
% 0.15/0.36 % CPUTime :
% 61.86/62.11 % Version: 1.5
% 61.86/62.11 % SZS status Unsatisfiable
% 61.86/62.11 % SZS output start CNFRefutation
% See solution above
% 61.86/62.11
% 61.86/62.11 % Initial clauses : 9
% 61.86/62.11 % Processed clauses : 1046
% 61.86/62.11 % Factors computed : 2
% 61.86/62.11 % Resolvents computed: 70116
% 61.86/62.11 % Tautologies deleted: 2
% 61.86/62.11 % Forward subsumed : 2214
% 61.86/62.11 % Backward subsumed : 12
% 61.86/62.11 % -------- CPU Time ---------
% 61.86/62.11 % User time : 61.513 s
% 61.86/62.11 % System time : 0.195 s
% 61.86/62.11 % Total time : 61.708 s
%------------------------------------------------------------------------------