%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR039-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n007.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 : Fri Sep 25 01:05:22 PM UTC 2026
% Result : Unsatisfiable 50.78s 7.00s
% Output : CNFRefutation 50.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 33
% Syntax : Number of clauses : 64 ( 64 unt; 0 nHn; 60 RR)
% Number of literals : 64 ( 63 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 31 con; 0-4 aty)
% Number of variables : 11 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(hi1110,axiom,
ifeq4(disjointwith(X,Y),true,disjointwith(Y,X),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi150,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1001,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1) = true,
inference(hyper_resolution,[status(thm)],[hi1110,hi150]) ).
cnf(hi1103,axiom,
ifeq4(genls(OLD,NEW),true,ifeq4(genls(ARG1,OLD),true,genls(ARG1,NEW),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi143,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi379,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1863,plain,
genls(c_tptpcol_3_16386,c_tptpcol_1_1) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi143,hi379]) ).
cnf(hi1111,axiom,
ifeq4(genls(NEW,OLD),true,ifeq4(disjointwith(ARG1,OLD),true,disjointwith(ARG1,NEW),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h4344,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_3_16386) = true,
inference(hyper_resolution,[status(thm)],[hi1111,h1863,h1001]) ).
cnf(hi281,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi21,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1530,plain,
genls(c_tptpcol_5_16388,c_tptpcol_3_16386) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi281,hi21]) ).
cnf(hi346,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h3869,plain,
genls(c_tptpcol_6_18436,c_tptpcol_3_16386) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1530,hi346]) ).
cnf(h5752,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_6_18436) = true,
inference(hyper_resolution,[status(thm)],[hi1111,h3869,h4344]) ).
cnf(hi107,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi204,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1177,plain,
genls(c_tptpcol_13_18664,c_tptpcol_11_18631) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi107,hi204]) ).
cnf(hi41,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi171,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1090,plain,
genls(c_tptpcol_11_18631,c_tptpcol_9_18439) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi41,hi171]) ).
cnf(h3439,plain,
genls(c_tptpcol_13_18664,c_tptpcol_9_18439) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1090,h1177]) ).
cnf(hi348,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi251,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1770,plain,
genls(c_tptpcol_9_18439,c_tptpcol_7_18437) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi348,hi251]) ).
cnf(hi477,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h4181,plain,
genls(c_tptpcol_9_18439,c_tptpcol_6_18436) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi477,h1770]) ).
cnf(h5592,plain,
genls(c_tptpcol_13_18664,c_tptpcol_6_18436) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h4181,h3439]) ).
cnf(h8681,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_13_18664) = true,
inference(hyper_resolution,[status(thm)],[hi1111,h5592,h5752]) ).
cnf(hi187,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi178,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1140,plain,
genls(c_tptpcol_15_93775,c_tptpcol_13_93766) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi187,hi178]) ).
cnf(hi70,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi76,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h585,plain,
genls(c_tptpcol_13_93766,c_tptpcol_11_93764) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi70,hi76]) ).
cnf(h3391,plain,
genls(c_tptpcol_15_93775,c_tptpcol_11_93764) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h585,h1140]) ).
cnf(hi373,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi366,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1838,plain,
genls(c_tptpcol_11_93764,c_tptpcol_9_93699) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi373,hi366]) ).
cnf(hi340,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi364,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1817,plain,
genls(c_tptpcol_9_93699,c_tptpcol_7_93186) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi340,hi364]) ).
cnf(h4329,plain,
genls(c_tptpcol_11_93764,c_tptpcol_7_93186) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1817,h1838]) ).
cnf(h5714,plain,
genls(c_tptpcol_15_93775,c_tptpcol_7_93186) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h4329,h3391]) ).
cnf(hi411,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi12,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1961,plain,
genls(c_tptpcol_7_93186,c_tptpcol_5_90114) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi411,hi12]) ).
cnf(hi470,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h4506,plain,
genls(c_tptpcol_7_93186,c_tptpcol_4_90113) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi470,h1961]) ).
cnf(hi343,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi39,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1744,plain,
genls(c_tptpcol_3_81921,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi343,hi39]) ).
cnf(hi370,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h4162,plain,
genls(c_tptpcol_4_90113,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1744,hi370]) ).
cnf(h5969,plain,
genls(c_tptpcol_7_93186,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h4162,h4506]) ).
cnf(h9635,plain,
genls(c_tptpcol_15_93775,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h5969,h5714]) ).
cnf(hi1112,axiom,
ifeq4(genls(NEW,OLD),true,ifeq4(disjointwith(OLD,ARG2),true,disjointwith(NEW,ARG2),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h18079,plain,
disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) = true,
inference(hyper_resolution,[status(thm)],[hi1112,h9635,h8681]) ).
cnf(hi1132,negated_conjecture,
ifeq3(disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),true,a,b) = b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t0,plain,
b = a,
inference(hyper_resolution,[status(thm)],[hi1132,h18079]) ).
cnf(t838,plain,
a = b,
inference(orient,[status(thm)],[t0]) ).
cnf(goal_0,negated_conjecture,
b != a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
b != b,
inference(rw,[status(thm)],[goal_0,t838]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR039-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n007.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 08:21:40 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 50.78/7.00 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 50.78/7.00 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------