%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SCT058-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:06:51 PM UTC 2026
% Result : Unsatisfiable 0.21s 5.59s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 20
% Syntax : Number of formulae : 62 ( 14 unt; 7 def)
% Number of atoms : 112 ( 21 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 90 ( 40 ~; 43 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 10 con; 0-5 aty)
% Number of variables : 109 ( 109 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f13,axiom,
! [V_A,V_B,T_a,V_C] : c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [V_A,V_B,V_C,T_a] : c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(V_B,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [V_R,V_A,V_B,T_b,T_a] : c_Relation_OImage(V_R,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_b,tc_bool)),T_b,T_a) = c_Lattices_Oupper__semilattice__class_Osup(c_Relation_OImage(V_R,V_A,T_b,T_a),c_Relation_OImage(V_R,V_B,T_b,T_a),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [V_R,V_S,T_b,T_a,V_A] : c_Relation_OImage(c_Lattices_Oupper__semilattice__class_Osup(V_R,V_S,tc_fun(tc_prod(T_b,T_a),tc_bool)),V_A,T_b,T_a) = c_Lattices_Oupper__semilattice__class_Osup(c_Relation_OImage(V_R,V_A,T_b,T_a),c_Relation_OImage(V_S,V_A,T_b,T_a),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [T_b,V_f,V_g] :
( hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_f,V_g,tc_fun(t_a,T_b)),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(V_f,v_x),hAPP(V_g,v_x),T_b)
| ~ class_Lattices_Olattice(T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f597,axiom,
! [V_a,V_b,T_a,T_b,V_r] :
( ~ hBOOL(c_in(c_Pair(V_b,V_a,T_b,T_a),V_r,tc_prod(T_b,T_a)))
| hBOOL(c_in(c_Pair(V_a,V_b,T_a,T_b),hAPP(c_Relation_Oconverse(T_b,T_a),V_r),tc_prod(T_a,T_b))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f599,axiom,
! [V_b,V_a,T_b,T_a,V_r] :
( ~ hBOOL(c_in(c_Pair(V_a,V_b,T_a,T_b),hAPP(c_Relation_Oconverse(T_b,T_a),V_r),tc_prod(T_a,T_b)))
| hBOOL(c_in(c_Pair(V_b,V_a,T_b,T_a),V_r,tc_prod(T_b,T_a))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f602,axiom,
! [V_i] :
( ~ hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f603,axiom,
! [V_i] :
( ~ hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f606,axiom,
! [V_a,V_b,V_v,T_c,T_b,T_a] : hAPP(V_a,hAPP(V_b,V_v)) = hAPP(c_Fun_Ocomp(V_a,V_b,T_c,T_b,T_a),V_v),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f618,negated_conjecture,
( hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f619,negated_conjecture,
( ~ hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| ~ hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f635,axiom,
class_Lattices_Olattice(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f659,plain,
! [X0,X1,X2,X3] : c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),X3,tc_fun(X2,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f660,plain,
! [X0,X1,X2,X3] : c_Lattices_Oupper__semilattice__class_Osup(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(X1,c_Lattices_Oupper__semilattice__class_Osup(X0,X2,tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool)),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f670,plain,
! [X0,X1,X2,X3,X4] : c_Relation_OImage(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),X3,X4) = c_Lattices_Oupper__semilattice__class_Osup(c_Relation_OImage(X0,X1,X3,X4),c_Relation_OImage(X0,X2,X3,X4),tc_fun(X4,tc_bool)),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f671,plain,
! [X0,X1,X2,X3,X4] : c_Relation_OImage(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(tc_prod(X2,X3),tc_bool)),X4,X2,X3) = c_Lattices_Oupper__semilattice__class_Osup(c_Relation_OImage(X0,X4,X2,X3),c_Relation_OImage(X1,X4,X2,X3),tc_fun(X3,tc_bool)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f684,plain,
! [T_b] :
( ! [V_f,V_g] : hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_f,V_g,tc_fun(t_a,T_b)),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(V_f,v_x),hAPP(V_g,v_x),T_b)
| ~ class_Lattices_Olattice(T_b) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f685,plain,
! [X0,X1,X2] :
( hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(t_a,X0)),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(X1,v_x),hAPP(X2,v_x),X0)
| ~ class_Lattices_Olattice(X0) ),
inference(cnf_transformation,[status(thm)],[f684]) ).
fof(f1533,plain,
! [X0,X1,X2,X3,X4] :
( ~ hBOOL(c_in(c_Pair(X1,X0,X3,X2),X4,tc_prod(X3,X2)))
| hBOOL(c_in(c_Pair(X0,X1,X2,X3),hAPP(c_Relation_Oconverse(X3,X2),X4),tc_prod(X2,X3))) ),
inference(cnf_transformation,[status(thm)],[f597]) ).
fof(f1535,plain,
! [X0,X1,X2,X3,X4] :
( ~ hBOOL(c_in(c_Pair(X1,X0,X3,X2),hAPP(c_Relation_Oconverse(X2,X3),X4),tc_prod(X3,X2)))
| hBOOL(c_in(c_Pair(X0,X1,X2,X3),X4,tc_prod(X2,X3))) ),
inference(cnf_transformation,[status(thm)],[f599]) ).
fof(f1538,plain,
! [X0] :
( ~ hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(cnf_transformation,[status(thm)],[f602]) ).
fof(f1539,plain,
! [X0] :
( ~ hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(cnf_transformation,[status(thm)],[f603]) ).
fof(f1542,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(X0,hAPP(X1,X2)) = hAPP(c_Fun_Ocomp(X0,X1,X3,X4,X5),X2),
inference(cnf_transformation,[status(thm)],[f606]) ).
fof(f1556,plain,
( hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(cnf_transformation,[status(thm)],[f618]) ).
fof(f1557,plain,
( ~ hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| ~ hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(cnf_transformation,[status(thm)],[f619]) ).
fof(f1583,plain,
class_Lattices_Olattice(tc_bool),
inference(cnf_transformation,[status(thm)],[f635]) ).
fof(f1591,definition,
( sQ0_spl
<=> hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1592,plain,
( ~ sQ0_spl
| hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(component_clause,[status(thm)],[f1591]) ).
fof(f1593,plain,
( sQ0_spl
| ~ hBOOL(c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(component_clause,[status(thm)],[f1591]) ).
fof(f1594,definition,
( sQ1_spl
<=> hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1595,plain,
( ~ sQ1_spl
| hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(component_clause,[status(thm)],[f1594]) ).
fof(f1596,plain,
( sQ1_spl
| ~ hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(component_clause,[status(thm)],[f1594]) ).
fof(f1597,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1556,f1591,f1594]) ).
fof(f1598,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1557,f1591,f1594]) ).
fof(f1637,plain,
( sQ1_spl
| ~ hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_x)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(backward_demodulation,[status(thm)],[f1542,f1596]) ).
fof(f1662,plain,
! [X0,X1,X2] :
( hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(t_a,tc_bool)),tc_fun(t_a,tc_bool)),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(t_a,tc_bool)),v_x),hAPP(X2,v_x),tc_bool)
| ~ class_Lattices_Olattice(tc_bool) ),
inference(paramodulation,[status(thm)],[f659,f685]) ).
fof(f1678,definition,
( sQ3_spl
<=> class_Lattices_Olattice(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1680,plain,
( sQ3_spl
| ~ class_Lattices_Olattice(tc_bool) ),
inference(component_clause,[status(thm)],[f1678]) ).
fof(f1681,definition,
! [X0,X1,X2] :
( sQ4_spl
<=> hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(t_a,tc_bool)),tc_fun(t_a,tc_bool)),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(t_a,tc_bool)),v_x),hAPP(X2,v_x),tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1684,plain,
( sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1662,f1678,f1681]) ).
fof(f1693,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1680,f1583]) ).
fof(f1694,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f1693]) ).
fof(f1716,plain,
! [X0,X1,X2] :
( hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(t_a,tc_bool)),tc_fun(t_a,tc_bool)),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(X1,v_x),hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X2,tc_fun(t_a,tc_bool)),v_x),tc_bool)
| ~ class_Lattices_Olattice(tc_bool) ),
inference(paramodulation,[status(thm)],[f660,f685]) ).
fof(f1752,definition,
! [X0,X1,X2] :
( sQ5_spl
<=> hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(t_a,tc_bool)),tc_fun(t_a,tc_bool)),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(X1,v_x),hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X2,tc_fun(t_a,tc_bool)),v_x),tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1755,plain,
( sQ5_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1716,f1678,f1752]) ).
fof(f1814,plain,
( sQ1_spl
| ~ hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(resolution,[status(thm)],[f1533,f1637]) ).
fof(f1847,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Relation_OImage(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),X3,t_a),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_Relation_OImage(X0,X1,X3,t_a),v_x),hAPP(c_Relation_OImage(X0,X2,X3,t_a),v_x),tc_bool)
| ~ class_Lattices_Olattice(tc_bool) ),
inference(paramodulation,[status(thm)],[f670,f685]) ).
fof(f1860,definition,
! [X0,X1,X2,X3] :
( sQ8_spl
<=> hAPP(c_Relation_OImage(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),X3,t_a),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_Relation_OImage(X0,X1,X3,t_a),v_x),hAPP(c_Relation_OImage(X0,X2,X3,t_a),v_x),tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1863,plain,
( sQ8_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1847,f1678,f1860]) ).
fof(f1866,plain,
( ~ sQ0_spl
| hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(resolution,[status(thm)],[f1538,f1592]) ).
fof(f1868,plain,
( ~ sQ0_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1866,f1814]) ).
fof(f1869,plain,
( ~ sQ0_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1868]) ).
fof(f1870,plain,
( ~ sQ1_spl
| hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_x)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(forward_demodulation,[status(thm)],[f1542,f1595]) ).
fof(f1873,plain,
( sQ0_spl
| ~ hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(resolution,[status(thm)],[f1539,f1593]) ).
fof(f1880,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Relation_OImage(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(tc_prod(X2,t_a),tc_bool)),X3,X2,t_a),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_Relation_OImage(X0,X3,X2,t_a),v_x),hAPP(c_Relation_OImage(X1,X3,X2,t_a),v_x),tc_bool)
| ~ class_Lattices_Olattice(tc_bool) ),
inference(paramodulation,[status(thm)],[f671,f685]) ).
fof(f1893,definition,
! [X0,X1,X2,X3] :
( sQ9_spl
<=> hAPP(c_Relation_OImage(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(tc_prod(X2,t_a),tc_bool)),X3,X2,t_a),v_x) = c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_Relation_OImage(X0,X3,X2,t_a),v_x),hAPP(c_Relation_OImage(X1,X3,X2,t_a),v_x),tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1896,plain,
( sQ9_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1880,f1678,f1893]) ).
fof(f1906,plain,
( ~ sQ1_spl
| hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(resolution,[status(thm)],[f1870,f1535]) ).
fof(f1909,plain,
( ~ sQ1_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1906,f1873]) ).
fof(f1910,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f1909]) ).
fof(f1911,plain,
$false,
inference(sat_refutation,[status(thm)],[f1597,f1598,f1684,f1694,f1755,f1863,f1869,f1896,f1910]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT058-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.46 % Computer : n002.cluster.edu
% 0.16/5.46 % Model : x86_64 x86_64
% 0.16/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.46 % Memory : 8046.5625MB
% 0.16/5.46 % OS : Linux 6.8.0-71-generic
% 0.16/5.46 % CPULimit : 300
% 0.16/5.46 % WCLimit : 300
% 0.16/5.46 % DateTime : Mon Sep 21 04:31:22 UTC 2026
% 0.16/5.46 % CPUTime :
% 0.21/5.54 % Drodi V4.1.1
% 0.21/5.59 % Refutation found
% 0.21/5.59 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.21/5.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/5.68 % Elapsed time: 0.200407 seconds
% 0.21/5.68 % CPU time: 0.326939 seconds
% 0.21/5.68 % Total memory used: 44.239 MB
% 0.21/5.68 % Net memory used: 44.145 MB
%------------------------------------------------------------------------------