%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CAT004-4 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:16:57 EDT 2024
% Result : Unsatisfiable 42.57s 42.72s
% Output : Refutation 42.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 8
% Syntax : Number of clauses : 16 ( 9 unt; 0 nHn; 13 RR)
% Number of literals : 26 ( 25 equ; 11 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 : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 24 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_h_equals_g,negated_conjecture,
h != g,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_h_equals_g) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(cancellation_for_product1,plain,
( compose(X35,a) != X37
| compose(X36,a) != X37
| X35 = X36 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cancellation_for_product1) ).
cnf(c52,plain,
( compose(X81,a) != compose(X80,a)
| X81 = X80 ),
inference(resolution,[status(thm)],[cancellation_for_product1,reflexivity]) ).
cnf(cancellation_for_product2,plain,
( compose(X38,b) != X40
| compose(X39,b) != X40
| X38 = X39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cancellation_for_product2) ).
cnf(symmetry,axiom,
( X12 != X13
| X13 = X12 ),
theory(equality) ).
cnf(associativity_of_compose,axiom,
compose(X30,compose(X32,X31)) = compose(compose(X30,X32),X31),
file('/export/starexec/sandbox/benchmark/Axioms/CAT004-0.ax',associativity_of_compose) ).
cnf(c37,plain,
compose(compose(X71,X73),X72) = compose(X71,compose(X73,X72)),
inference(resolution,[status(thm)],[associativity_of_compose,symmetry]) ).
cnf(c281,plain,
( compose(X256,b) != compose(X257,compose(X255,b))
| X256 = compose(X257,X255) ),
inference(resolution,[status(thm)],[c37,cancellation_for_product2]) ).
cnf(h_ab_equals_g_ab,plain,
compose(h,compose(a,b)) = compose(g,compose(a,b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',h_ab_equals_g_ab) ).
cnf(transitivity,axiom,
( X42 != X44
| X44 != X43
| X42 = X43 ),
theory(equality) ).
cnf(c106,plain,
( X138 != compose(h,compose(a,b))
| X138 = compose(g,compose(a,b)) ),
inference(resolution,[status(thm)],[transitivity,h_ab_equals_g_ab]) ).
cnf(c978,plain,
compose(compose(h,a),b) = compose(g,compose(a,b)),
inference(resolution,[status(thm)],[c106,c37]) ).
cnf(c40544,plain,
compose(h,a) = compose(g,a),
inference(resolution,[status(thm)],[c978,c281]) ).
cnf(c47356,plain,
h = g,
inference(resolution,[status(thm)],[c40544,c52]) ).
cnf(c47449,plain,
$false,
inference(resolution,[status(thm)],[c47356,prove_h_equals_g]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : CAT004-4 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n029.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 21:03:23 EDT 2024
% 0.15/0.37 % CPUTime :
% 42.57/42.72 % Version: 1.5
% 42.57/42.72 % SZS status Unsatisfiable
% 42.57/42.72 % SZS output start CNFRefutation
% See solution above
% 42.57/42.72
% 42.57/42.72 % Initial clauses : 25
% 42.57/42.72 % Processed clauses : 1546
% 42.57/42.72 % Factors computed : 20
% 42.57/42.72 % Resolvents computed: 47432
% 42.57/42.72 % Tautologies deleted: 3
% 42.57/42.72 % Forward subsumed : 2689
% 42.57/42.72 % Backward subsumed : 13
% 42.57/42.72 % -------- CPU Time ---------
% 42.57/42.72 % User time : 42.235 s
% 42.57/42.72 % System time : 0.116 s
% 42.57/42.72 % Total time : 42.351 s
%------------------------------------------------------------------------------