%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV886-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 02:49:43 PM UTC 2026
% Result : Unsatisfiable 12.49s 2.10s
% Output : CNFRefutation 13.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 18
% Syntax : Number of formulae : 65 ( 41 unt; 0 def)
% Number of atoms : 96 ( 60 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 62 ( 31 ~; 31 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 9 con; 0-4 aty)
% Number of variables : 69 ( 69 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f107,axiom,
! [T_a,V_x] :
( c_lessequals(c_Orderings_Obot__class_Obot(T_a),V_x,T_a)
| ~ class_Orderings_Obot(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,axiom,
! [V_m,V_n] : c_HOL_Oplus__class_Oplus(c_Suc(V_m),V_n,tc_nat) = c_HOL_Oplus__class_Oplus(V_m,c_Suc(V_n),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,axiom,
! [V_n] : c_Suc(V_n) = c_HOL_Oplus__class_Oplus(V_n,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f268,axiom,
! [T_a,V_A] : c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f286,axiom,
! [V_A,T_a] :
( V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_Finite__Set_Ocard(V_A,T_a) != c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f300,axiom,
! [V_n] :
( ~ c_lessequals(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)
| V_n = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f321,axiom,
! [V_m] : c_HOL_Ominus__class_Ominus(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = V_m,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f330,axiom,
! [V_m,V_n] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),V_n,tc_nat) = V_m,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f331,axiom,
! [V_n,V_m] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_n,V_m,tc_nat),V_n,tc_nat) = V_m,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f366,axiom,
! [V_x,V_A,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_A,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f377,axiom,
! [V_m,V_n] :
( ~ c_lessequals(V_n,V_m,tc_nat)
| c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_n,tc_nat) = V_m ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f508,axiom,
! [V_x,V_xa,T_a] :
( c_Finite__Set_Ocard(V_xa,T_a) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_xa,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(V_xa,T_a))
| c_in(V_x,V_xa,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f582,negated_conjecture,
c_lessequals(c_Suc(v_na),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f583,negated_conjecture,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f585,negated_conjecture,
~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f586,negated_conjecture,
c_Finite__Set_Ofinite(v_G,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f587,negated_conjecture,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f611,axiom,
class_Orderings_Obot(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f792,plain,
! [T_a] :
( ! [V_x] : c_lessequals(c_Orderings_Obot__class_Obot(T_a),V_x,T_a)
| ~ class_Orderings_Obot(T_a) ),
inference(miniscoping,[status(thm)],[f107]) ).
fof(f793,plain,
! [X0,X1] :
( c_lessequals(c_Orderings_Obot__class_Obot(X0),X1,X0)
| ~ class_Orderings_Obot(X0) ),
inference(cnf_transformation,[status(thm)],[f792]) ).
fof(f873,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(c_Suc(X0),X1,tc_nat) = c_HOL_Oplus__class_Oplus(X0,c_Suc(X1),tc_nat),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f946,plain,
! [X0] : c_Suc(X0) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f1032,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,tc_fun(X0,tc_bool)) = c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f1060,plain,
! [X0,X1] :
( X0 = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))
| ~ c_Finite__Set_Ofinite(X0,X1)
| c_Finite__Set_Ocard(X0,X1) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f1077,plain,
! [X0] :
( ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f1112,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = X0,
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f1124,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat) = X0,
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f1125,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat) = X1,
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f1179,plain,
! [V_A,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ! [V_x] : c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_A,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a)) ),
inference(miniscoping,[status(thm)],[f366]) ).
fof(f1180,plain,
! [X0,X1,X2] :
( ~ c_Finite__Set_Ofinite(X1,X2)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(X1,c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),tc_fun(X2,tc_bool)),X2)) ),
inference(cnf_transformation,[status(thm)],[f1179]) ).
fof(f1197,plain,
! [X0,X1] :
( ~ c_lessequals(X1,X0,tc_nat)
| c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X1,tc_nat) = X0 ),
inference(cnf_transformation,[status(thm)],[f377]) ).
fof(f1392,plain,
! [V_xa,T_a] :
( c_Finite__Set_Ocard(V_xa,T_a) = c_HOL_Ozero__class_Ozero(tc_nat)
| ! [V_x] :
( c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_xa,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(V_xa,T_a))
| c_in(V_x,V_xa,T_a) ) ),
inference(miniscoping,[status(thm)],[f508]) ).
fof(f1393,plain,
! [X0,X1,X2] :
( c_Finite__Set_Ocard(X1,X2) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(X1,X2))
| c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1392]) ).
fof(f1502,plain,
c_lessequals(c_Suc(v_na),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
inference(cnf_transformation,[status(thm)],[f582]) ).
fof(f1503,plain,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),
inference(cnf_transformation,[status(thm)],[f583]) ).
fof(f1505,plain,
~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),
inference(cnf_transformation,[status(thm)],[f585]) ).
fof(f1506,plain,
c_Finite__Set_Ofinite(v_G,t_a),
inference(cnf_transformation,[status(thm)],[f586]) ).
fof(f1507,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat),
inference(cnf_transformation,[status(thm)],[f587]) ).
fof(f1536,plain,
class_Orderings_Obot(tc_nat),
inference(cnf_transformation,[status(thm)],[f611]) ).
fof(f1560,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = X0,
inference(paramodulation,[status(thm)],[f1112,f1125]) ).
fof(f3016,plain,
( ~ class_Orderings_Obot(tc_nat)
| c_Orderings_Obot__class_Obot(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(resolution,[status(thm)],[f1077,f793]) ).
fof(f3026,plain,
c_Orderings_Obot__class_Obot(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[f3016,f1536]) ).
fof(f3049,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_Orderings_Obot__class_Obot(tc_nat),X0,tc_nat) = X0,
inference(backward_demodulation,[status(thm)],[f3026,f1560]) ).
fof(f3252,plain,
c_Suc(c_Orderings_Obot__class_Obot(tc_nat)) = c_HOL_Oone__class_Oone(tc_nat),
inference(paramodulation,[status(thm)],[f946,f3049]) ).
fof(f4438,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,c_Suc(X1),tc_nat),X1,tc_nat) = c_Suc(X0),
inference(paramodulation,[status(thm)],[f873,f1124]) ).
fof(f6763,plain,
! [X0,X1] :
( X0 = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))
| ~ c_Finite__Set_Ofinite(X0,X1)
| c_Finite__Set_Ocard(X0,X1) != c_Orderings_Obot__class_Obot(tc_nat) ),
inference(forward_demodulation,[status(thm)],[f3026,f1060]) ).
fof(f20309,plain,
( ~ c_lessequals(c_Suc(v_na),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat)
| c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_Suc(v_na),tc_nat) = c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a) ),
inference(paramodulation,[status(thm)],[f1503,f1197]) ).
fof(f20321,plain,
c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_Suc(v_na),tc_nat) = c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),
inference(forward_subsumption_resolution,[status(thm)],[f20309,f1502]) ).
fof(f23168,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_Suc(v_na),tc_nat),v_na,tc_nat),
inference(backward_demodulation,[status(thm)],[f20321,f1507]) ).
fof(f23251,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_Suc(c_Finite__Set_Ocard(v_G,t_a)),
inference(forward_demodulation,[status(thm)],[f4438,f23168]) ).
fof(f31501,plain,
! [X0,X1,X2] :
( c_Finite__Set_Ocard(X1,X2) = c_Orderings_Obot__class_Obot(tc_nat)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(X1,X2))
| c_in(X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f3026,f1393]) ).
fof(f31502,plain,
( c_Finite__Set_Ocard(v_G,t_a) = c_Orderings_Obot__class_Obot(tc_nat)
| c_in(hAPP(v_mgt__call,v_pn),v_G,t_a) ),
inference(resolution,[status(thm)],[f31501,f23251]) ).
fof(f31545,plain,
c_Finite__Set_Ocard(v_G,t_a) = c_Orderings_Obot__class_Obot(tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[f31502,f1505]) ).
fof(f31587,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_Suc(c_Orderings_Obot__class_Obot(tc_nat)),
inference(backward_demodulation,[status(thm)],[f31545,f23251]) ).
fof(f31589,plain,
( v_G = c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool))
| ~ c_Finite__Set_Ofinite(v_G,t_a) ),
inference(resolution,[status(thm)],[f31545,f6763]) ).
fof(f31659,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_HOL_Oone__class_Oone(tc_nat),
inference(forward_demodulation,[status(thm)],[f3252,f31587]) ).
fof(f31661,plain,
v_G = c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),
inference(forward_subsumption_resolution,[status(thm)],[f31589,f1506]) ).
fof(f31679,plain,
! [X0] : c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)) = c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),
inference(paramodulation,[status(thm)],[f31661,f1032]) ).
fof(f31712,plain,
! [X0] : c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)) = v_G,
inference(forward_demodulation,[status(thm)],[f31661,f31679]) ).
fof(f31803,plain,
! [X0] :
( ~ c_Finite__Set_Ofinite(v_G,t_a)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,v_G,t_a),t_a) = c_Suc(c_Finite__Set_Ocard(v_G,t_a)) ),
inference(paramodulation,[status(thm)],[f31712,f1180]) ).
fof(f31850,plain,
! [X0] :
( ~ c_Finite__Set_Ofinite(v_G,t_a)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,v_G,t_a),t_a) = c_Suc(c_Orderings_Obot__class_Obot(tc_nat)) ),
inference(forward_demodulation,[status(thm)],[f31545,f31803]) ).
fof(f31851,plain,
! [X0] :
( ~ c_Finite__Set_Ofinite(v_G,t_a)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,v_G,t_a),t_a) = c_HOL_Oone__class_Oone(tc_nat) ),
inference(forward_demodulation,[status(thm)],[f3252,f31850]) ).
fof(f31852,plain,
! [X0] : c_Finite__Set_Ocard(c_Set_Oinsert(X0,v_G,t_a),t_a) = c_HOL_Oone__class_Oone(tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[f31851,f1506]) ).
fof(f32119,plain,
c_HOL_Oone__class_Oone(tc_nat) != c_HOL_Oone__class_Oone(tc_nat),
inference(forward_demodulation,[status(thm)],[f31852,f31659]) ).
fof(f32120,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f32119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV886-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n001.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 09:35:44 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 12.49/2.10 % Refutation found
% 12.49/2.10 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 12.49/2.10 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.30/2.18 % Elapsed time: 1.818541 seconds
% 13.30/2.18 % CPU time: 13.661103 seconds
% 13.30/2.18 % Total memory used: 255.397 MB
% 13.30/2.18 % Net memory used: 245.431 MB
%------------------------------------------------------------------------------