%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV691-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 : n017.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:21 PM UTC 2026
% Result : Unsatisfiable 114.97s 15.09s
% Output : CNFRefutation 112.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 13
% Syntax : Number of formulae : 49 ( 28 unt; 0 def)
% Number of atoms : 78 ( 47 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 58 ( 29 ~; 29 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-5 aty)
% Number of variables : 131 ( 131 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [T_a,V_a] :
( hAPP(c_HOL_Oinverse__class_Oinverse(T_a),hAPP(c_HOL_Oinverse__class_Oinverse(T_a),V_a)) = V_a
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Odivision__ring(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,axiom,
! [V_n] :
( V_n = c_HOL_Ozero__class_Ozero(tc_nat)
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_n)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,axiom,
! [V_x,V_a] :
( V_a = c_HOL_Ozero__class_Ozero(tc_nat)
| V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f216,axiom,
! [V_n] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),V_n) = V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f248,axiom,
! [V_m,V_l,V_k,V_n] :
( hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_k,tc_nat),V_l))
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_l) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f249,axiom,
! [V_m,V_n] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f282,axiom,
! [V_j,V_i] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_i),tc_nat),V_i)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f774,axiom,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f929,axiom,
! [V_P,T_b,T_c,T_a,V_Q,V_R] : hAPP(hAPP(c_COMBC(V_P,T_b,T_c,T_a),V_Q),V_R) = hAPP(hAPP(V_P,V_R),V_Q),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f930,axiom,
! [V_P,V_Q,T_b,T_c,T_a,V_R] : hAPP(c_COMBS(V_P,V_Q,T_b,T_c,T_a),V_R) = hAPP(hAPP(V_P,V_R),hAPP(V_Q,V_R)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1011,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1034,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1042,axiom,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1073,plain,
! [T_a] :
( ! [V_a] : hAPP(c_HOL_Oinverse__class_Oinverse(T_a),hAPP(c_HOL_Oinverse__class_Oinverse(T_a),V_a)) = V_a
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Odivision__ring(T_a) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f1074,plain,
! [X0,X1] :
( hAPP(c_HOL_Oinverse__class_Oinverse(X0),hAPP(c_HOL_Oinverse__class_Oinverse(X0),X1)) = X1
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Odivision__ring(X0) ),
inference(cnf_transformation,[status(thm)],[f1073]) ).
fof(f1382,plain,
! [X0] :
( X0 = c_HOL_Ozero__class_Ozero(tc_nat)
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0)) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f1403,plain,
! [V_a] :
( V_a = c_HOL_Ozero__class_Ozero(tc_nat)
| ! [V_x] : V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_a) ),
inference(miniscoping,[status(thm)],[f211]) ).
fof(f1404,plain,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(tc_nat)
| X0 != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1) ),
inference(cnf_transformation,[status(thm)],[f1403]) ).
fof(f1410,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),X0) = X0,
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f1460,plain,
! [V_m,V_n] :
( hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n))
| ! [V_l,V_k] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_k,tc_nat),V_l))
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_l) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n) ) ),
inference(miniscoping,[status(thm)],[f248]) ).
fof(f1461,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X3))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,tc_nat),X1))
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X2),X3) ),
inference(cnf_transformation,[status(thm)],[f1460]) ).
fof(f1462,plain,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f1512,plain,
! [X0,X1] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),tc_nat),X1)),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f2321,plain,
! [X0] :
( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(thm)],[f774]) ).
fof(f2592,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(hAPP(c_COMBC(X0,X1,X2,X3),X4),X5) = hAPP(hAPP(X0,X5),X4),
inference(cnf_transformation,[status(thm)],[f929]) ).
fof(f2593,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(c_COMBS(X0,X1,X2,X3,X4),X5) = hAPP(hAPP(X0,X5),hAPP(X1,X5)),
inference(cnf_transformation,[status(thm)],[f930]) ).
fof(f2721,plain,
class_Ring__and__Field_Ozero__neq__one(tc_nat),
inference(cnf_transformation,[status(thm)],[f1011]) ).
fof(f2744,plain,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1034]) ).
fof(f2752,plain,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1042]) ).
fof(f2952,plain,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(tc_nat)
| X0 != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0) ),
inference(paramodulation,[status(thm)],[f1462,f1404]) ).
fof(f3009,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : hAPP(c_COMBS(c_COMBC(X0,X1,X2,X3),X4,X5,X6,X7),X8) = hAPP(hAPP(X0,hAPP(X4,X8)),X8),
inference(paramodulation,[status(thm)],[f2592,f2593]) ).
fof(f3014,plain,
! [X0,X1,X2,X3,X4] : hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X0,X1,X2,X3),X4) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(X0,X4)),X4),
inference(paramodulation,[status(thm)],[f1462,f2593]) ).
fof(f3068,plain,
! [X0,X1,X2,X3,X4] :
( X1 = c_HOL_Ozero__class_Ozero(tc_nat)
| hAPP(X0,X1) != hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X0,X2,X3,X4),X1) ),
inference(paramodulation,[status(thm)],[f2593,f2952]) ).
fof(f3073,plain,
! [X0,X1,X2,X3,X4] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X0,X1,X2,X3),X4),tc_nat),hAPP(X0,X4))),
inference(paramodulation,[status(thm)],[f2593,f1512]) ).
fof(f3359,plain,
! [X0] :
( hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0)) = X0
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f2752,f1074]) ).
fof(f3360,plain,
! [X0] : hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0)) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f3359,f2744]) ).
fof(f4464,plain,
c_HOL_Oone__class_Oone(tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(resolution,[status(thm)],[f2321,f2721]) ).
fof(f4801,plain,
! [X0,X1,X2,X3,X4,X5,X6] : hAPP(c_COMBS(c_COMBC(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0,X1,X2),c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X3,X4,X5),X6) = hAPP(X6,X6),
inference(paramodulation,[status(thm)],[f3360,f3009]) ).
fof(f5002,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),c_COMBS(c_COMBC(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0,X1,X2),c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X3,X4,X5),X6,X7,X8) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(resolution,[status(thm)],[f4801,f3068]) ).
fof(f5029,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),c_COMBS(c_COMBC(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0,X1,X2),c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X3,X4,X5),X6,X7,X8),X9) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(X9,X9)),X9),
inference(paramodulation,[status(thm)],[f4801,f3014]) ).
fof(f5134,plain,
! [X0] : hAPP(c_HOL_Ozero__class_Ozero(tc_nat),X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(X0,X0)),X0),
inference(forward_demodulation,[status(thm)],[f5002,f5029]) ).
fof(f7558,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X2))
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),X2)
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(resolution,[status(thm)],[f1382,f1461]) ).
fof(f7573,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X2))
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0) != X2
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(forward_demodulation,[status(thm)],[f1410,f7558]) ).
fof(f7574,plain,
! [X0,X1] :
( hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0)))
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(destructive_equality_resolution,[status(thm)],[f7573]) ).
fof(f9205,plain,
! [X0] :
( hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(X0,X0),tc_nat),hAPP(c_HOL_Ozero__class_Ozero(tc_nat),X0)))
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(paramodulation,[status(thm)],[f5134,f7574]) ).
fof(f10319,plain,
! [X0,X1,X2] : c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),X0,X1,X2) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(resolution,[status(thm)],[f9205,f3073]) ).
fof(f10392,plain,
! [X0] :
( X0 = c_HOL_Ozero__class_Ozero(tc_nat)
| hAPP(c_HOL_Ozero__class_Ozero(tc_nat),X0) != hAPP(c_HOL_Ozero__class_Ozero(tc_nat),X0) ),
inference(paramodulation,[status(thm)],[f10319,f3068]) ).
fof(f10398,plain,
! [X0] : X0 = c_HOL_Ozero__class_Ozero(tc_nat),
inference(trivial_equality_resolution,[status(thm)],[f10392]) ).
fof(f10399,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f4464,f10398]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV691-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 09:14:42 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.11/0.45 % Drodi V4.1.1
% 114.97/15.09 % Refutation found
% 114.97/15.09 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 114.97/15.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 112.70/15.20 % Elapsed time: 14.829520 seconds
% 112.70/15.20 % CPU time: 116.289864 seconds
% 112.70/15.20 % Total memory used: 688.244 MB
% 112.70/15.20 % Net memory used: 662.100 MB
%------------------------------------------------------------------------------