%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT023-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:07:13 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT023-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n012.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 04:26:21 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 0.12/0.41 % Refutation found
% 0.12/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.41 fof(f573,axiom,(
% 0.12/0.41 (![V_x,V_z,T_a,V_r,V_y]: (( c_in(c_Pair(V_x,V_z,T_a,T_a),V_r,tc_prod(T_a,T_a))| ~ c_in(c_Pair(V_y,V_z,T_a,T_a),V_r,tc_prod(T_a,T_a))| ~ c_in(c_Pair(V_x,V_y,T_a,T_a),V_r,tc_prod(T_a,T_a))| ~ c_Relation_Otrans(V_r,T_a) ) ))),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f579,negated_conjecture,(
% 0.12/0.41 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)) ),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f580,negated_conjecture,(
% 0.12/0.41 c_Relation_Otrans(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt) ),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f581,negated_conjecture,(
% 0.12/0.41 (![V_xa]: (~ c_in(c_Pair(V_xa,V_xa,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)) ))),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f582,negated_conjecture,(
% 0.12/0.41 ~ 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)) ),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f583,negated_conjecture,(
% 0.12/0.41 (![V_y,V_xa,V_x]: (( c_in(c_Pair(V_y,V_xa,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))| c_in(c_Pair(V_xa,V_y,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))| V_xa = V_y ) ))),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f585,negated_conjecture,(
% 0.12/0.41 (![V_a,V_b]: (( 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))| ~ 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))| V_a = V_b ) ))),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f1460,plain,(
% 0.12/0.41 ![T_a,V_r]: ((![V_x,V_y]: ((![V_z]: (c_in(c_Pair(V_x,V_z,T_a,T_a),V_r,tc_prod(T_a,T_a))|~c_in(c_Pair(V_y,V_z,T_a,T_a),V_r,tc_prod(T_a,T_a))))|~c_in(c_Pair(V_x,V_y,T_a,T_a),V_r,tc_prod(T_a,T_a))))|~c_Relation_Otrans(V_r,T_a))),
% 0.12/0.41 inference(miniscoping,[status(thm)],[f573])).
% 0.12/0.41 fof(f1461,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4]: (c_in(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2))|~c_in(c_Pair(X4,X1,X2,X2),X3,tc_prod(X2,X2))|~c_in(c_Pair(X0,X4,X2,X2),X3,tc_prod(X2,X2))|~c_Relation_Otrans(X3,X2))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f1460])).
% 0.12/0.41 fof(f1470,plain,(
% 0.12/0.41 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))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f579])).
% 0.12/0.41 fof(f1471,plain,(
% 0.12/0.41 c_Relation_Otrans(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f580])).
% 0.12/0.41 fof(f1472,plain,(
% 0.12/0.41 ![X0]: (~c_in(c_Pair(X0,X0,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)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f581])).
% 0.12/0.41 fof(f1473,plain,(
% 0.12/0.41 ~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))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f582])).
% 0.12/0.41 fof(f1474,plain,(
% 0.12/0.41 ![V_y,V_xa]: ((![V_x]: (c_in(c_Pair(V_y,V_xa,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))|c_in(c_Pair(V_xa,V_y,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))))|V_xa=V_y)),
% 0.12/0.42 inference(miniscoping,[status(thm)],[f583])).
% 0.12/0.42 fof(f1475,plain,(
% 0.12/0.42 ![X0,X1,X2]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X1=X0)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f1474])).
% 0.12/0.42 fof(f1477,plain,(
% 0.12/0.42 ![X0,X1]: (c_in(c_Pair(X0,X1,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))|~c_in(c_Pair(X0,X1,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))|X0=X1)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f585])).
% 0.12/0.42 fof(f1558,plain,(
% 0.12/0.42 ![X0]: (c_in(c_Pair(X0,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))|~c_in(c_Pair(X0,v_a,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))|~c_Relation_Otrans(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt))),
% 0.12/0.42 inference(resolution,[status(thm)],[f1461,f1470])).
% 0.12/0.42 fof(f1559,plain,(
% 0.12/0.42 ![X0]: (c_in(c_Pair(X0,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))|~c_in(c_Pair(X0,v_a,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)))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1558,f1471])).
% 0.12/0.42 fof(f1599,plain,(
% 0.12/0.42 ![X0,X1]: (c_in(c_Pair(X0,X1,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))|X0=X1|c_in(c_Pair(X1,X0,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))|X0=X1)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1477,f1475])).
% 0.12/0.42 fof(f1602,plain,(
% 0.12/0.42 ![X0,X1]: (c_in(c_Pair(X0,X1,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))|X0=X1|c_in(c_Pair(X1,X0,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)))),
% 0.12/0.42 inference(duplicate_literals_removal,[status(thm)],[f1599])).
% 0.12/0.42 fof(f1643,plain,(
% 0.12/0.42 ~c_in(c_Pair(v_b,v_a,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))),
% 0.12/0.42 inference(resolution,[status(thm)],[f1559,f1472])).
% 0.12/0.42 fof(f1690,plain,(
% 0.12/0.42 c_in(c_Pair(v_b,v_a,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))|v_b=v_a),
% 0.12/0.42 inference(resolution,[status(thm)],[f1602,f1473])).
% 0.12/0.42 fof(f1695,plain,(
% 0.12/0.42 v_b=v_a),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1690,f1643])).
% 0.12/0.42 fof(f1702,plain,(
% 0.12/0.42 c_in(c_Pair(v_a,v_a,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))),
% 0.12/0.42 inference(backward_demodulation,[status(thm)],[f1695,f1470])).
% 0.12/0.42 fof(f1703,plain,(
% 0.12/0.42 $false),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1702,f1472])).
% 0.12/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.45 % Elapsed time: 0.081610 seconds
% 0.12/0.45 % CPU time: 0.257309 seconds
% 0.12/0.45 % Total memory used: 113.924 MB
% 0.12/0.45 % Net memory used: 113.637 MB
%------------------------------------------------------------------------------