%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG004-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.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 02:37:23 PM UTC 2026
% Result : Unsatisfiable 33.53s 4.75s
% Output : CNFRefutation 33.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 17
% Syntax : Number of clauses : 129 ( 129 unt; 0 nHn; 46 RR)
% Number of literals : 129 ( 128 equ; 8 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-4 aty)
% Number of variables : 164 ( 18 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(hi8,axiom,
ifeq(sum(X,Y,Z),true,sum(Y,X,Z),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi3,axiom,
sum(X,Y,add(X,Y)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h17,plain,
sum(V0,V1,add(V1,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi8,hi3]) ).
cnf(hi15,axiom,
ifeq2(sum(X,Y,V),true,ifeq2(sum(X,Y,U),true,U,V),V) = V,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
add(X1,X2) = add(X2,X1),
inference(hyper_resolution,[status(thm)],[hi15,hi3,h17]) ).
cnf(t263,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t12]) ).
cnf(hi7,axiom,
ifeq(sum(Y,Z,V),true,ifeq(sum(X,V,W),true,ifeq(sum(X,Y,U),true,sum(U,Z,W),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h18,plain,
sum(add(V0,V1),V2,add(V0,add(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi3,hi3,hi3]) ).
cnf(t88,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(hyper_resolution,[status(thm)],[hi15,hi3,h18]) ).
cnf(t278,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t88]) ).
cnf(hi5,axiom,
sum(X,additive_inverse(X),additive_identity) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t5,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(hyper_resolution,[status(thm)],[hi15,hi3,hi5]) ).
cnf(t303,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t305,plain,
add(X1,add(additive_inverse(X1),X2)) = add(additive_identity,X2),
inference(cp,[status(thm)],[t278,t303]) ).
cnf(hi1,axiom,
sum(X,additive_identity,X) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi0,axiom,
sum(additive_identity,X,X) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h22,plain,
sum(add(additive_identity,V0),additive_identity,V0) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi1,hi0,hi3]) ).
cnf(t15,plain,
add(add(additive_identity,X1),additive_identity) = X1,
inference(hyper_resolution,[status(thm)],[hi15,hi3,h22]) ).
cnf(t1,plain,
add(X1,additive_identity) = X1,
inference(hyper_resolution,[status(thm)],[hi15,hi1,hi3]) ).
cnf(t257,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t3179,plain,
add(additive_identity,X1) = X1,
inference(step,[status(thm)],[t15,t257]) ).
cnf(t258,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t3179]) ).
cnf(t3226,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t305,t258]) ).
cnf(t1444,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t3226]) ).
cnf(t1446,plain,
additive_inverse(additive_inverse(X1)) = add(X1,additive_identity),
inference(cp,[status(thm)],[t1444,t303]) ).
cnf(t3227,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(step,[status(thm)],[t1446,t257]) ).
cnf(t1461,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t3227]) ).
cnf(t61,plain,
add(X1,add(X2,additive_inverse(add(X1,X2)))) = additive_identity,
inference(hyper_resolution,[status(thm)],[hi15,hi5,h18]) ).
cnf(t287,plain,
add(X1,add(X2,additive_inverse(add(X1,X2)))) = additive_identity,
inference(orient,[status(thm)],[t61]) ).
cnf(t1447,plain,
add(X1,additive_inverse(add(additive_inverse(X2),X1))) = add(X2,additive_identity),
inference(cp,[status(thm)],[t1444,t287]) ).
cnf(t3230,plain,
add(X1,additive_inverse(add(additive_inverse(X2),X1))) = X2,
inference(step,[status(thm)],[t1447,t257]) ).
cnf(t1548,plain,
add(X1,additive_inverse(add(additive_inverse(X2),X1))) = X2,
inference(orient,[status(thm)],[t3230]) ).
cnf(t1553,plain,
additive_inverse(X1) = add(X2,additive_inverse(add(X1,X2))),
inference(cp,[status(thm)],[t1548,t1461]) ).
cnf(t1570,plain,
add(X1,additive_inverse(add(X2,X1))) = additive_inverse(X2),
inference(orient,[status(thm)],[t1553]) ).
cnf(t1577,plain,
additive_inverse(X1) = add(X2,additive_inverse(add(X2,X1))),
inference(cp,[status(thm)],[t1570,t263]) ).
cnf(t1638,plain,
add(X1,additive_inverse(add(X1,X2))) = additive_inverse(X2),
inference(orient,[status(thm)],[t1577]) ).
cnf(hi11,axiom,
ifeq(product(X,V3,V4),true,ifeq(product(X,Z,V2),true,ifeq(product(X,Y,V1),true,ifeq(sum(Y,Z,V3),true,sum(V1,V2,V4),true),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi2,axiom,
product(X,Y,multiply(X,Y)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h16,plain,
sum(multiply(V0,V1),multiply(V0,V2),multiply(V0,add(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi11,hi2,hi2,hi2,hi3]) ).
cnf(t172,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X3,X2)),
inference(hyper_resolution,[status(thm)],[hi15,h16,h17]) ).
cnf(t316,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X3,X2)),
inference(orient,[status(thm)],[t172]) ).
cnf(hi14,axiom,
ifeq(product(Z,X,V2),true,ifeq(product(Y,X,V1),true,ifeq(sum(V1,V2,V4),true,ifeq(sum(Y,Z,V3),true,product(V3,X,V4),true),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h11,plain,
product(V0,V1,add(multiply(additive_identity,V1),multiply(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi14,hi2,hi2,hi3,hi0]) ).
cnf(hi16,axiom,
ifeq2(product(X,Y,V),true,ifeq2(product(X,Y,U),true,U,V),V) = V,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi18,axiom,
product(additive_inverse(a),additive_inverse(b),d) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t114,plain,
add(multiply(additive_identity,additive_inverse(b)),multiply(additive_inverse(a),additive_inverse(b))) = d,
inference(hyper_resolution,[status(thm)],[hi16,hi18,h11]) ).
cnf(hi13,axiom,
ifeq(product(V3,X,V4),true,ifeq(product(Z,X,V2),true,ifeq(product(Y,X,V1),true,ifeq(sum(Y,Z,V3),true,sum(V1,V2,V4),true),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h12,plain,
sum(multiply(V0,V1),multiply(V2,V1),multiply(add(V0,V2),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi13,hi2,hi2,hi2,hi3]) ).
cnf(t174,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X3,X1),X2),
inference(hyper_resolution,[status(thm)],[hi15,h12,h17]) ).
cnf(t310,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X3,X1),X2),
inference(orient,[status(thm)],[t174]) ).
cnf(t3184,plain,
multiply(add(additive_inverse(a),additive_identity),additive_inverse(b)) = d,
inference(step,[status(thm)],[t114,t310]) ).
cnf(t3185,plain,
multiply(additive_inverse(a),additive_inverse(b)) = d,
inference(step,[status(thm)],[t3184,t257]) ).
cnf(t328,plain,
multiply(additive_inverse(a),additive_inverse(b)) = d,
inference(orient,[status(thm)],[t3185]) ).
cnf(t329,plain,
multiply(additive_inverse(a),add(X1,additive_inverse(b))) = add(d,multiply(additive_inverse(a),X1)),
inference(cp,[status(thm)],[t316,t328]) ).
cnf(t2755,plain,
multiply(additive_inverse(a),add(X1,additive_inverse(b))) = add(d,multiply(additive_inverse(a),X1)),
inference(orient,[status(thm)],[t329]) ).
cnf(t2759,plain,
add(d,multiply(additive_inverse(a),additive_identity)) = multiply(additive_inverse(a),additive_inverse(b)),
inference(cp,[status(thm)],[t2755,t258]) ).
cnf(t3258,plain,
add(d,multiply(additive_inverse(a),additive_identity)) = d,
inference(step,[status(thm)],[t2759,t328]) ).
cnf(t2767,plain,
add(d,multiply(additive_inverse(a),additive_identity)) = d,
inference(orient,[status(thm)],[t3258]) ).
cnf(t2781,plain,
additive_inverse(multiply(additive_inverse(a),additive_identity)) = add(d,additive_inverse(d)),
inference(cp,[status(thm)],[t1638,t2767]) ).
cnf(t3259,plain,
additive_inverse(multiply(additive_inverse(a),additive_identity)) = additive_identity,
inference(step,[status(thm)],[t2781,t303]) ).
cnf(t2788,plain,
additive_inverse(multiply(additive_inverse(a),additive_identity)) = additive_identity,
inference(orient,[status(thm)],[t3259]) ).
cnf(t2795,plain,
multiply(additive_inverse(a),additive_identity) = additive_inverse(additive_identity),
inference(cp,[status(thm)],[t1461,t2788]) ).
cnf(hi4,axiom,
sum(additive_inverse(X),X,additive_identity) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h56,plain,
sum(additive_inverse(additive_identity),additive_identity,additive_identity) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi1,hi4,hi1]) ).
cnf(hi6,axiom,
ifeq(sum(U,Z,W),true,ifeq(sum(Y,Z,V),true,ifeq(sum(X,Y,U),true,sum(X,V,W),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h32,plain,
sum(V0,V1,add(add(V0,additive_identity),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi6,hi3,hi0,hi3]) ).
cnf(t25,plain,
add(add(additive_inverse(additive_identity),additive_identity),additive_identity) = additive_identity,
inference(hyper_resolution,[status(thm)],[hi15,h32,h56]) ).
cnf(t3180,plain,
add(additive_inverse(additive_identity),add(additive_identity,additive_identity)) = additive_identity,
inference(step,[status(thm)],[t25,t278]) ).
cnf(h21,plain,
sum(add(V0,additive_identity),additive_identity,V0) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi1,hi1,hi3]) ).
cnf(t13,plain,
add(X1,add(additive_identity,additive_identity)) = X1,
inference(hyper_resolution,[status(thm)],[hi15,h18,h21]) ).
cnf(t256,plain,
add(X1,add(additive_identity,additive_identity)) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t3181,plain,
additive_inverse(additive_identity) = additive_identity,
inference(step,[status(thm)],[t3180,t256]) ).
cnf(t309,plain,
additive_inverse(additive_identity) = additive_identity,
inference(orient,[status(thm)],[t3181]) ).
cnf(t3260,plain,
multiply(additive_inverse(a),additive_identity) = additive_identity,
inference(step,[status(thm)],[t2795,t309]) ).
cnf(t2823,plain,
multiply(additive_inverse(a),additive_identity) = additive_identity,
inference(orient,[status(thm)],[t3260]) ).
cnf(hi17,axiom,
product(a,b,c) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t50,plain,
add(multiply(additive_identity,b),multiply(a,b)) = c,
inference(hyper_resolution,[status(thm)],[hi16,hi17,h11]) ).
cnf(t3182,plain,
multiply(add(a,additive_identity),b) = c,
inference(step,[status(thm)],[t50,t310]) ).
cnf(t3183,plain,
multiply(a,b) = c,
inference(step,[status(thm)],[t3182,t257]) ).
cnf(t323,plain,
multiply(a,b) = c,
inference(orient,[status(thm)],[t3183]) ).
cnf(t326,plain,
multiply(add(X1,a),b) = add(c,multiply(X1,b)),
inference(cp,[status(thm)],[t310,t323]) ).
cnf(t1536,plain,
add(c,multiply(X1,b)) = multiply(add(X1,a),b),
inference(orient,[status(thm)],[t326]) ).
cnf(t2756,plain,
add(d,multiply(additive_inverse(a),b)) = multiply(additive_inverse(a),additive_identity),
inference(cp,[status(thm)],[t2755,t303]) ).
cnf(t3268,plain,
add(d,multiply(additive_inverse(a),b)) = additive_identity,
inference(step,[status(thm)],[t2756,t2823]) ).
cnf(t2963,plain,
add(d,multiply(additive_inverse(a),b)) = additive_identity,
inference(orient,[status(thm)],[t3268]) ).
cnf(t2980,plain,
additive_inverse(d) = add(multiply(additive_inverse(a),b),additive_inverse(additive_identity)),
inference(cp,[status(thm)],[t1570,t2963]) ).
cnf(t3269,plain,
additive_inverse(d) = add(additive_inverse(additive_identity),multiply(additive_inverse(a),b)),
inference(step,[status(thm)],[t2980,t263]) ).
cnf(t3270,plain,
additive_inverse(d) = add(additive_identity,multiply(additive_inverse(a),b)),
inference(step,[status(thm)],[t3269,t309]) ).
cnf(t3271,plain,
additive_inverse(d) = multiply(additive_inverse(a),b),
inference(step,[status(thm)],[t3270,t258]) ).
cnf(t2986,plain,
multiply(additive_inverse(a),b) = additive_inverse(d),
inference(orient,[status(thm)],[t3271]) ).
cnf(t2987,plain,
multiply(add(additive_inverse(a),a),b) = add(c,additive_inverse(d)),
inference(cp,[status(thm)],[t1536,t2986]) ).
cnf(t3278,plain,
multiply(add(a,additive_inverse(a)),b) = add(c,additive_inverse(d)),
inference(step,[status(thm)],[t2987,t263]) ).
cnf(t3279,plain,
multiply(additive_identity,b) = add(c,additive_inverse(d)),
inference(step,[status(thm)],[t3278,t303]) ).
cnf(h2,plain,
sum(multiply(additive_identity,V0),multiply(V1,V0),multiply(V1,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi13,hi2,hi2,hi2,hi0]) ).
cnf(t56,plain,
multiply(additive_identity,add(X1,X1)) = multiply(additive_identity,X1),
inference(hyper_resolution,[status(thm)],[hi15,h2,h16]) ).
cnf(t367,plain,
multiply(additive_identity,add(X1,X1)) = multiply(additive_identity,X1),
inference(orient,[status(thm)],[t56]) ).
cnf(t374,plain,
multiply(additive_identity,add(X1,add(X2,X2))) = add(multiply(additive_identity,X2),multiply(additive_identity,X1)),
inference(cp,[status(thm)],[t316,t367]) ).
cnf(t3237,plain,
multiply(additive_identity,add(X1,add(X2,X2))) = multiply(additive_identity,add(X1,X2)),
inference(step,[status(thm)],[t374,t316]) ).
cnf(t2156,plain,
multiply(additive_identity,add(X1,add(X2,X2))) = multiply(additive_identity,add(X1,X2)),
inference(orient,[status(thm)],[t3237]) ).
cnf(t1448,plain,
X1 = add(X2,add(X1,additive_inverse(X2))),
inference(cp,[status(thm)],[t1444,t263]) ).
cnf(t1490,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(orient,[status(thm)],[t1448]) ).
cnf(t2157,plain,
multiply(additive_identity,add(X1,additive_inverse(X1))) = multiply(additive_identity,additive_inverse(X1)),
inference(cp,[status(thm)],[t2156,t1490]) ).
cnf(t3238,plain,
multiply(additive_identity,additive_identity) = multiply(additive_identity,additive_inverse(X1)),
inference(step,[status(thm)],[t2157,t303]) ).
cnf(t2178,plain,
multiply(additive_identity,additive_inverse(X1)) = multiply(additive_identity,additive_identity),
inference(orient,[status(thm)],[t3238]) ).
cnf(t2181,plain,
multiply(additive_identity,additive_identity) = multiply(additive_identity,X1),
inference(cp,[status(thm)],[t2178,t1461]) ).
cnf(t2191,plain,
multiply(additive_identity,additive_identity) = multiply(additive_identity,X1),
inference(orient,[status(thm)],[t2181]) ).
cnf(t2199,plain,
multiply(additive_identity,X1) = multiply(additive_identity,X2),
inference(cp,[status(thm)],[t2191,t2191]) ).
cnf(t2215,plain,
multiply(additive_identity,X1) = multiply(additive_identity,X2),
inference(orient,[status(thm)],[t2199]) ).
cnf(t2218,plain,
multiply(add(additive_identity,a),b) = add(c,multiply(additive_identity,X1)),
inference(cp,[status(thm)],[t1536,t2215]) ).
cnf(t3241,plain,
multiply(a,b) = add(c,multiply(additive_identity,X1)),
inference(step,[status(thm)],[t2218,t258]) ).
cnf(t3242,plain,
c = add(c,multiply(additive_identity,X1)),
inference(step,[status(thm)],[t3241,t323]) ).
cnf(t2234,plain,
add(c,multiply(additive_identity,X1)) = c,
inference(orient,[status(thm)],[t3242]) ).
cnf(t2246,plain,
additive_inverse(multiply(additive_identity,X1)) = add(c,additive_inverse(c)),
inference(cp,[status(thm)],[t1638,t2234]) ).
cnf(t3243,plain,
additive_inverse(multiply(additive_identity,X1)) = additive_identity,
inference(step,[status(thm)],[t2246,t303]) ).
cnf(t2253,plain,
additive_inverse(multiply(additive_identity,X1)) = additive_identity,
inference(orient,[status(thm)],[t3243]) ).
cnf(t2260,plain,
multiply(additive_identity,X1) = additive_inverse(additive_identity),
inference(cp,[status(thm)],[t1461,t2253]) ).
cnf(t3244,plain,
multiply(additive_identity,X1) = additive_identity,
inference(step,[status(thm)],[t2260,t309]) ).
cnf(t2276,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t3244]) ).
cnf(t3280,plain,
additive_identity = add(c,additive_inverse(d)),
inference(step,[status(thm)],[t3279,t2276]) ).
cnf(t3152,plain,
add(c,additive_inverse(d)) = additive_identity,
inference(orient,[status(thm)],[t3280]) ).
cnf(goal_0,negated_conjecture,
d != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
d != add(d,multiply(additive_inverse(a),additive_identity)),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
d != add(multiply(additive_inverse(a),additive_identity),d),
inference(rw,[status(thm)],[g0_0,t263]) ).
cnf(g0_2,plain,
d != add(additive_identity,d),
inference(rw,[status(thm)],[g0_1,t2823]) ).
cnf(g0_3,plain,
d != add(add(c,additive_inverse(d)),d),
inference(rw,[status(thm)],[g0_2,t3152]) ).
cnf(g0_4,plain,
d != add(add(additive_inverse(d),c),d),
inference(rw,[status(thm)],[g0_3,t263]) ).
cnf(g0_5,plain,
d != add(d,add(additive_inverse(d),c)),
inference(rw,[status(thm)],[g0_4,t263]) ).
cnf(g0_6,plain,
d != c,
inference(rw,[status(thm)],[g0_5,t1444]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG004-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n015.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 07:44:25 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 33.53/4.75 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.53/4.75 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------