%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN193-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 : Sun Sep 27 09:37:16 AM UTC 2026
% Result : Unsatisfiable 11.42s 1.97s
% Output : CNFRefutation 11.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 21
% Syntax : Number of formulae : 209 ( 209 unt; 0 def)
% Number of atoms : 209 ( 208 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 5 con; 0-4 aty)
% Number of variables : 319 ( 153 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(axiom_1,axiom,
s0(d) = true,
file('theBenchmark.p',axiom_1) ).
cnf(c_2,plain,
s0(d) = true,
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_3,plain,
true = s0(d),
inference(copy,[status(thm)],[c_2]) ).
fof(axiom_2,axiom,
q0(e,d) = true,
file('theBenchmark.p',axiom_2) ).
cnf(c_4,plain,
q0(e,d) = true,
inference(clausify,[status(thm)],[axiom_2]) ).
cnf(c_3123,plain,
q0(e,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_4]) ).
cnf(c_5,plain,
s0(d) = q0(e,d),
inference(copy,[status(thm)],[c_3123]) ).
fof(axiom_6,axiom,
q0(b,b) = true,
file('theBenchmark.p',axiom_6) ).
cnf(c_12,plain,
q0(b,b) = true,
inference(clausify,[status(thm)],[axiom_6]) ).
cnf(c_3124,plain,
q0(b,b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_12]) ).
cnf(c_3125,plain,
q0(b,b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3124]) ).
cnf(c_13,plain,
q0(e,d) = q0(b,b),
inference(copy,[status(thm)],[c_3125]) ).
fof(axiom_10,axiom,
p0(b,d) = true,
file('theBenchmark.p',axiom_10) ).
cnf(c_20,plain,
p0(b,d) = true,
inference(clausify,[status(thm)],[axiom_10]) ).
cnf(c_3126,plain,
p0(b,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_20]) ).
cnf(c_3127,plain,
p0(b,d) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3126]) ).
cnf(c_3128,plain,
p0(b,d) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3127]) ).
cnf(c_21,plain,
q0(b,b) = p0(b,d),
inference(copy,[status(thm)],[c_3128]) ).
fof(axiom_11,axiom,
n0(e,b) = true,
file('theBenchmark.p',axiom_11) ).
cnf(c_22,plain,
n0(e,b) = true,
inference(clausify,[status(thm)],[axiom_11]) ).
cnf(c_3129,plain,
n0(e,b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_22]) ).
cnf(c_3130,plain,
n0(e,b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3129]) ).
cnf(c_3131,plain,
n0(e,b) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3130]) ).
cnf(c_23,plain,
n0(e,b) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_3131]) ).
fof(axiom_13,axiom,
r0(e) = true,
file('theBenchmark.p',axiom_13) ).
cnf(c_26,plain,
r0(e) = true,
inference(clausify,[status(thm)],[axiom_13]) ).
cnf(c_3132,plain,
r0(e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_26]) ).
cnf(c_3133,plain,
r0(e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3132]) ).
cnf(c_3134,plain,
r0(e) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3133]) ).
cnf(c_27,plain,
r0(e) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_3134]) ).
fof(axiom_14,axiom,
! [VAR_0] : p0(b,VAR_0) = true,
file('theBenchmark.p',axiom_14) ).
cnf(c_28,plain,
p0(b,A) = true,
inference(clausify,[status(thm)],[axiom_14]) ).
cnf(c_3135,plain,
p0(b,A) = s0(d),
inference(paramod,[status(thm)],[c_3,c_28]) ).
cnf(c_3136,plain,
p0(b,A) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3135]) ).
cnf(c_3137,plain,
p0(b,A) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3136]) ).
cnf(c_3138,plain,
p0(b,A) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_3137]) ).
cnf(c_29,plain,
p0(b,d) = p0(b,A),
inference(copy,[status(thm)],[c_3138]) ).
fof(axiom_17,axiom,
! [VAR_0] : q0(VAR_0,d) = true,
file('theBenchmark.p',axiom_17) ).
cnf(c_34,plain,
q0(A,d) = true,
inference(clausify,[status(thm)],[axiom_17]) ).
cnf(c_3139,plain,
q0(A,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_34]) ).
cnf(c_3140,plain,
q0(A,d) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3139]) ).
cnf(c_3141,plain,
q0(A,d) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3140]) ).
cnf(c_35,plain,
q0(A,d) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_3141]) ).
fof(axiom_18,axiom,
p0(c,b) = true,
file('theBenchmark.p',axiom_18) ).
cnf(c_36,plain,
p0(c,b) = true,
inference(clausify,[status(thm)],[axiom_18]) ).
cnf(c_3142,plain,
p0(c,b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_36]) ).
cnf(c_3143,plain,
p0(c,b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3142]) ).
cnf(c_37,plain,
p0(c,b) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3143]) ).
fof(axiom_19,axiom,
! [VAR_0,VAR_1] : m0(VAR_0,d,VAR_1) = true,
file('theBenchmark.p',axiom_19) ).
cnf(c_38,plain,
m0(A,d,B) = true,
inference(clausify,[status(thm)],[axiom_19]) ).
cnf(c_3144,plain,
m0(A,d,B) = s0(d),
inference(paramod,[status(thm)],[c_3,c_38]) ).
cnf(c_3145,plain,
m0(A,d,B) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3144]) ).
cnf(c_39,plain,
m0(A,d,B) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3145]) ).
fof(axiom_28,axiom,
k0(e) = true,
file('theBenchmark.p',axiom_28) ).
cnf(c_54,plain,
k0(e) = true,
inference(clausify,[status(thm)],[axiom_28]) ).
cnf(c_3146,plain,
k0(e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_54]) ).
cnf(c_3147,plain,
k0(e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3146]) ).
cnf(c_55,plain,
k0(e) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3147]) ).
fof(axiom_32,axiom,
k0(b) = true,
file('theBenchmark.p',axiom_32) ).
cnf(c_62,plain,
k0(b) = true,
inference(clausify,[status(thm)],[axiom_32]) ).
cnf(c_3148,plain,
k0(b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_62]) ).
cnf(c_3149,plain,
k0(b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3148]) ).
cnf(c_63,plain,
k0(b) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3149]) ).
fof(rule_090,axiom,
ifeq(k0(e),true,ifeq(r0(e),true,p1(e,e,e),true),true) = true,
file('theBenchmark.p',rule_090) ).
cnf(c_246,plain,
ifeq(k0(e),true,ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(clausify,[status(thm)],[rule_090]) ).
cnf(c_3150,plain,
ifeq(p0(b,d),true,ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_55,c_246]) ).
cnf(c_3151,plain,
ifeq(p0(b,d),s0(d),ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3150]) ).
cnf(c_3152,plain,
ifeq(p0(b,d),q0(e,d),ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3151]) ).
cnf(c_3153,plain,
ifeq(p0(b,d),p0(b,d),ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3152]) ).
cnf(c_3154,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_27,c_3153]) ).
cnf(c_3155,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),s0(d),p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3154]) ).
cnf(c_3156,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),q0(e,d),p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3155]) ).
cnf(c_3157,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3156]) ).
cnf(c_3158,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(e,e,e),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_3157]) ).
cnf(c_3159,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(e,e,e),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_3158]) ).
cnf(c_3160,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(e,e,e),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_3159]) ).
cnf(c_3161,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),true) = true,
inference(paramod,[status(thm)],[c_1,c_3160]) ).
cnf(c_3162,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3161]) ).
cnf(c_3163,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3162]) ).
cnf(c_3164,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3163]) ).
cnf(c_3165,plain,
p1(e,e,e) = true,
inference(paramod,[status(thm)],[c_1,c_3164]) ).
cnf(c_3166,plain,
p1(e,e,e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3165]) ).
cnf(c_3167,plain,
p1(e,e,e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3166]) ).
cnf(c_247,plain,
p1(e,e,e) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3167]) ).
fof(rule_110,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(m0(VAR_0,VAR_1,VAR_2),true,q1(VAR_2,VAR_2,VAR_2),true) = true,
file('theBenchmark.p',rule_110) ).
cnf(c_285,plain,
ifeq(m0(A,B,C),true,q1(C,C,C),true) = true,
inference(clausify,[status(thm)],[rule_110]) ).
cnf(c_3168,plain,
ifeq(m0(A,B,C),s0(d),q1(C,C,C),true) = true,
inference(paramod,[status(thm)],[c_3,c_285]) ).
cnf(c_3169,plain,
ifeq(m0(A,B,C),q0(e,d),q1(C,C,C),true) = true,
inference(paramod,[status(thm)],[c_5,c_3168]) ).
cnf(c_3170,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),true) = true,
inference(paramod,[status(thm)],[c_35,c_3169]) ).
cnf(c_3171,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3170]) ).
cnf(c_3172,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3171]) ).
cnf(c_3173,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3172]) ).
cnf(c_3174,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3173]) ).
cnf(c_3175,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3174]) ).
cnf(c_286,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3175]) ).
fof(rule_154,axiom,
! [VAR_0] : ifeq(q1(VAR_0,VAR_0,VAR_0),true,p2(VAR_0,VAR_0,VAR_0),true) = true,
file('theBenchmark.p',rule_154) ).
cnf(c_369,plain,
ifeq(q1(A,A,A),true,p2(A,A,A),true) = true,
inference(clausify,[status(thm)],[rule_154]) ).
cnf(c_3176,plain,
ifeq(q1(A,A,A),s0(d),p2(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_3,c_369]) ).
cnf(c_3177,plain,
ifeq(q1(A,A,A),q0(e,d),p2(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_5,c_3176]) ).
cnf(c_3178,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_35,c_3177]) ).
cnf(c_3179,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3178]) ).
cnf(c_3180,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3179]) ).
cnf(c_3181,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3180]) ).
cnf(c_3182,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3181]) ).
cnf(c_3183,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3182]) ).
cnf(c_370,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3183]) ).
fof(rule_177,axiom,
! [VAR_0,VAR_1] : ifeq(p1(VAR_0,VAR_0,VAR_0),true,ifeq(k0(VAR_1),true,q2(VAR_0,VAR_1,VAR_1),true),true) = true,
file('theBenchmark.p',rule_177) ).
cnf(c_415,plain,
ifeq(p1(A,A,A),true,ifeq(k0(B),true,q2(A,B,B),true),true) = true,
inference(clausify,[status(thm)],[rule_177]) ).
cnf(c_3184,plain,
ifeq(p1(A,A,A),s0(d),ifeq(k0(B),true,q2(A,B,B),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_415]) ).
cnf(c_3185,plain,
ifeq(p1(A,A,A),q0(e,d),ifeq(k0(B),true,q2(A,B,B),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3184]) ).
cnf(c_3186,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),true,q2(A,B,B),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3185]) ).
cnf(c_3187,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),s0(d),q2(A,B,B),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3186]) ).
cnf(c_3188,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),q0(e,d),q2(A,B,B),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3187]) ).
cnf(c_3189,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3188]) ).
cnf(c_3190,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_3189]) ).
cnf(c_3191,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_3190]) ).
cnf(c_3192,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_3191]) ).
cnf(c_3193,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3192]) ).
cnf(c_3194,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3193]) ).
cnf(c_3195,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3194]) ).
cnf(c_3196,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3195]) ).
cnf(c_3197,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3196]) ).
cnf(c_416,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(k0(B),p0(b,d),q2(A,B,B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3197]) ).
fof(rule_240,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(p2(VAR_0,VAR_1,VAR_2),true,n3(VAR_2),true) = true,
file('theBenchmark.p',rule_240) ).
cnf(c_537,plain,
ifeq(p2(A,B,C),true,n3(C),true) = true,
inference(clausify,[status(thm)],[rule_240]) ).
cnf(c_3198,plain,
ifeq(p2(A,B,C),s0(d),n3(C),true) = true,
inference(paramod,[status(thm)],[c_3,c_537]) ).
cnf(c_3199,plain,
ifeq(p2(A,B,C),q0(e,d),n3(C),true) = true,
inference(paramod,[status(thm)],[c_5,c_3198]) ).
cnf(c_3200,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),true) = true,
inference(paramod,[status(thm)],[c_35,c_3199]) ).
cnf(c_3201,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3200]) ).
cnf(c_3202,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3201]) ).
cnf(c_3203,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3202]) ).
cnf(c_3204,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3203]) ).
cnf(c_3205,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3204]) ).
cnf(c_538,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3205]) ).
fof(rule_255,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(q2(VAR_0,VAR_1,VAR_2),true,ifeq(n0(VAR_0,VAR_1),true,q3(VAR_1,VAR_2),true),true) = true,
file('theBenchmark.p',rule_255) ).
cnf(c_567,plain,
ifeq(q2(A,B,C),true,ifeq(n0(A,B),true,q3(B,C),true),true) = true,
inference(clausify,[status(thm)],[rule_255]) ).
cnf(c_3206,plain,
ifeq(q2(A,B,C),s0(d),ifeq(n0(A,B),true,q3(B,C),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_567]) ).
cnf(c_3207,plain,
ifeq(q2(A,B,C),q0(e,d),ifeq(n0(A,B),true,q3(B,C),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3206]) ).
cnf(c_3208,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),true,q3(B,C),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3207]) ).
cnf(c_3209,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),s0(d),q3(B,C),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3208]) ).
cnf(c_3210,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),q0(e,d),q3(B,C),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3209]) ).
cnf(c_3211,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3210]) ).
cnf(c_3212,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_3211]) ).
cnf(c_3213,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_3212]) ).
cnf(c_3214,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_3213]) ).
cnf(c_3215,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3214]) ).
cnf(c_3216,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3215]) ).
cnf(c_3217,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3216]) ).
cnf(c_3218,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3217]) ).
cnf(c_3219,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3218]) ).
cnf(c_568,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(n0(A,B),p0(b,d),q3(B,C),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3219]) ).
fof(rule_298,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq(q3(VAR_0,VAR_1),true,ifeq(n3(VAR_2),true,ifeq(p0(VAR_3,VAR_2),true,r4(VAR_2),true),true),true) = true,
file('theBenchmark.p',rule_298) ).
cnf(c_649,plain,
ifeq(q3(A,B),true,ifeq(n3(C),true,ifeq(p0(D,C),true,r4(C),true),true),true) = true,
inference(clausify,[status(thm)],[rule_298]) ).
cnf(c_3220,plain,
ifeq(q3(A,B),s0(d),ifeq(n3(C),true,ifeq(p0(D,C),true,r4(C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_649]) ).
cnf(c_3221,plain,
ifeq(q3(A,B),q0(e,d),ifeq(n3(C),true,ifeq(p0(D,C),true,r4(C),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3220]) ).
cnf(c_3222,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),true,ifeq(p0(D,C),true,r4(C),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3221]) ).
cnf(c_3223,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),s0(d),ifeq(p0(D,C),true,r4(C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3222]) ).
cnf(c_3224,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),q0(e,d),ifeq(p0(D,C),true,r4(C),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3223]) ).
cnf(c_3225,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),true,r4(C),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3224]) ).
cnf(c_3226,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),s0(d),r4(C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3225]) ).
cnf(c_3227,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),q0(e,d),r4(C),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3226]) ).
cnf(c_3228,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3227]) ).
cnf(c_3229,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),s0(d)),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3228]) ).
cnf(c_3230,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),q0(e,d)),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3229]) ).
cnf(c_3231,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3230]) ).
cnf(c_3232,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_3231]) ).
cnf(c_3233,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_3232]) ).
cnf(c_3234,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_3233]) ).
cnf(c_3235,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3234]) ).
cnf(c_3236,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3235]) ).
cnf(c_3237,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3236]) ).
cnf(c_3238,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3237]) ).
cnf(c_3239,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3238]) ).
cnf(c_650,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(C),p0(b,d),ifeq(p0(D,C),p0(b,d),r4(C),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3239]) ).
fof(prove_this,axiom,
r4(b) != true,
file('theBenchmark.p',prove_this) ).
cnf(c_715,plain,
r4(b) != true,
inference(clausify,[status(thm)],[prove_this]) ).
cnf(c_3240,plain,
r4(b) != s0(d),
inference(paramod,[status(thm)],[c_3,c_715]) ).
cnf(c_3241,plain,
r4(b) != q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3240]) ).
cnf(c_716,plain,
r4(b) != p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3241]) ).
cnf(c_725,plain,
p0(b,A) = p0(b,B),
inference(paramod,[status(thm)],[c_29,c_29]) ).
cnf(c_3242,plain,
ifeq(p0(b,d),p0(b,d),q1(A,A,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_39,c_286]) ).
cnf(c_961,plain,
q1(A,A,A) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3242]) ).
cnf(c_3243,plain,
ifeq(p0(b,d),p0(b,d),p2(A,A,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_961,c_370]) ).
cnf(c_963,plain,
p2(A,A,A) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3243]) ).
cnf(c_3244,plain,
ifeq(p0(b,d),p0(b,d),ifeq(k0(A),p0(b,d),q2(e,A,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_247,c_416]) ).
cnf(c_1029,plain,
ifeq(k0(A),p0(b,d),q2(e,A,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3244]) ).
cnf(c_3245,plain,
ifeq(q2(e,b,A),p0(b,d),ifeq(p0(b,d),p0(b,d),q3(b,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_23,c_568]) ).
cnf(c_1064,plain,
ifeq(q2(e,b,A),p0(b,d),q3(b,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3245]) ).
cnf(c_3246,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(b),p0(b,d),ifeq(p0(b,d),p0(b,d),r4(b),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_37,c_650]) ).
cnf(c_1092,plain,
ifeq(q3(A,B),p0(b,d),ifeq(n3(b),p0(b,d),r4(b),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3246]) ).
cnf(c_1666,plain,
ifeq(p2(A,B,C),p0(b,D),n3(C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_538]) ).
cnf(c_2011,plain,
r4(b) != p0(b,A),
inference(paramod,[status(thm)],[c_725,c_716]) ).
cnf(c_3247,plain,
ifeq(p0(b,d),p0(b,d),q2(e,b,b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_63,c_1029]) ).
cnf(c_2660,plain,
q2(e,b,b) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3247]) ).
cnf(c_2805,plain,
ifeq(p0(b,d),p0(b,A),n3(B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_963,c_1666]) ).
cnf(c_3248,plain,
p0(b,d) = n3(A),
inference(paramod,[status(thm)],[c_2805,c_1]) ).
cnf(c_2821,plain,
n3(A) = p0(b,d),
inference(copy,[status(thm)],[c_3248]) ).
cnf(c_3249,plain,
ifeq(q3(A,B),p0(b,d),ifeq(p0(b,d),p0(b,d),r4(b),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2821,c_1092]) ).
cnf(c_2848,plain,
ifeq(q3(A,B),p0(b,d),r4(b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3249]) ).
cnf(c_2855,plain,
ifeq(q3(A,B),p0(b,C),r4(b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_2848]) ).
cnf(c_2897,plain,
ifeq(q3(A,B),p0(b,C),r4(b),p0(b,D)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_2855]) ).
cnf(c_3250,plain,
ifeq(p0(b,d),p0(b,d),q3(b,b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2660,c_1064]) ).
cnf(c_3113,plain,
q3(b,b) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3250]) ).
cnf(c_3119,plain,
ifeq(p0(b,d),p0(b,A),r4(b),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_3113,c_2897]) ).
cnf(c_3251,plain,
p0(b,d) = r4(b),
inference(paramod,[status(thm)],[c_3119,c_1]) ).
cnf(c_3121,plain,
r4(b) = p0(b,d),
inference(copy,[status(thm)],[c_3251]) ).
cnf(c_3122,plain,
$false,
inference(resolve,[status(thm)],[c_3121,c_2011]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN193-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n014.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 17:19:31 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 3712868 was started by sandbox on n014,
% 0.17/0.45 % Sat Sep 26 17:19:31 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/0.47
% 0.17/0.47 % From the command line: assign(max_seconds, 300).
% 11.42/1.97
% 11.42/1.97 % given #500 (A,wt=49): 885 ifeq(n1(A,B,C),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),p0(b,d)) = p0(b,d). [para(41(a,1),228(a,1,3,1)),rewrite([1(23)])].
% 11.42/1.97
% 11.42/1.97 % SZS status Unsatisfiable for theBenchmark
% 11.42/1.97
% 11.42/1.97 % Proof 1 at 1.27 (+ 0.19) seconds.
% 11.42/1.97 % Length of proof is 59.
% 11.42/1.97 % Level of proof is 16.
% 11.42/1.97 % Maximum clause weight is 60.000.
% 11.42/1.97 % Given clauses 729.
% 11.42/1.97
% 11.42/1.97 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------