%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ANA045-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:02:19 PM UTC 2026
% Result : Unsatisfiable 3.08s 1.04s
% Output : CNFRefutation 3.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 7
% Syntax : Number of formulae : 23 ( 15 unt; 0 def)
% Number of atoms : 33 ( 9 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 23 ( 13 ~; 10 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 16 ( 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f268,axiom,
c_IntDef_Oint(c_0) = c_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f271,axiom,
c_lessequals(c_IntDef_Oint(c_0),c_0,tc_IntDef_Oint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f290,axiom,
! [T_a] :
( c_0 = c_IntDef_Oof__int(c_0,T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f292,axiom,
! [T_a,V_z] :
( c_lessequals(c_0,c_IntDef_Oof__int(V_z,T_a),T_a)
| ~ c_lessequals(c_0,V_z,tc_IntDef_Oint)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1363,axiom,
! [T_a,V_b] :
( c_0 = c_times(c_0,V_b,T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2783,negated_conjecture,
! [V_U] : ~ c_lessequals(c_0,c_times(V_U,c_HOL_Oabs(v_g(v_x(V_U)),t_b),t_b),t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2784,negated_conjecture,
class_Ring__and__Field_Oordered__idom(t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3145,plain,
c_IntDef_Oint(c_0) = c_0,
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f3148,plain,
c_lessequals(c_IntDef_Oint(c_0),c_0,tc_IntDef_Oint),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f3170,plain,
! [X0] :
( c_0 = c_IntDef_Oof__int(c_0,X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f3173,plain,
! [X0,X1] :
( c_lessequals(c_0,c_IntDef_Oof__int(X1,X0),X0)
| ~ c_lessequals(c_0,X1,tc_IntDef_Oint)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f4654,plain,
! [T_a] :
( ! [V_b] : c_0 = c_times(c_0,V_b,T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(miniscoping,[status(thm)],[f1363]) ).
fof(f4655,plain,
! [X0,X1] :
( c_0 = c_times(c_0,X1,X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(thm)],[f4654]) ).
fof(f6221,plain,
! [X0] : ~ c_lessequals(c_0,c_times(X0,c_HOL_Oabs(v_g(v_x(X0)),t_b),t_b),t_b),
inference(cnf_transformation,[status(thm)],[f2783]) ).
fof(f6222,plain,
class_Ring__and__Field_Oordered__idom(t_b),
inference(cnf_transformation,[status(thm)],[f2784]) ).
fof(f6537,plain,
! [X0] : c_0 = c_times(c_0,X0,t_b),
inference(resolution,[status(thm)],[f4655,f6222]) ).
fof(f6546,plain,
~ c_lessequals(c_0,c_0,t_b),
inference(paramodulation,[status(thm)],[f6537,f6221]) ).
fof(f11588,plain,
c_lessequals(c_0,c_0,tc_IntDef_Oint),
inference(forward_demodulation,[status(thm)],[f3145,f3148]) ).
fof(f12222,plain,
c_0 = c_IntDef_Oof__int(c_0,t_b),
inference(resolution,[status(thm)],[f3170,f6222]) ).
fof(f12590,plain,
! [X0] :
( c_lessequals(c_0,c_IntDef_Oof__int(X0,t_b),t_b)
| ~ c_lessequals(c_0,X0,tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[f3173,f6222]) ).
fof(f12804,plain,
c_lessequals(c_0,c_IntDef_Oof__int(c_0,t_b),t_b),
inference(resolution,[status(thm)],[f12590,f11588]) ).
fof(f12815,plain,
c_lessequals(c_0,c_0,t_b),
inference(forward_demodulation,[status(thm)],[f12222,f12804]) ).
fof(f12816,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f12815,f6546]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ANA045-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 13:31:08 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.21/0.48 % Drodi V4.1.1
% 3.08/1.04 % Refutation found
% 3.08/1.04 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.08/1.04 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.08/1.08 % Elapsed time: 0.694554 seconds
% 3.08/1.08 % CPU time: 4.211151 seconds
% 3.08/1.08 % Total memory used: 259.498 MB
% 3.08/1.08 % Net memory used: 256.044 MB
%------------------------------------------------------------------------------