%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN214-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:19 AM UTC 2026
% Result : Unsatisfiable 3.38s 6.15s
% Output : CNFRefutation 3.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 28
% Syntax : Number of formulae : 325 ( 325 unt; 0 def)
% Number of atoms : 325 ( 324 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 : 25 ( 25 usr; 6 con; 0-4 aty)
% Number of variables : 565 ( 281 sgn 37 !; 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_3137,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_3137]) ).
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_3138,plain,
q0(b,b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_12]) ).
cnf(c_3139,plain,
q0(b,b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3138]) ).
cnf(c_13,plain,
q0(e,d) = q0(b,b),
inference(copy,[status(thm)],[c_3139]) ).
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_3140,plain,
p0(b,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_20]) ).
cnf(c_3141,plain,
p0(b,d) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3140]) ).
cnf(c_3142,plain,
p0(b,d) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3141]) ).
cnf(c_21,plain,
q0(b,b) = p0(b,d),
inference(copy,[status(thm)],[c_3142]) ).
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_3143,plain,
n0(e,b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_22]) ).
cnf(c_3144,plain,
n0(e,b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3143]) ).
cnf(c_3145,plain,
n0(e,b) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3144]) ).
cnf(c_23,plain,
n0(e,b) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_3145]) ).
fof(axiom_12,axiom,
! [VAR_0] : m0(a,VAR_0,a) = true,
file('theBenchmark.p',axiom_12) ).
cnf(c_24,plain,
m0(a,A,a) = true,
inference(clausify,[status(thm)],[axiom_12]) ).
cnf(c_3146,plain,
m0(a,A,a) = s0(d),
inference(paramod,[status(thm)],[c_3,c_24]) ).
cnf(c_3147,plain,
m0(a,A,a) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3146]) ).
cnf(c_3148,plain,
m0(a,A,a) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3147]) ).
cnf(c_25,plain,
m0(a,A,a) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_3148]) ).
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_3149,plain,
r0(e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_26]) ).
cnf(c_3150,plain,
r0(e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3149]) ).
cnf(c_3151,plain,
r0(e) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3150]) ).
cnf(c_27,plain,
r0(e) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_3151]) ).
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_3152,plain,
p0(b,A) = s0(d),
inference(paramod,[status(thm)],[c_3,c_28]) ).
cnf(c_3153,plain,
p0(b,A) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3152]) ).
cnf(c_3154,plain,
p0(b,A) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3153]) ).
cnf(c_3155,plain,
p0(b,A) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_3154]) ).
cnf(c_29,plain,
p0(b,d) = p0(b,A),
inference(copy,[status(thm)],[c_3155]) ).
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_3156,plain,
q0(A,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_34]) ).
cnf(c_3157,plain,
q0(A,d) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3156]) ).
cnf(c_3158,plain,
q0(A,d) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_3157]) ).
cnf(c_35,plain,
q0(A,d) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_3158]) ).
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_3159,plain,
p0(c,b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_36]) ).
cnf(c_3160,plain,
p0(c,b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3159]) ).
cnf(c_37,plain,
p0(c,b) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3160]) ).
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_3161,plain,
m0(A,d,B) = s0(d),
inference(paramod,[status(thm)],[c_3,c_38]) ).
cnf(c_3162,plain,
m0(A,d,B) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3161]) ).
cnf(c_39,plain,
m0(A,d,B) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3162]) ).
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_3163,plain,
k0(e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_54]) ).
cnf(c_3164,plain,
k0(e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3163]) ).
cnf(c_55,plain,
k0(e) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3164]) ).
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_3165,plain,
k0(b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_62]) ).
cnf(c_3166,plain,
k0(b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3165]) ).
cnf(c_63,plain,
k0(b) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3166]) ).
fof(rule_075,axiom,
ifeq(p0(b,a),true,p1(a,a,a),true) = true,
file('theBenchmark.p',rule_075) ).
cnf(c_219,plain,
ifeq(p0(b,a),true,p1(a,a,a),true) = true,
inference(clausify,[status(thm)],[rule_075]) ).
cnf(c_3167,plain,
ifeq(p0(b,d),true,p1(a,a,a),true) = true,
inference(paramod,[status(thm)],[c_29,c_219]) ).
cnf(c_3168,plain,
ifeq(p0(b,d),s0(d),p1(a,a,a),true) = true,
inference(paramod,[status(thm)],[c_3,c_3167]) ).
cnf(c_3169,plain,
ifeq(p0(b,d),q0(e,d),p1(a,a,a),true) = true,
inference(paramod,[status(thm)],[c_5,c_3168]) ).
cnf(c_3170,plain,
ifeq(p0(b,d),p0(b,d),p1(a,a,a),true) = true,
inference(paramod,[status(thm)],[c_35,c_3169]) ).
cnf(c_3171,plain,
ifeq(p0(b,d),p0(b,d),p1(a,a,a),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3170]) ).
cnf(c_3172,plain,
ifeq(p0(b,d),p0(b,d),p1(a,a,a),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3171]) ).
cnf(c_3173,plain,
ifeq(p0(b,d),p0(b,d),p1(a,a,a),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3172]) ).
cnf(c_3174,plain,
p1(a,a,a) = true,
inference(paramod,[status(thm)],[c_1,c_3173]) ).
cnf(c_3175,plain,
p1(a,a,a) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3174]) ).
cnf(c_3176,plain,
p1(a,a,a) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3175]) ).
cnf(c_220,plain,
p1(a,a,a) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3176]) ).
fof(rule_082,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq(p1(VAR_0,VAR_1,VAR_2),true,ifeq(m0(VAR_0,VAR_1,VAR_2),true,p1(VAR_1,VAR_3,VAR_0),true),true) = true,
file('theBenchmark.p',rule_082) ).
cnf(c_231,plain,
ifeq(p1(A,B,C),true,ifeq(m0(A,B,C),true,p1(B,D,A),true),true) = true,
inference(clausify,[status(thm)],[rule_082]) ).
cnf(c_3177,plain,
ifeq(p1(A,B,C),s0(d),ifeq(m0(A,B,C),true,p1(B,D,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_231]) ).
cnf(c_3178,plain,
ifeq(p1(A,B,C),q0(e,d),ifeq(m0(A,B,C),true,p1(B,D,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3177]) ).
cnf(c_3179,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),true,p1(B,D,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3178]) ).
cnf(c_3180,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),s0(d),p1(B,D,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3179]) ).
cnf(c_3181,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),q0(e,d),p1(B,D,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3180]) ).
cnf(c_3182,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3181]) ).
cnf(c_3183,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_3182]) ).
cnf(c_3184,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_3183]) ).
cnf(c_3185,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_3184]) ).
cnf(c_3186,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3185]) ).
cnf(c_3187,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3186]) ).
cnf(c_3188,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3187]) ).
cnf(c_3189,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3188]) ).
cnf(c_3190,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3189]) ).
cnf(c_232,plain,
ifeq(p1(A,B,C),p0(b,d),ifeq(m0(A,B,C),p0(b,d),p1(B,D,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3190]) ).
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_3191,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_3192,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_3191]) ).
cnf(c_3193,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_3192]) ).
cnf(c_3194,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_3193]) ).
cnf(c_3195,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_3194]) ).
cnf(c_3196,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_3195]) ).
cnf(c_3197,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_3196]) ).
cnf(c_3198,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_3197]) ).
cnf(c_3199,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_3198]) ).
cnf(c_3200,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_3199]) ).
cnf(c_3201,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_3200]) ).
cnf(c_3202,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),true) = true,
inference(paramod,[status(thm)],[c_1,c_3201]) ).
cnf(c_3203,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3202]) ).
cnf(c_3204,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3203]) ).
cnf(c_3205,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3204]) ).
cnf(c_3206,plain,
p1(e,e,e) = true,
inference(paramod,[status(thm)],[c_1,c_3205]) ).
cnf(c_3207,plain,
p1(e,e,e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3206]) ).
cnf(c_3208,plain,
p1(e,e,e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3207]) ).
cnf(c_247,plain,
p1(e,e,e) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3208]) ).
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_3209,plain,
ifeq(m0(A,B,C),s0(d),q1(C,C,C),true) = true,
inference(paramod,[status(thm)],[c_3,c_285]) ).
cnf(c_3210,plain,
ifeq(m0(A,B,C),q0(e,d),q1(C,C,C),true) = true,
inference(paramod,[status(thm)],[c_5,c_3209]) ).
cnf(c_3211,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),true) = true,
inference(paramod,[status(thm)],[c_35,c_3210]) ).
cnf(c_3212,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3211]) ).
cnf(c_3213,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3212]) ).
cnf(c_3214,plain,
ifeq(m0(A,B,C),p0(b,d),q1(C,C,C),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3213]) ).
cnf(c_3215,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_3214]) ).
cnf(c_3216,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_3215]) ).
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_3216]) ).
fof(rule_137,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(p1(VAR_0,VAR_1,VAR_2),true,n2(VAR_2),true) = true,
file('theBenchmark.p',rule_137) ).
cnf(c_335,plain,
ifeq(p1(A,B,C),true,n2(C),true) = true,
inference(clausify,[status(thm)],[rule_137]) ).
cnf(c_3217,plain,
ifeq(p1(A,B,C),s0(d),n2(C),true) = true,
inference(paramod,[status(thm)],[c_3,c_335]) ).
cnf(c_3218,plain,
ifeq(p1(A,B,C),q0(e,d),n2(C),true) = true,
inference(paramod,[status(thm)],[c_5,c_3217]) ).
cnf(c_3219,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),true) = true,
inference(paramod,[status(thm)],[c_35,c_3218]) ).
cnf(c_3220,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3219]) ).
cnf(c_3221,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3220]) ).
cnf(c_3222,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3221]) ).
cnf(c_3223,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3222]) ).
cnf(c_3224,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3223]) ).
cnf(c_336,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3224]) ).
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_3225,plain,
ifeq(q1(A,A,A),s0(d),p2(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_3,c_369]) ).
cnf(c_3226,plain,
ifeq(q1(A,A,A),q0(e,d),p2(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_5,c_3225]) ).
cnf(c_3227,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_35,c_3226]) ).
cnf(c_3228,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3227]) ).
cnf(c_3229,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3228]) ).
cnf(c_3230,plain,
ifeq(q1(A,A,A),p0(b,d),p2(A,A,A),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3229]) ).
cnf(c_3231,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_3230]) ).
cnf(c_3232,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_3231]) ).
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_3232]) ).
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_3233,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_3234,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_3233]) ).
cnf(c_3235,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_3234]) ).
cnf(c_3236,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_3235]) ).
cnf(c_3237,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_3236]) ).
cnf(c_3238,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_3237]) ).
cnf(c_3239,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_3238]) ).
cnf(c_3240,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_3239]) ).
cnf(c_3241,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_3240]) ).
cnf(c_3242,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_3241]) ).
cnf(c_3243,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_3242]) ).
cnf(c_3244,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_3243]) ).
cnf(c_3245,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_3244]) ).
cnf(c_3246,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_3245]) ).
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_3246]) ).
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_3247,plain,
ifeq(p2(A,B,C),s0(d),n3(C),true) = true,
inference(paramod,[status(thm)],[c_3,c_537]) ).
cnf(c_3248,plain,
ifeq(p2(A,B,C),q0(e,d),n3(C),true) = true,
inference(paramod,[status(thm)],[c_5,c_3247]) ).
cnf(c_3249,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),true) = true,
inference(paramod,[status(thm)],[c_35,c_3248]) ).
cnf(c_3250,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3249]) ).
cnf(c_3251,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3250]) ).
cnf(c_3252,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3251]) ).
cnf(c_3253,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3252]) ).
cnf(c_3254,plain,
ifeq(p2(A,B,C),p0(b,d),n3(C),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3253]) ).
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_3254]) ).
fof(rule_244,axiom,
! [VAR_0] : ifeq(n2(VAR_0),true,p3(VAR_0,VAR_0,VAR_0),true) = true,
file('theBenchmark.p',rule_244) ).
cnf(c_545,plain,
ifeq(n2(A),true,p3(A,A,A),true) = true,
inference(clausify,[status(thm)],[rule_244]) ).
cnf(c_3255,plain,
ifeq(n2(A),s0(d),p3(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_3,c_545]) ).
cnf(c_3256,plain,
ifeq(n2(A),q0(e,d),p3(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_5,c_3255]) ).
cnf(c_3257,plain,
ifeq(n2(A),p0(b,d),p3(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_35,c_3256]) ).
cnf(c_3258,plain,
ifeq(n2(A),p0(b,d),p3(A,A,A),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3257]) ).
cnf(c_3259,plain,
ifeq(n2(A),p0(b,d),p3(A,A,A),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3258]) ).
cnf(c_3260,plain,
ifeq(n2(A),p0(b,d),p3(A,A,A),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3259]) ).
cnf(c_3261,plain,
ifeq(n2(A),p0(b,d),p3(A,A,A),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3260]) ).
cnf(c_3262,plain,
ifeq(n2(A),p0(b,d),p3(A,A,A),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3261]) ).
cnf(c_546,plain,
ifeq(n2(A),p0(b,d),p3(A,A,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3262]) ).
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_3263,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_3264,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_3263]) ).
cnf(c_3265,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_3264]) ).
cnf(c_3266,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_3265]) ).
cnf(c_3267,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_3266]) ).
cnf(c_3268,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_3267]) ).
cnf(c_3269,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_3268]) ).
cnf(c_3270,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_3269]) ).
cnf(c_3271,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_3270]) ).
cnf(c_3272,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_3271]) ).
cnf(c_3273,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_3272]) ).
cnf(c_3274,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_3273]) ).
cnf(c_3275,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_3274]) ).
cnf(c_3276,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_3275]) ).
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_3276]) ).
fof(rule_277,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(p3(VAR_0,VAR_1,VAR_2),true,l4(VAR_2),true) = true,
file('theBenchmark.p',rule_277) ).
cnf(c_609,plain,
ifeq(p3(A,B,C),true,l4(C),true) = true,
inference(clausify,[status(thm)],[rule_277]) ).
cnf(c_3277,plain,
ifeq(p3(A,B,C),s0(d),l4(C),true) = true,
inference(paramod,[status(thm)],[c_3,c_609]) ).
cnf(c_3278,plain,
ifeq(p3(A,B,C),q0(e,d),l4(C),true) = true,
inference(paramod,[status(thm)],[c_5,c_3277]) ).
cnf(c_3279,plain,
ifeq(p3(A,B,C),p0(b,d),l4(C),true) = true,
inference(paramod,[status(thm)],[c_35,c_3278]) ).
cnf(c_3280,plain,
ifeq(p3(A,B,C),p0(b,d),l4(C),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3279]) ).
cnf(c_3281,plain,
ifeq(p3(A,B,C),p0(b,d),l4(C),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3280]) ).
cnf(c_3282,plain,
ifeq(p3(A,B,C),p0(b,d),l4(C),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3281]) ).
cnf(c_3283,plain,
ifeq(p3(A,B,C),p0(b,d),l4(C),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3282]) ).
cnf(c_3284,plain,
ifeq(p3(A,B,C),p0(b,d),l4(C),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3283]) ).
cnf(c_610,plain,
ifeq(p3(A,B,C),p0(b,d),l4(C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3284]) ).
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_3285,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_3286,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_3285]) ).
cnf(c_3287,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_3286]) ).
cnf(c_3288,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_3287]) ).
cnf(c_3289,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_3288]) ).
cnf(c_3290,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_3289]) ).
cnf(c_3291,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_3290]) ).
cnf(c_3292,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_3291]) ).
cnf(c_3293,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_3292]) ).
cnf(c_3294,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_3293]) ).
cnf(c_3295,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_3294]) ).
cnf(c_3296,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_3295]) ).
cnf(c_3297,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_3296]) ).
cnf(c_3298,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_3297]) ).
cnf(c_3299,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_3298]) ).
cnf(c_3300,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_3299]) ).
cnf(c_3301,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_3300]) ).
cnf(c_3302,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_3301]) ).
cnf(c_3303,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_3302]) ).
cnf(c_3304,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_3303]) ).
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_3304]) ).
fof(rule_329,axiom,
! [VAR_0,VAR_1] : ifeq(r4(VAR_0),true,ifeq(l4(VAR_1),true,s5(VAR_1),true),true) = true,
file('theBenchmark.p',rule_329) ).
cnf(c_711,plain,
ifeq(r4(A),true,ifeq(l4(B),true,s5(B),true),true) = true,
inference(clausify,[status(thm)],[rule_329]) ).
cnf(c_3305,plain,
ifeq(r4(A),s0(d),ifeq(l4(B),true,s5(B),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_711]) ).
cnf(c_3306,plain,
ifeq(r4(A),q0(e,d),ifeq(l4(B),true,s5(B),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3305]) ).
cnf(c_3307,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),true,s5(B),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3306]) ).
cnf(c_3308,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),s0(d),s5(B),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3307]) ).
cnf(c_3309,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),q0(e,d),s5(B),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_3308]) ).
cnf(c_3310,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_3309]) ).
cnf(c_3311,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_3310]) ).
cnf(c_3312,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_3311]) ).
cnf(c_3313,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_3312]) ).
cnf(c_3314,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3313]) ).
cnf(c_3315,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_3314]) ).
cnf(c_3316,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_3315]) ).
cnf(c_3317,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3316]) ).
cnf(c_3318,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3317]) ).
cnf(c_712,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3318]) ).
fof(prove_this,axiom,
s5(c) != true,
file('theBenchmark.p',prove_this) ).
cnf(c_715,plain,
s5(c) != true,
inference(clausify,[status(thm)],[prove_this]) ).
cnf(c_3319,plain,
s5(c) != s0(d),
inference(paramod,[status(thm)],[c_3,c_715]) ).
cnf(c_3320,plain,
s5(c) != q0(e,d),
inference(paramod,[status(thm)],[c_5,c_3319]) ).
cnf(c_716,plain,
s5(c) != p0(b,d),
inference(paramod,[status(thm)],[c_35,c_3320]) ).
cnf(c_725,plain,
p0(b,A) = p0(b,B),
inference(paramod,[status(thm)],[c_29,c_29]) ).
cnf(c_3321,plain,
ifeq(p1(a,A,a),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(A,B,a),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_25,c_232]) ).
cnf(c_893,plain,
ifeq(p1(a,A,a),p0(b,d),p1(A,B,a),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3321]) ).
cnf(c_3322,plain,
ifeq(p1(A,d,B),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(d,C,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_39,c_232]) ).
cnf(c_895,plain,
ifeq(p1(A,d,B),p0(b,d),p1(d,C,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3322]) ).
cnf(c_3323,plain,
ifeq(p0(b,d),p0(b,d),ifeq(m0(a,a,a),p0(b,d),p1(a,A,a),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_220,c_232]) ).
cnf(c_3324,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(a,A,a),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_25,c_3323]) ).
cnf(c_3325,plain,
ifeq(p0(b,d),p0(b,d),p1(a,A,a),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3324]) ).
cnf(c_901,plain,
p1(a,A,a) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3325]) ).
cnf(c_3326,plain,
ifeq(p0(b,d),p0(b,d),p1(A,B,a),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_901,c_893]) ).
cnf(c_904,plain,
p1(A,B,a) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3326]) ).
cnf(c_3327,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_3327]) ).
cnf(c_3328,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_3328]) ).
cnf(c_3329,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_3329]) ).
cnf(c_3330,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_3330]) ).
cnf(c_3331,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_3331]) ).
cnf(c_1417,plain,
ifeq(p1(A,B,C),p0(b,D),n2(C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_336]) ).
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_1685,plain,
ifeq(n2(A),p0(b,d),p3(A,A,A),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_546]) ).
cnf(c_1814,plain,
ifeq(p3(A,B,C),p0(b,D),l4(C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_610]) ).
cnf(c_2002,plain,
ifeq(r4(A),p0(b,d),ifeq(l4(B),p0(b,d),s5(B),p0(b,d)),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_712]) ).
cnf(c_2011,plain,
s5(c) != p0(b,A),
inference(paramod,[status(thm)],[c_725,c_716]) ).
cnf(c_3332,plain,
ifeq(p0(b,d),p0(b,d),p1(d,A,B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_904,c_895]) ).
cnf(c_2534,plain,
p1(d,A,B) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3332]) ).
cnf(c_3333,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_3333]) ).
cnf(c_2747,plain,
ifeq(p0(b,d),p0(b,A),n2(B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2534,c_1417]) ).
cnf(c_3334,plain,
p0(b,d) = n2(A),
inference(paramod,[status(thm)],[c_2747,c_1]) ).
cnf(c_2748,plain,
n2(A) = p0(b,d),
inference(copy,[status(thm)],[c_3334]) ).
cnf(c_3335,plain,
ifeq(p0(b,d),p0(b,d),p3(A,A,A),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_2748,c_1685]) ).
cnf(c_2756,plain,
p3(A,A,A) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3335]) ).
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_3336,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_3336]) ).
cnf(c_3337,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_3337]) ).
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_2917,plain,
ifeq(p0(b,d),p0(b,A),l4(B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2756,c_1814]) ).
cnf(c_3338,plain,
p0(b,d) = l4(A),
inference(paramod,[status(thm)],[c_2917,c_1]) ).
cnf(c_2918,plain,
l4(A) = p0(b,d),
inference(copy,[status(thm)],[c_3338]) ).
cnf(c_3339,plain,
ifeq(r4(A),p0(b,d),ifeq(p0(b,d),p0(b,d),s5(B),p0(b,d)),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_2918,c_2002]) ).
cnf(c_2924,plain,
ifeq(r4(A),p0(b,d),s5(B),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_3339]) ).
cnf(c_2948,plain,
ifeq(r4(A),p0(b,B),s5(C),p0(b,D)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_2924]) ).
cnf(c_3340,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_3340]) ).
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_3341,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_3341]) ).
cnf(c_3124,plain,
ifeq(p0(b,d),p0(b,A),s5(B),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_3121,c_2948]) ).
cnf(c_3342,plain,
p0(b,d) = s5(A),
inference(paramod,[status(thm)],[c_3124,c_1]) ).
cnf(c_3135,plain,
s5(A) = p0(b,d),
inference(copy,[status(thm)],[c_3342]) ).
cnf(c_3136,plain,
$false,
inference(resolve,[status(thm)],[c_3135,c_2011]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN214-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.59 % Computer : n017.cluster.edu
% 0.10/5.59 % Model : x86_64 x86_64
% 0.10/5.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.59 % Memory : 8046.5625MB
% 0.10/5.59 % OS : Linux 6.8.0-71-generic
% 0.10/5.59 % CPULimit : 300
% 0.10/5.59 % WCLimit : 300
% 0.10/5.59 % DateTime : Sat Sep 26 17:17:54 UTC 2026
% 0.10/5.60 % CPUTime :
% 0.16/5.60 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/5.60 % Process 1253611 was started by sandbox2 on n017,
% 0.16/5.60 % Sat Sep 26 17:17:54 2026
% 0.16/5.60 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/5.61
% 0.16/5.61 % From the command line: assign(max_seconds, 300).
% 3.38/6.15
% 3.38/6.15 % 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)])].
% 3.38/6.15
% 3.38/6.15 % SZS status Unsatisfiable for theBenchmark
% 3.38/6.15
% 3.38/6.15 % Proof 1 at 0.46 (+ 0.06) seconds.
% 3.38/6.15 % Length of proof is 91.
% 3.38/6.15 % Level of proof is 19.
% 3.38/6.15 % Maximum clause weight is 60.000.
% 3.38/6.15 % Given clauses 737.
% 3.38/6.15
% 3.38/6.15 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------