%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : ANA016-2 : TPTP v8.1.2. Released v3.2.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:15:27 EDT 2024
% Result : Unsatisfiable 30.92s 31.10s
% Output : Refutation 30.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 13
% Syntax : Number of clauses : 29 ( 15 unt; 2 nHn; 16 RR)
% Number of literals : 48 ( 34 equ; 19 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty)
% Number of variables : 48 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_conjecture_2,negated_conjecture,
v_g(v_x) != c_times(v_c,c_times(c_HOL_Oinverse(v_c,t_a),v_g(v_x),t_a),t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
cnf(transitivity,axiom,
( X34 != X33
| X33 != X32
| X34 = X32 ),
theory(equality) ).
cnf(clsrel_Ring__and__Field_Ofield_21,axiom,
( ~ class_Ring__and__Field_Ofield(X4)
| class_OrderedGroup_Osemigroup__mult(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Ofield_21) ).
cnf(tfree_tcs,negated_conjecture,
class_Ring__and__Field_Oordered__field(t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_tcs) ).
cnf(clsrel_Ring__and__Field_Oordered__field_0,axiom,
( ~ class_Ring__and__Field_Oordered__field(X5)
| class_Ring__and__Field_Ofield(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__field_0) ).
cnf(c7,plain,
class_Ring__and__Field_Ofield(t_a),
inference(resolution,[status(thm)],[clsrel_Ring__and__Field_Oordered__field_0,tfree_tcs]) ).
cnf(c9,plain,
class_OrderedGroup_Osemigroup__mult(t_a),
inference(resolution,[status(thm)],[c7,clsrel_Ring__and__Field_Ofield_21]) ).
cnf(cls_OrderedGroup_Osemigroup__mult__class_Omult__assoc_0,axiom,
( ~ class_OrderedGroup_Osemigroup__mult(X17)
| c_times(c_times(X18,X20,X17),X19,X17) = c_times(X18,c_times(X20,X19,X17),X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Osemigroup__mult__class_Omult__assoc_0) ).
cnf(c14,plain,
c_times(c_times(X57,X58,t_a),X59,t_a) = c_times(X57,c_times(X58,X59,t_a),t_a),
inference(resolution,[status(thm)],[cls_OrderedGroup_Osemigroup__mult__class_Omult__assoc_0,c9]) ).
cnf(c61,plain,
( X196 != c_times(c_times(X197,X195,t_a),X194,t_a)
| X196 = c_times(X197,c_times(X195,X194,t_a),t_a) ),
inference(resolution,[status(thm)],[c14,transitivity]) ).
cnf(symmetry,axiom,
( X7 != X6
| X6 = X7 ),
theory(equality) ).
cnf(clsrel_Ring__and__Field_Ofield_12,axiom,
( ~ class_Ring__and__Field_Ofield(X3)
| class_OrderedGroup_Omonoid__mult(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Ofield_12) ).
cnf(c8,plain,
class_OrderedGroup_Omonoid__mult(t_a),
inference(resolution,[status(thm)],[c7,clsrel_Ring__and__Field_Ofield_12]) ).
cnf(cls_OrderedGroup_Omonoid__mult__class_Oaxioms__1_0,axiom,
( ~ class_OrderedGroup_Omonoid__mult(X8)
| c_times(c_1,X9,X8) = X9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Omonoid__mult__class_Oaxioms__1_0) ).
cnf(c11,plain,
c_times(c_1,X27,t_a) = X27,
inference(resolution,[status(thm)],[cls_OrderedGroup_Omonoid__mult__class_Oaxioms__1_0,c8]) ).
cnf(c29,plain,
( X64 != c_times(c_1,X63,t_a)
| X64 = X63 ),
inference(resolution,[status(thm)],[transitivity,c11]) ).
cnf(cls_conjecture_0,negated_conjecture,
v_c != c_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(cls_Ring__and__Field_Oright__inverse_0,axiom,
( ~ class_Ring__and__Field_Ofield(X28)
| X29 = c_0
| c_times(X29,c_HOL_Oinverse(X29,X28),X28) = c_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Ring__and__Field_Oright__inverse_0) ).
cnf(c22,plain,
( X62 = c_0
| c_times(X62,c_HOL_Oinverse(X62,t_a),t_a) = c_1 ),
inference(resolution,[status(thm)],[cls_Ring__and__Field_Oright__inverse_0,c7]) ).
cnf(c79,plain,
c_times(v_c,c_HOL_Oinverse(v_c,t_a),t_a) = c_1,
inference(resolution,[status(thm)],[c22,cls_conjecture_0]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c1,axiom,
( X50 != X49
| X46 != X45
| X48 != X47
| c_times(X50,X46,X48) = c_times(X49,X45,X47) ),
theory(equality) ).
cnf(c38,plain,
( X102 != X103
| X99 != X100
| c_times(X102,X99,X101) = c_times(X103,X100,X101) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(c244,plain,
( X157 != X156
| c_times(X157,X155,X158) = c_times(X156,X155,X158) ),
inference(resolution,[status(thm)],[c38,reflexivity]) ).
cnf(c500,plain,
c_times(c_times(v_c,c_HOL_Oinverse(v_c,t_a),t_a),X2072,X2071) = c_times(c_1,X2072,X2071),
inference(resolution,[status(thm)],[c244,c79]) ).
cnf(c66663,plain,
c_times(c_times(v_c,c_HOL_Oinverse(v_c,t_a),t_a),X2076,t_a) = X2076,
inference(resolution,[status(thm)],[c500,c29]) ).
cnf(c67024,plain,
X2077 = c_times(c_times(v_c,c_HOL_Oinverse(v_c,t_a),t_a),X2077,t_a),
inference(resolution,[status(thm)],[c66663,symmetry]) ).
cnf(c67295,plain,
X2079 = c_times(v_c,c_times(c_HOL_Oinverse(v_c,t_a),X2079,t_a),t_a),
inference(resolution,[status(thm)],[c67024,c61]) ).
cnf(c67396,plain,
$false,
inference(resolution,[status(thm)],[c67295,cls_conjecture_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : ANA016-2 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n029.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 17:16:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 30.92/31.10 % Version: 1.5
% 30.92/31.10 % SZS status Unsatisfiable
% 30.92/31.10 % SZS output start CNFRefutation
% See solution above
% 30.92/31.10
% 30.92/31.10 % Initial clauses : 19
% 30.92/31.10 % Processed clauses : 1010
% 30.92/31.10 % Factors computed : 24
% 30.92/31.10 % Resolvents computed: 67422
% 30.92/31.10 % Tautologies deleted: 6
% 30.92/31.10 % Forward subsumed : 782
% 30.92/31.10 % Backward subsumed : 56
% 30.92/31.10 % -------- CPU Time ---------
% 30.92/31.10 % User time : 30.523 s
% 30.92/31.10 % System time : 0.211 s
% 30.92/31.10 % Total time : 30.734 s
%------------------------------------------------------------------------------