%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SCT024-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 : n011.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:48 PM UTC 2026
% Result : Unsatisfiable 0.26s 0.58s
% Output : CNFRefutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 12
% Syntax : Number of formulae : 41 ( 16 unt; 5 def)
% Number of atoms : 84 ( 6 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 81 ( 38 ~; 38 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 6 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-4 aty)
% Number of variables : 24 ( 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f672,axiom,
! [V_x,T_a,V_r] :
( ~ c_Relation_Oirrefl(V_r,T_a)
| ~ hBOOL(c_in(c_Pair(V_x,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f679,negated_conjecture,
! [V_x] : c_Relation_Otrans(hAPP(v_P,V_x),tc_Arrow__Order__Mirabelle_Oalt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f680,negated_conjecture,
! [V_x] : c_Relation_Oirrefl(hAPP(v_P,V_x),tc_Arrow__Order__Mirabelle_Oalt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f681,negated_conjecture,
! [V_x] : c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,V_x),tc_Arrow__Order__Mirabelle_Oalt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f682,negated_conjecture,
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(f683,negated_conjecture,
~ hBOOL(c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f687,negated_conjecture,
! [V_a,V_b,V_P] :
( ~ c_Relation_Otrans(hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt)
| ~ c_Relation_Oirrefl(hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt)
| ~ c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt)
| V_a = V_b
| ~ 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_a,V_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(V_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1705,plain,
! [T_a,V_r] :
( ~ c_Relation_Oirrefl(V_r,T_a)
| ! [V_x] : ~ hBOOL(c_in(c_Pair(V_x,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a))) ),
inference(miniscoping,[status(thm)],[f672]) ).
fof(f1706,plain,
! [X0,X1,X2] :
( ~ c_Relation_Oirrefl(X2,X1)
| ~ hBOOL(c_in(c_Pair(X0,X0,X1,X1),X2,tc_prod(X1,X1))) ),
inference(cnf_transformation,[status(thm)],[f1705]) ).
fof(f1716,plain,
! [X0] : c_Relation_Otrans(hAPP(v_P,X0),tc_Arrow__Order__Mirabelle_Oalt),
inference(cnf_transformation,[status(thm)],[f679]) ).
fof(f1717,plain,
! [X0] : c_Relation_Oirrefl(hAPP(v_P,X0),tc_Arrow__Order__Mirabelle_Oalt),
inference(cnf_transformation,[status(thm)],[f680]) ).
fof(f1718,plain,
! [X0] : c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,X0),tc_Arrow__Order__Mirabelle_Oalt),
inference(cnf_transformation,[status(thm)],[f681]) ).
fof(f1719,plain,
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))),
inference(cnf_transformation,[status(thm)],[f682]) ).
fof(f1720,plain,
~ hBOOL(c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
inference(cnf_transformation,[status(thm)],[f683]) ).
fof(f1724,plain,
! [V_P] :
( ~ c_Relation_Otrans(hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt)
| ~ c_Relation_Oirrefl(hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt)
| ~ c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt)
| ! [V_a,V_b] :
( V_a = V_b
| ~ 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_a,V_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(V_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ) ),
inference(miniscoping,[status(thm)],[f687]) ).
fof(f1725,plain,
! [X0,X1,X2] :
( ~ c_Relation_Otrans(hAPP(X2,v_Pa(X2)),tc_Arrow__Order__Mirabelle_Oalt)
| ~ c_Relation_Oirrefl(hAPP(X2,v_Pa(X2)),tc_Arrow__Order__Mirabelle_Oalt)
| ~ c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(X2,v_Pa(X2)),tc_Arrow__Order__Mirabelle_Oalt)
| X0 = X1
| ~ hBOOL(c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| hBOOL(c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(cnf_transformation,[status(thm)],[f1724]) ).
fof(f1794,plain,
( ~ c_Relation_Otrans(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)
| ~ c_Relation_Oirrefl(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)
| ~ c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)
| v_a = v_b
| hBOOL(c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(resolution,[status(thm)],[f1725,f1719]) ).
fof(f1796,definition,
( sQ5_spl
<=> hBOOL(c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1797,plain,
( ~ sQ5_spl
| hBOOL(c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
inference(component_clause,[status(thm)],[f1796]) ).
fof(f1799,definition,
( sQ6_spl
<=> v_a = v_b ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1800,plain,
( ~ sQ6_spl
| v_a = v_b ),
inference(component_clause,[status(thm)],[f1799]) ).
fof(f1802,definition,
( sQ7_spl
<=> c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1804,plain,
( sQ7_spl
| ~ c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt) ),
inference(component_clause,[status(thm)],[f1802]) ).
fof(f1805,definition,
( sQ8_spl
<=> c_Relation_Oirrefl(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1807,plain,
( sQ8_spl
| ~ c_Relation_Oirrefl(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt) ),
inference(component_clause,[status(thm)],[f1805]) ).
fof(f1808,definition,
( sQ9_spl
<=> c_Relation_Otrans(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1810,plain,
( sQ9_spl
| ~ c_Relation_Otrans(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt) ),
inference(component_clause,[status(thm)],[f1808]) ).
fof(f1811,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1794,f1796,f1799,f1802,f1805,f1808]) ).
fof(f1812,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1810,f1716]) ).
fof(f1813,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1812]) ).
fof(f1814,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1807,f1717]) ).
fof(f1815,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f1814]) ).
fof(f1816,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1804,f1718]) ).
fof(f1817,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f1816]) ).
fof(f1818,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1797,f1720]) ).
fof(f1819,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1818]) ).
fof(f1821,plain,
( ~ sQ6_spl
| hBOOL(c_in(c_Pair(v_b,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))) ),
inference(backward_demodulation,[status(thm)],[f1800,f1719]) ).
fof(f1917,plain,
( ~ sQ6_spl
| ~ c_Relation_Oirrefl(hAPP(v_P,v_i),tc_Arrow__Order__Mirabelle_Oalt) ),
inference(resolution,[status(thm)],[f1706,f1821]) ).
fof(f1921,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1917,f1717]) ).
fof(f1922,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1921]) ).
fof(f1923,plain,
$false,
inference(sat_refutation,[status(thm)],[f1811,f1813,f1815,f1817,f1819,f1922]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SCT024-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n011.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 04:26:25 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.26/0.53 % Drodi V4.1.1
% 0.26/0.58 % Refutation found
% 0.26/0.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.26/0.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.26/0.61 % Elapsed time: 0.163652 seconds
% 0.26/0.61 % CPU time: 0.461113 seconds
% 0.26/0.61 % Total memory used: 103.720 MB
% 0.26/0.61 % Net memory used: 103.536 MB
%------------------------------------------------------------------------------