%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV902-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 : 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 02:49:45 PM UTC 2026
% Result : Unsatisfiable 98.95s 18.22s
% Output : CNFRefutation 98.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of formulae : 39 ( 29 unt; 0 def)
% Number of atoms : 53 ( 16 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 33 ( 19 ~; 14 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 8 con; 0-5 aty)
% Number of variables : 96 ( 96 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f112,axiom,
! [V_P,T_a] : c_Collect(V_P,T_a) = V_P,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f501,axiom,
! [T_a,V_a] : c_Collect(hAPP(c_fequal(T_a),V_a),T_a) = c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f556,axiom,
! [V_x,T_a] : c_Option_Oset(c_Option_Ooption_OSome(V_x,T_a),T_a) = c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f604,axiom,
! [V_x,V_A,T_a,V_B] :
( ~ hBOOL(c_in(V_x,V_B,T_a))
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f606,axiom,
! [V_f,V_a,V_B,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oinsert(V_a,V_B,T_b),T_b,T_a) = c_Set_Oinsert(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_B,T_b,T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f639,axiom,
! [T_a,V_A] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f648,axiom,
! [V_x,V_A,T_a] : hBOOL(c_in(V_x,c_Set_Oinsert(V_x,V_A,T_a),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f654,axiom,
! [V_P,V_Q,T_b,T_a,T_c,V_R] : hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f670,axiom,
! [V_G,V_ts,T_a] :
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f672,axiom,
! [V_a,V_A,T_a] :
( ~ hBOOL(c_in(V_a,V_A,T_a))
| c_Set_Oinsert(V_a,V_A,T_a) = V_A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f686,negated_conjecture,
hBOOL(c_in(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f687,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f906,plain,
! [X0,X1] : X0 = c_Collect(X0,X1),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f1520,plain,
! [X0,X1] : c_Collect(hAPP(c_fequal(X0),X1),X0) = c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0),
inference(cnf_transformation,[status(thm)],[f501]) ).
fof(f1603,plain,
! [X0,X1] : c_Option_Oset(c_Option_Ooption_OSome(X0,X1),X1) = c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(thm)],[f556]) ).
fof(f1678,plain,
! [V_x,T_a,V_B] :
( ~ hBOOL(c_in(V_x,V_B,T_a))
| ! [V_A] :
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ) ),
inference(miniscoping,[status(thm)],[f604]) ).
fof(f1679,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(c_in(X0,X3,X2))
| ~ c_lessequals(X1,X3,tc_fun(X2,tc_bool))
| c_lessequals(c_Set_Oinsert(X0,X1,X2),X3,tc_fun(X2,tc_bool)) ),
inference(cnf_transformation,[status(thm)],[f1678]) ).
fof(f1681,plain,
! [X0,X1,X2,X3,X4] : c_Set_Oinsert(hAPP(X0,X1),c_Set_Oimage(X0,X2,X3,X4),X4) = c_Set_Oimage(X0,c_Set_Oinsert(X1,X2,X3),X3,X4),
inference(cnf_transformation,[status(thm)],[f606]) ).
fof(f1727,plain,
! [X0,X1] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(thm)],[f639]) ).
fof(f1742,plain,
! [X0,X1,X2] : hBOOL(c_in(X0,c_Set_Oinsert(X0,X1,X2),X2)),
inference(cnf_transformation,[status(thm)],[f648]) ).
fof(f1750,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(X0,hAPP(X1,X2)) = hAPP(c_COMBB(X0,X1,X3,X4,X5),X2),
inference(cnf_transformation,[status(thm)],[f654]) ).
fof(f1777,plain,
! [X0,X1,X2] :
( c_Hoare__Mirabelle_Ohoare__derivs(X1,X0,X2)
| ~ c_lessequals(X0,X1,tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)) ),
inference(cnf_transformation,[status(thm)],[f670]) ).
fof(f1779,plain,
! [X0,X1,X2] :
( ~ hBOOL(c_in(X1,X0,X2))
| X0 = c_Set_Oinsert(X1,X0,X2) ),
inference(cnf_transformation,[status(thm)],[f672]) ).
fof(f1799,plain,
hBOOL(c_in(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)),
inference(cnf_transformation,[status(thm)],[f686]) ).
fof(f1800,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(cnf_transformation,[status(thm)],[f687]) ).
fof(f1900,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Option_Oset(c_Option_Ooption_OSome(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(backward_demodulation,[status(thm)],[f1603,f1800]) ).
fof(f1962,plain,
! [X0,X1] : c_Collect(hAPP(c_fequal(X0),X1),X0) = c_Option_Oset(c_Option_Ooption_OSome(X1,X0),X0),
inference(backward_demodulation,[status(thm)],[f1603,f1520]) ).
fof(f2001,plain,
! [X0,X1] : hAPP(c_fequal(X0),X1) = c_Option_Oset(c_Option_Ooption_OSome(X1,X0),X0),
inference(backward_demodulation,[status(thm)],[f906,f1962]) ).
fof(f2032,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x))),tc_Com_Ostate),
inference(backward_demodulation,[status(thm)],[f2001,f1900]) ).
fof(f2073,plain,
! [X0,X1] : c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1) = hAPP(c_fequal(X1),X0),
inference(backward_demodulation,[status(thm)],[f2001,f1603]) ).
fof(f2130,plain,
c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom) = c_Set_Oinsert(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
inference(resolution,[status(thm)],[f1779,f1799]) ).
fof(f3349,plain,
! [X0,X1,X2,X3,X4] : hBOOL(c_in(hAPP(X0,X1),c_Set_Oimage(X0,c_Set_Oinsert(X1,X2,X3),X3,X4),X4)),
inference(paramodulation,[status(thm)],[f1681,f1742]) ).
fof(f3438,plain,
! [X0,X1] : hBOOL(c_in(hAPP(X0,v_x),c_Set_Oimage(X0,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,X1),X1)),
inference(paramodulation,[status(thm)],[f2130,f3349]) ).
fof(f3793,plain,
! [X0,X1,X2,X3,X4,X5] : hBOOL(c_in(hAPP(X0,hAPP(X1,v_x)),c_Set_Oimage(c_COMBB(X0,X1,X2,X3,X4),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,X5),X5)),
inference(paramodulation,[status(thm)],[f1750,f3438]) ).
fof(f5855,plain,
! [X0,X1,X2] :
( ~ hBOOL(c_in(X1,X2,X0))
| ~ c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X2,tc_fun(X0,tc_bool))
| c_lessequals(hAPP(c_fequal(X0),X1),X2,tc_fun(X0,tc_bool)) ),
inference(paramodulation,[status(thm)],[f2073,f1679]) ).
fof(f5910,plain,
! [X0,X1,X2] :
( ~ hBOOL(c_in(X1,X2,X0))
| c_lessequals(hAPP(c_fequal(X0),X1),X2,tc_fun(X0,tc_bool)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5855,f1727]) ).
fof(f7686,plain,
! [X0,X1,X2] :
( ~ hBOOL(c_in(X2,X0,tc_Hoare__Mirabelle_Otriple(X1)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(X1)),X2),X1) ),
inference(resolution,[status(thm)],[f5910,f1777]) ).
fof(f8321,plain,
~ hBOOL(c_in(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))),
inference(resolution,[status(thm)],[f7686,f2032]) ).
fof(f8327,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f8321,f3793]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV902-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/5.51 % Computer : n016.cluster.edu
% 0.16/5.51 % Model : x86_64 x86_64
% 0.16/5.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.51 % Memory : 8046.5625MB
% 0.16/5.51 % OS : Linux 6.8.0-71-generic
% 0.16/5.52 % CPULimit : 300
% 0.16/5.52 % WCLimit : 300
% 0.16/5.52 % DateTime : Mon Sep 21 09:35:44 UTC 2026
% 0.16/5.52 % CPUTime :
% 0.21/5.61 % Drodi V4.1.1
% 98.95/18.22 % Refutation found
% 98.95/18.22 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 98.95/18.22 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.13/19.04 % Elapsed time: 13.500291 seconds
% 7.13/19.04 % CPU time: 101.746283 seconds
% 7.13/19.04 % Total memory used: 821.056 MB
% 7.13/19.04 % Net memory used: 755.904 MB
%------------------------------------------------------------------------------