%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL747-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 : n004.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 01:08:41 PM UTC 2026
% Result : Unsatisfiable 185.45s 23.92s
% Output : CNFRefutation 180.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of formulae : 46 ( 30 unt; 0 def)
% Number of atoms : 62 ( 20 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 39 ( 23 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-4 aty)
% Number of variables : 178 ( 178 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f148,axiom,
! [V_m,V_n] :
( V_n = c_HOL_Ozero__class_Ozero(tc_nat)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != V_m ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f407,axiom,
! [V_m,V_n,V_k] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m),tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n)))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f408,axiom,
! [V_i,V_k,V_j] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_i,tc_nat),V_j))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_k))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f410,axiom,
! [V_i,V_j] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),tc_nat),V_i)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f415,axiom,
! [V_x] : hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,tc_nat),c_Suc(V_x))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f424,axiom,
! [V_i,V_m,V_j] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_i,tc_nat),V_j))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(V_i,tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_j))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f575,axiom,
c_HOL_Oord__class_Oless(v_n,tc_nat) = hAPP(c_lessequals(tc_nat),c_Suc(v_n)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f595,axiom,
! [V_t,V_k,V_s] : hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_Olift,V_t),V_k)),V_s),V_k) = V_t,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f662,axiom,
! [T_b,T_a,T_c,V_P,V_Q,V_R] : hAPP(hAPP(hAPP(c_COMBB(T_b,T_a,T_c),V_P),V_Q),V_R) = hAPP(V_P,hAPP(V_Q,V_R)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f663,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(f664,axiom,
! [V_P,T_b,T_c,T_a,V_Q,V_R] : hAPP(hAPP(c_COMBS(V_P,T_b,T_c,T_a),V_Q),V_R) = hAPP(hAPP(V_P,V_R),hAPP(V_Q,V_R)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f958,plain,
! [V_n] :
( V_n = c_HOL_Ozero__class_Ozero(tc_nat)
| ! [V_m] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != V_m ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f959,plain,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(tc_nat)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1) != X0 ),
inference(cnf_transformation,[status(thm)],[f958]) ).
fof(f1382,plain,
! [V_m,V_n] :
( ! [V_k] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m),tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n)))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n)) ),
inference(miniscoping,[status(thm)],[f407]) ).
fof(f1383,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X2),X0),tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X2),X1)))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X1)) ),
inference(cnf_transformation,[status(thm)],[f1382]) ).
fof(f1384,plain,
! [V_i,V_j] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_i,tc_nat),V_j))
| ! [V_k] : hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_k))) ),
inference(miniscoping,[status(thm)],[f408]) ).
fof(f1385,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X2))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X2),X1))) ),
inference(cnf_transformation,[status(thm)],[f1384]) ).
fof(f1387,plain,
! [X0,X1] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),tc_nat),X0)),
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f1394,plain,
! [X0] : hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),c_Suc(X0))),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f1405,plain,
! [V_i,V_j] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_i,tc_nat),V_j))
| ! [V_m] : hBOOL(hAPP(c_HOL_Oord__class_Oless(V_i,tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_j))) ),
inference(miniscoping,[status(thm)],[f424]) ).
fof(f1406,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X2))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X2))) ),
inference(cnf_transformation,[status(thm)],[f1405]) ).
fof(f1642,plain,
c_HOL_Oord__class_Oless(v_n,tc_nat) = hAPP(c_lessequals(tc_nat),c_Suc(v_n)),
inference(cnf_transformation,[status(thm)],[f575]) ).
fof(f1668,plain,
! [X0,X1,X2] : hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_Olift,X0),X1)),X2),X1) = X0,
inference(cnf_transformation,[status(thm)],[f595]) ).
fof(f1771,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(hAPP(hAPP(c_COMBB(X0,X1,X2),X3),X4),X5) = hAPP(X3,hAPP(X4,X5)),
inference(cnf_transformation,[status(thm)],[f662]) ).
fof(f1772,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)],[f663]) ).
fof(f1773,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(hAPP(c_COMBS(X0,X1,X2,X3),X4),X5) = hAPP(hAPP(X0,X5),hAPP(X4,X5)),
inference(cnf_transformation,[status(thm)],[f664]) ).
fof(f2024,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : hAPP(hAPP(c_COMBS(c_COMBC(X0,X1,X2,X3),X4,X5,X6),X7),X8) = hAPP(hAPP(X0,hAPP(X7,X8)),X8),
inference(paramodulation,[status(thm)],[f1772,f1773]) ).
fof(f3609,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X2),X0),tc_nat),X1))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X1)) ),
inference(resolution,[status(thm)],[f1383,f1406]) ).
fof(f3635,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X3,X4,X5),X0),X1),tc_nat),X2))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(X0,X1),tc_nat),X2)) ),
inference(paramodulation,[status(thm)],[f1773,f3609]) ).
fof(f3647,plain,
! [X0,X1,X2,X3,X4] : hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(X0,X1),tc_nat),c_Suc(hAPP(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X2,X3,X4),X0),X1)))),
inference(resolution,[status(thm)],[f3635,f1394]) ).
fof(f3673,plain,
! [X0,X1] : hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(X0,X1),tc_nat),c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),hAPP(X0,X1))))),
inference(paramodulation,[status(thm)],[f1773,f3647]) ).
fof(f3681,plain,
! [X0,X1,X2,X3,X4,X5] : hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(X0,X1),X2),tc_nat),c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),hAPP(hAPP(c_COMBC(X0,X3,X4,X5),X2),X1))))),
inference(paramodulation,[status(thm)],[f1772,f3673]) ).
fof(f3709,plain,
! [X0,X1,X2] : hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(X0,X1),X2),tc_nat),c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),hAPP(hAPP(X0,X1),X2))))),
inference(forward_demodulation,[status(thm)],[f1772,f3681]) ).
fof(f3754,plain,
! [X0,X1,X2,X3] : hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(X0,X1),tc_nat),c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X2),hAPP(hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_Olift,X0),X2)),X3),X2),X1))))),
inference(paramodulation,[status(thm)],[f1668,f3709]) ).
fof(f3800,plain,
! [X0,X1,X2] : hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(X0,X1),tc_nat),c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X2),hAPP(X0,X1))))),
inference(forward_demodulation,[status(thm)],[f1668,f3754]) ).
fof(f3822,plain,
! [X0] : hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Oord__class_Oless(v_n,tc_nat),tc_nat),c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),hAPP(c_lessequals(tc_nat),c_Suc(v_n)))))),
inference(paramodulation,[status(thm)],[f1642,f3800]) ).
fof(f3852,plain,
! [X0] : hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Oord__class_Oless(v_n,tc_nat),tc_nat),c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oord__class_Oless(v_n,tc_nat))))),
inference(forward_demodulation,[status(thm)],[f1642,f3822]) ).
fof(f4164,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X2)))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X1)) ),
inference(resolution,[status(thm)],[f1385,f3609]) ).
fof(f12741,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_COMBS(c_COMBC(c_HOL_Oplus__class_Oplus(tc_nat),X0,X1,X2),X3,X4,X5),X6),X7),tc_nat),hAPP(X6,X7))),
inference(paramodulation,[status(thm)],[f2024,f1387]) ).
fof(f12743,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( X7 = c_HOL_Ozero__class_Ozero(tc_nat)
| hAPP(hAPP(c_COMBS(c_COMBC(c_HOL_Oplus__class_Oplus(tc_nat),X0,X1,X2),X3,X4,X5),X6),X7) != hAPP(X6,X7) ),
inference(paramodulation,[status(thm)],[f2024,f959]) ).
fof(f17456,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] : c_COMBS(c_COMBC(c_COMBS(c_COMBC(c_HOL_Oplus__class_Oplus(tc_nat),X0,X1,X2),X3,X4,X5),X6,X7,X8),X9,X10,X11) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(resolution,[status(thm)],[f12743,f2024]) ).
fof(f25079,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_COMBS(c_COMBC(c_COMBS(c_COMBC(c_HOL_Oplus__class_Oplus(tc_nat),X0,X1,X2),X3,X4,X5),X6,X7,X8),X9,X10,X11),X12),X13),tc_nat),hAPP(hAPP(X12,X13),X13))),
inference(paramodulation,[status(thm)],[f2024,f12741]) ).
fof(f25130,plain,
! [X0,X1] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Ozero__class_Ozero(tc_nat),X0),X1),tc_nat),hAPP(hAPP(X0,X1),X1))),
inference(forward_demodulation,[status(thm)],[f17456,f25079]) ).
fof(f25169,plain,
! [X0,X1,X2,X3,X4] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(c_COMBB(X0,X1,X2),X3)),X4),tc_nat),hAPP(X3,hAPP(X4,X4)))),
inference(paramodulation,[status(thm)],[f1771,f25130]) ).
fof(f31162,plain,
! [X0,X1] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X1)),
inference(resolution,[status(thm)],[f25169,f4164]) ).
fof(f31244,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f3852,f31162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL747-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 01:00:50 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.42 % Drodi V4.1.1
% 185.45/23.92 % Refutation found
% 185.45/23.92 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 185.45/23.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 37.83/25.20 % Elapsed time: 24.614624 seconds
% 37.83/25.20 % CPU time: 176.037138 seconds
% 37.83/25.20 % Total memory used: 1.165 GB
% 37.83/25.20 % Net memory used: 1.104 GB
%------------------------------------------------------------------------------