%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV914-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:47 PM UTC 2026
% Result : Unsatisfiable 111.88s 24.65s
% Output : CNFRefutation 111.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 14
% Syntax : Number of formulae : 64 ( 32 unt; 2 def)
% Number of atoms : 115 ( 24 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 100 ( 49 ~; 49 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 8 con; 0-6 aty)
% Number of variables : 158 ( 158 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
! [V_P,T_a] : c_Collect(V_P,T_a) = V_P,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f297,axiom,
! [T_a,V_a] : c_Collect(hAPP(c_COMBC(c_fequal(T_a),T_a,T_a,tc_bool),V_a),T_a) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f447,axiom,
! [T_a,V_P,V_Q] : c_Collect(hAPP(hAPP(c_COMBS(T_a,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),T_a),V_P)),V_Q),T_a) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),c_Collect(V_P,T_a)),c_Collect(V_Q,T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f451,axiom,
! [T_a,V_a] : c_Collect(hAPP(c_fequal(T_a),V_a),T_a) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f481,axiom,
! [V_G,V_P,V_c,V_Q,V_xa,V_Z_H,V_x] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(V_x,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(V_G,V_P,V_Q,V_c)))
| hBOOL(hAPP(hAPP(V_xa,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f486,axiom,
! [V_G,V_P,V_c,V_Q] :
( hBOOL(hAPP(hAPP(V_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(V_G,V_P,V_Q,V_c)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f490,axiom,
! [V_G,V_P,V_c,V_Q,V_x,V_xa] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(V_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f497,axiom,
! [T_a,V_a,V_P] :
( ~ hBOOL(hAPP(V_P,V_a))
| c_Collect(hAPP(hAPP(c_COMBS(T_a,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),T_a),hAPP(c_COMBC(c_fequal(T_a),T_a,T_a,tc_bool),V_a))),V_P),T_a) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f526,axiom,
! [V_P,T_b,T_a,T_c,V_Q,V_R] : hAPP(hAPP(c_COMBB(V_P,T_b,T_a,T_c),V_Q),V_R) = hAPP(V_P,hAPP(V_Q,V_R)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f533,negated_conjecture,
! [V_s_H] : c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),V_s_H))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_c,v_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f534,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f564,axiom,
! [T_a,V_x] : hBOOL(hAPP(hAPP(c_fequal(T_a),V_x),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f595,plain,
! [X0,X1] : c_Collect(X0,X1) = X0,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f1028,plain,
! [X0,X1] : hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) = c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f1263,plain,
! [X0,X1,X2] : hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),c_Collect(X1,X0)),c_Collect(X2,X0)) = c_Collect(hAPP(hAPP(c_COMBS(X0,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),X0),X1)),X2),X0),
inference(cnf_transformation,[status(thm)],[f447]) ).
fof(f1267,plain,
! [X0,X1] : hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) = c_Collect(hAPP(c_fequal(X0),X1),X0),
inference(cnf_transformation,[status(thm)],[f451]) ).
fof(f1309,plain,
! [V_G,V_c,V_xa,V_x] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ! [V_P,V_Q,V_Z_H] :
( ~ hBOOL(hAPP(hAPP(V_x,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(V_G,V_P,V_Q,V_c)))
| hBOOL(hAPP(hAPP(V_xa,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ) ),
inference(miniscoping,[status(thm)],[f481]) ).
fof(f1310,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X5,X2,X6,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(X1,X4),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X5,X6,X2)))
| hBOOL(hAPP(hAPP(X3,X4),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X5,X6,X2,X1,X3)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
inference(cnf_transformation,[status(thm)],[f1309]) ).
fof(f1318,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X1,X3,X2)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
inference(cnf_transformation,[status(thm)],[f486]) ).
fof(f1325,plain,
! [V_G,V_c,V_x,V_xa] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ! [V_P,V_Q] :
( ~ hBOOL(hAPP(hAPP(V_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ) ),
inference(miniscoping,[status(thm)],[f490]) ).
fof(f1326,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X4,X3,X5,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| c_Hoare__Mirabelle_Ohoare__derivs(X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X2,X3,X0,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(X0,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X1,X2,X0,X3)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X1,X2,X0,X3,X4,X5))) ),
inference(cnf_transformation,[status(thm)],[f1325]) ).
fof(f1337,plain,
! [V_a,V_P] :
( ~ hBOOL(hAPP(V_P,V_a))
| ! [T_a] : c_Collect(hAPP(hAPP(c_COMBS(T_a,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),T_a),hAPP(c_COMBC(c_fequal(T_a),T_a,T_a,tc_bool),V_a))),V_P),T_a) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) ),
inference(miniscoping,[status(thm)],[f497]) ).
fof(f1338,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X2,X1))
| c_Collect(hAPP(hAPP(c_COMBS(X0,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),X0),hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1))),X2),X0) = hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) ),
inference(cnf_transformation,[status(thm)],[f1337]) ).
fof(f1383,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(X0,hAPP(X1,X2)) = hAPP(hAPP(c_COMBB(X0,X3,X4,X5),X1),X2),
inference(cnf_transformation,[status(thm)],[f526]) ).
fof(f1393,plain,
! [X0] : c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X0))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_c,v_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
inference(cnf_transformation,[status(thm)],[f533]) ).
fof(f1394,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
inference(cnf_transformation,[status(thm)],[f534]) ).
fof(f1437,plain,
! [X0,X1] : hBOOL(hAPP(hAPP(c_fequal(X0),X1),X1)),
inference(cnf_transformation,[status(thm)],[f564]) ).
fof(f1503,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,v_Q,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,v_P,v_Q,v_c,X0,X1)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X0,v_c,X1,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
inference(resolution,[status(thm)],[f1326,f1394]) ).
fof(f1526,plain,
! [X0] : c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Collect(hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X0))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_c,v_Q,t_a)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(backward_demodulation,[status(thm)],[f1267,f1393]) ).
fof(f1529,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Collect(hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(backward_demodulation,[status(thm)],[f1267,f1394]) ).
fof(f1574,plain,
! [X0,X1,X2,X3] :
( c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Collect(hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X3,X2,t_a)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)
| hBOOL(hAPP(hAPP(X0,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X1,X0,X2,X3)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X1,X0,X2,X3))) ),
inference(forward_demodulation,[status(thm)],[f1267,f1318]) ).
fof(f1581,plain,
hBOOL(hAPP(hAPP(v_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,v_Q,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c))),
inference(resolution,[status(thm)],[f1529,f1574]) ).
fof(f1597,plain,
! [X0] : c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X0))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_c,v_Q,t_a)),t_a),
inference(backward_demodulation,[status(thm)],[f595,f1526]) ).
fof(f1598,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a),
inference(backward_demodulation,[status(thm)],[f595,f1529]) ).
fof(f1603,plain,
! [X0,X1] : hAPP(c_fequal(X0),X1) = hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),
inference(backward_demodulation,[status(thm)],[f595,f1267]) ).
fof(f1702,plain,
! [X0,X1,X2] : hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),X1),c_Collect(X2,X0)) = c_Collect(hAPP(hAPP(c_COMBS(X0,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),X0),X1)),X2),X0),
inference(forward_demodulation,[status(thm)],[f595,f1263]) ).
fof(f1703,plain,
! [X0,X1,X2] : hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),X1),X2) = c_Collect(hAPP(hAPP(c_COMBS(X0,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),X0),X1)),X2),X0),
inference(forward_demodulation,[status(thm)],[f595,f1702]) ).
fof(f1706,plain,
! [X0,X1,X2] : hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),X1),X2) = hAPP(hAPP(c_COMBS(X0,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),X0),X1)),X2),
inference(forward_demodulation,[status(thm)],[f595,f1703]) ).
fof(f1731,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X2,X1))
| hAPP(hAPP(c_COMBS(X0,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),X0),hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1))),X2) = hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) ),
inference(forward_demodulation,[status(thm)],[f595,f1338]) ).
fof(f1732,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X2,X1))
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1)),X2) = hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) ),
inference(forward_demodulation,[status(thm)],[f1706,f1731]) ).
fof(f1733,plain,
! [X0,X1,X2] :
( hAPP(c_fequal(X2),X1) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X2,tc_bool)),hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X1)),X0)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f1603,f1732]) ).
fof(f1734,plain,
! [X0] : hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c))),hAPP(v_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,v_Q,v_c))) = hAPP(c_fequal(X0),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c)),
inference(resolution,[status(thm)],[f1733,f1581]) ).
fof(f1828,plain,
! [X0,X1] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X0,v_c,X1,t_a)),t_a)
| ~ hBOOL(hAPP(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,v_Q,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,v_P,v_Q,v_c,X0,X1))) ),
inference(forward_demodulation,[status(thm)],[f1603,f1503]) ).
fof(f1950,plain,
! [X0,X1] : hAPP(c_fequal(X0),X1) = c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0),
inference(forward_demodulation,[status(thm)],[f1603,f1028]) ).
fof(f1952,plain,
! [X0,X1] : hAPP(c_fequal(X0),X1) = hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),
inference(forward_demodulation,[status(thm)],[f595,f1950]) ).
fof(f1967,definition,
( sQ8_spl
<=> c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1968,plain,
( ~ sQ8_spl
| c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a) ),
inference(component_clause,[status(thm)],[f1967]) ).
fof(f1978,plain,
( ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1968,f1598]) ).
fof(f1979,plain,
~ sQ8_spl,
inference(contradiction_clause,[status(thm)],[f1978]) ).
fof(f2075,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X5,X2,X6,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(X1,X4),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X5,X6,X2)))
| hBOOL(hAPP(hAPP(X3,X4),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X5,X6,X2,X1,X3)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a) ),
inference(forward_demodulation,[status(thm)],[f1603,f1310]) ).
fof(f2076,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ hBOOL(hAPP(hAPP(X1,X6),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X4,X5,X2)))
| hBOOL(hAPP(hAPP(X3,X6),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X4,X5,X2,X1,X3)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a)),t_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a) ),
inference(forward_demodulation,[status(thm)],[f1603,f2075]) ).
fof(f2078,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(hAPP(hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X3))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),X2),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,X0,X1,v_c)))
| hBOOL(hAPP(hAPP(v_Q,X2),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,X0,X1,v_c,hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X3))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_Q)))
| c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X0,v_c,X1,t_a)),t_a) ),
inference(resolution,[status(thm)],[f2076,f1597]) ).
fof(f2081,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(hAPP(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X3))),hAPP(v_P,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,X0,X1,v_c)))
| hBOOL(hAPP(hAPP(v_Q,X2),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,X0,X1,v_c,hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X3))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_Q)))
| c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X0,v_c,X1,t_a)),t_a) ),
inference(forward_demodulation,[status(thm)],[f1383,f2078]) ).
fof(f2082,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP(v_Q,X3),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,X0,X1,v_c,hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X2))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_Q)))
| ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_fequal(tc_Com_Ostate),X2)),hAPP(v_P,X3)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,X0,X1,v_c)))
| c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X0,v_c,X1,t_a)),t_a) ),
inference(forward_demodulation,[status(thm)],[f1706,f2081]) ).
fof(f2174,plain,
! [X0] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X0))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_c,v_Q,t_a)),t_a)
| ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_fequal(tc_Com_Ostate),X0)),hAPP(v_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,v_Q,v_c))),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c)))
| c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a) ),
inference(resolution,[status(thm)],[f2082,f1828]) ).
fof(f2176,definition,
! [X0] :
( sQ14_spl
<=> ( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X0))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_c,v_Q,t_a)),t_a)
| ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_fequal(tc_Com_Ostate),X0)),hAPP(v_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,v_Q,v_c))),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c))) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f2177,plain,
! [X0] :
( ~ sQ14_spl
| ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(c_COMBB(hAPP(c_COMBS(tc_Com_Ostate,tc_bool,tc_bool),hAPP(c_COMBB(c_and,tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),hAPP(c_fequal(tc_Com_Ostate),X0))),tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_P),v_c,v_Q,t_a)),t_a)
| ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_fequal(tc_Com_Ostate),X0)),hAPP(v_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,v_Q,v_c))),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c))) ),
inference(component_clause,[status(thm)],[f2176]) ).
fof(f2179,plain,
( sQ14_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f2174,f1967,f2176]) ).
fof(f2181,plain,
! [X0] :
( ~ sQ14_spl
| ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_fequal(tc_Com_Ostate),X0)),hAPP(v_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,v_Q,v_c))),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2177,f1597]) ).
fof(f3739,plain,
! [X0] : hAPP(c_fequal(X0),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),hAPP(c_fequal(X0),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c))),hAPP(v_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,v_Q,v_c))),
inference(forward_demodulation,[status(thm)],[f1952,f1734]) ).
fof(f6195,plain,
( ~ sQ14_spl
| ~ hBOOL(hAPP(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,v_Q,v_c))) ),
inference(paramodulation,[status(thm)],[f3739,f2181]) ).
fof(f6199,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6195,f1437]) ).
fof(f6200,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f6199]) ).
fof(f6201,plain,
$false,
inference(sat_refutation,[status(thm)],[f1979,f2179,f6200]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV914-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.38 % Computer : n002.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Mon Sep 21 09:34:15 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.13/10.44 % Drodi V4.1.1
% 111.88/24.65 % Refutation found
% 111.88/24.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 111.88/24.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 72.49/25.88 % Elapsed time: 15.272799 seconds
% 72.49/25.88 % CPU time: 107.355409 seconds
% 72.49/25.88 % Total memory used: 779.637 MB
% 72.49/25.88 % Net memory used: 747.187 MB
%------------------------------------------------------------------------------