%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN143-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:08 AM UTC 2026
% Result : Unsatisfiable 34.14s 4.76s
% Output : CNFRefutation 34.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 35
% Syntax : Number of formulae : 530 ( 530 unt; 0 def)
% Number of atoms : 530 ( 529 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 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 5 con; 0-4 aty)
% Number of variables : 1187 ( 349 sgn 57 !; 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_4970,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_4970]) ).
fof(axiom_5,axiom,
s0(b) = true,
file('theBenchmark.p',axiom_5) ).
cnf(c_10,plain,
s0(b) = true,
inference(clausify,[status(thm)],[axiom_5]) ).
cnf(c_4971,plain,
s0(b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_10]) ).
cnf(c_11,plain,
s0(b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4971]) ).
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_4972,plain,
q0(b,b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_12]) ).
cnf(c_4973,plain,
q0(b,b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4972]) ).
cnf(c_13,plain,
q0(e,d) = q0(b,b),
inference(copy,[status(thm)],[c_4973]) ).
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_4974,plain,
p0(b,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_20]) ).
cnf(c_4975,plain,
p0(b,d) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4974]) ).
cnf(c_4976,plain,
p0(b,d) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_4975]) ).
cnf(c_21,plain,
q0(b,b) = p0(b,d),
inference(copy,[status(thm)],[c_4976]) ).
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_4977,plain,
n0(e,b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_22]) ).
cnf(c_4978,plain,
n0(e,b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4977]) ).
cnf(c_4979,plain,
n0(e,b) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_4978]) ).
cnf(c_23,plain,
n0(e,b) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_4979]) ).
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_4980,plain,
r0(e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_26]) ).
cnf(c_4981,plain,
r0(e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4980]) ).
cnf(c_4982,plain,
r0(e) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_4981]) ).
cnf(c_27,plain,
r0(e) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_4982]) ).
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_4983,plain,
p0(b,A) = s0(d),
inference(paramod,[status(thm)],[c_3,c_28]) ).
cnf(c_4984,plain,
p0(b,A) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4983]) ).
cnf(c_4985,plain,
p0(b,A) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_4984]) ).
cnf(c_4986,plain,
p0(b,A) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_4985]) ).
cnf(c_29,plain,
p0(b,d) = p0(b,A),
inference(copy,[status(thm)],[c_4986]) ).
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_4987,plain,
q0(A,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_34]) ).
cnf(c_4988,plain,
q0(A,d) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4987]) ).
cnf(c_4989,plain,
q0(A,d) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_4988]) ).
cnf(c_35,plain,
q0(A,d) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_4989]) ).
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_4990,plain,
m0(A,d,B) = s0(d),
inference(paramod,[status(thm)],[c_3,c_38]) ).
cnf(c_4991,plain,
m0(A,d,B) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4990]) ).
cnf(c_39,plain,
m0(A,d,B) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_4991]) ).
fof(axiom_20,axiom,
l0(a) = true,
file('theBenchmark.p',axiom_20) ).
cnf(c_40,plain,
l0(a) = true,
inference(clausify,[status(thm)],[axiom_20]) ).
cnf(c_4992,plain,
l0(a) = s0(d),
inference(paramod,[status(thm)],[c_3,c_40]) ).
cnf(c_4993,plain,
l0(a) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4992]) ).
cnf(c_41,plain,
l0(a) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_4993]) ).
fof(axiom_30,axiom,
n0(e,e) = true,
file('theBenchmark.p',axiom_30) ).
cnf(c_58,plain,
n0(e,e) = true,
inference(clausify,[status(thm)],[axiom_30]) ).
cnf(c_4994,plain,
n0(e,e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_58]) ).
cnf(c_4995,plain,
n0(e,e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4994]) ).
cnf(c_59,plain,
n0(e,e) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_4995]) ).
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_4996,plain,
k0(b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_62]) ).
cnf(c_4997,plain,
k0(b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4996]) ).
cnf(c_63,plain,
k0(b) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_4997]) ).
fof(axiom_37,axiom,
n0(b,a) = true,
file('theBenchmark.p',axiom_37) ).
cnf(c_72,plain,
n0(b,a) = true,
inference(clausify,[status(thm)],[axiom_37]) ).
cnf(c_4998,plain,
n0(b,a) = s0(d),
inference(paramod,[status(thm)],[c_3,c_72]) ).
cnf(c_4999,plain,
n0(b,a) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_4998]) ).
cnf(c_73,plain,
n0(b,a) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_4999]) ).
fof(rule_001,axiom,
! [VAR_0,VAR_1] : ifeq(n0(VAR_0,VAR_1),true,k1(VAR_1),true) = true,
file('theBenchmark.p',rule_001) ).
cnf(c_76,plain,
ifeq(n0(A,B),true,k1(B),true) = true,
inference(clausify,[status(thm)],[rule_001]) ).
cnf(c_5000,plain,
ifeq(n0(A,B),s0(d),k1(B),true) = true,
inference(paramod,[status(thm)],[c_3,c_76]) ).
cnf(c_5001,plain,
ifeq(n0(A,B),q0(e,d),k1(B),true) = true,
inference(paramod,[status(thm)],[c_5,c_5000]) ).
cnf(c_5002,plain,
ifeq(n0(A,B),p0(b,d),k1(B),true) = true,
inference(paramod,[status(thm)],[c_35,c_5001]) ).
cnf(c_5003,plain,
ifeq(n0(A,B),p0(b,d),k1(B),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5002]) ).
cnf(c_5004,plain,
ifeq(n0(A,B),p0(b,d),k1(B),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5003]) ).
cnf(c_5005,plain,
ifeq(n0(A,B),p0(b,d),k1(B),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5004]) ).
cnf(c_5006,plain,
ifeq(n0(A,B),p0(b,d),k1(B),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5005]) ).
cnf(c_5007,plain,
ifeq(n0(A,B),p0(b,d),k1(B),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5006]) ).
cnf(c_77,plain,
ifeq(n0(A,B),p0(b,d),k1(B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5007]) ).
fof(rule_002,axiom,
! [VAR_0,VAR_1] : ifeq(n0(VAR_0,VAR_1),true,l1(VAR_1,VAR_1),true) = true,
file('theBenchmark.p',rule_002) ).
cnf(c_78,plain,
ifeq(n0(A,B),true,l1(B,B),true) = true,
inference(clausify,[status(thm)],[rule_002]) ).
cnf(c_5008,plain,
ifeq(n0(A,B),s0(d),l1(B,B),true) = true,
inference(paramod,[status(thm)],[c_3,c_78]) ).
cnf(c_5009,plain,
ifeq(n0(A,B),q0(e,d),l1(B,B),true) = true,
inference(paramod,[status(thm)],[c_5,c_5008]) ).
cnf(c_5010,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),true) = true,
inference(paramod,[status(thm)],[c_35,c_5009]) ).
cnf(c_5011,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5010]) ).
cnf(c_5012,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5011]) ).
cnf(c_5013,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5012]) ).
cnf(c_5014,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5013]) ).
cnf(c_5015,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5014]) ).
cnf(c_79,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5015]) ).
fof(rule_003,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq(p0(VAR_0,VAR_1),true,ifeq(r0(VAR_2),true,ifeq(m0(VAR_3,VAR_1,VAR_0),true,l1(VAR_1,VAR_3),true),true),true) = true,
file('theBenchmark.p',rule_003) ).
cnf(c_80,plain,
ifeq(p0(A,B),true,ifeq(r0(C),true,ifeq(m0(D,B,A),true,l1(B,D),true),true),true) = true,
inference(clausify,[status(thm)],[rule_003]) ).
cnf(c_5016,plain,
ifeq(p0(A,B),s0(d),ifeq(r0(C),true,ifeq(m0(D,B,A),true,l1(B,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_80]) ).
cnf(c_5017,plain,
ifeq(p0(A,B),q0(e,d),ifeq(r0(C),true,ifeq(m0(D,B,A),true,l1(B,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5016]) ).
cnf(c_5018,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),true,ifeq(m0(D,B,A),true,l1(B,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5017]) ).
cnf(c_5019,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),s0(d),ifeq(m0(D,B,A),true,l1(B,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5018]) ).
cnf(c_5020,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),q0(e,d),ifeq(m0(D,B,A),true,l1(B,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5019]) ).
cnf(c_5021,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),true,l1(B,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5020]) ).
cnf(c_5022,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),s0(d),l1(B,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5021]) ).
cnf(c_5023,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),q0(e,d),l1(B,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5022]) ).
cnf(c_5024,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5023]) ).
cnf(c_5025,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),s0(d)),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5024]) ).
cnf(c_5026,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),q0(e,d)),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5025]) ).
cnf(c_5027,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5026]) ).
cnf(c_5028,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5027]) ).
cnf(c_5029,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5028]) ).
cnf(c_5030,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5029]) ).
cnf(c_5031,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5030]) ).
cnf(c_5032,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5031]) ).
cnf(c_5033,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5032]) ).
cnf(c_5034,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5033]) ).
cnf(c_5035,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5034]) ).
cnf(c_81,plain,
ifeq(p0(A,B),p0(b,d),ifeq(r0(C),p0(b,d),ifeq(m0(D,B,A),p0(b,d),l1(B,D),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5035]) ).
fof(rule_050,axiom,
! [VAR_0,VAR_1] : ifeq(l0(VAR_0),true,ifeq(p0(b,VAR_1),true,ifeq(s0(b),true,n1(VAR_0,VAR_1,VAR_0),true),true),true) = true,
file('theBenchmark.p',rule_050) ).
cnf(c_169,plain,
ifeq(l0(A),true,ifeq(p0(b,B),true,ifeq(s0(b),true,n1(A,B,A),true),true),true) = true,
inference(clausify,[status(thm)],[rule_050]) ).
cnf(c_5036,plain,
ifeq(l0(A),s0(d),ifeq(p0(b,B),true,ifeq(s0(b),true,n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_169]) ).
cnf(c_5037,plain,
ifeq(l0(A),q0(e,d),ifeq(p0(b,B),true,ifeq(s0(b),true,n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5036]) ).
cnf(c_5038,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),true,ifeq(s0(b),true,n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5037]) ).
cnf(c_5039,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),s0(d),ifeq(s0(b),true,n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5038]) ).
cnf(c_5040,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),q0(e,d),ifeq(s0(b),true,n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5039]) ).
cnf(c_5041,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),ifeq(s0(b),true,n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5040]) ).
cnf(c_5042,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),ifeq(q0(e,d),true,n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_11,c_5041]) ).
cnf(c_5043,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),ifeq(p0(b,d),true,n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5042]) ).
cnf(c_5044,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),ifeq(p0(b,d),s0(d),n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5043]) ).
cnf(c_5045,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),ifeq(p0(b,d),q0(e,d),n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5044]) ).
cnf(c_5046,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),ifeq(p0(b,d),p0(b,d),n1(A,B,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5045]) ).
cnf(c_5047,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),ifeq(p0(b,d),p0(b,d),n1(A,B,A),s0(d)),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5046]) ).
cnf(c_5048,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),ifeq(p0(b,d),p0(b,d),n1(A,B,A),q0(e,d)),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5047]) ).
cnf(c_5049,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),ifeq(p0(b,d),p0(b,d),n1(A,B,A),p0(b,d)),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5048]) ).
cnf(c_5050,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),true),true) = true,
inference(paramod,[status(thm)],[c_1,c_5049]) ).
cnf(c_5051,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5050]) ).
cnf(c_5052,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5051]) ).
cnf(c_5053,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5052]) ).
cnf(c_5054,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5053]) ).
cnf(c_5055,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5054]) ).
cnf(c_5056,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5055]) ).
cnf(c_5057,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5056]) ).
cnf(c_5058,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5057]) ).
cnf(c_170,plain,
ifeq(l0(A),p0(b,d),ifeq(p0(b,B),p0(b,d),n1(A,B,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5058]) ).
fof(rule_054,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(n1(VAR_0,VAR_1,VAR_0),true,ifeq(l0(VAR_2),true,ifeq(l1(VAR_2,VAR_0),true,n1(VAR_0,VAR_1,VAR_1),true),true),true) = true,
file('theBenchmark.p',rule_054) ).
cnf(c_177,plain,
ifeq(n1(A,B,A),true,ifeq(l0(C),true,ifeq(l1(C,A),true,n1(A,B,B),true),true),true) = true,
inference(clausify,[status(thm)],[rule_054]) ).
cnf(c_5059,plain,
ifeq(n1(A,B,A),s0(d),ifeq(l0(C),true,ifeq(l1(C,A),true,n1(A,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_177]) ).
cnf(c_5060,plain,
ifeq(n1(A,B,A),q0(e,d),ifeq(l0(C),true,ifeq(l1(C,A),true,n1(A,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5059]) ).
cnf(c_5061,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),true,ifeq(l1(C,A),true,n1(A,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5060]) ).
cnf(c_5062,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),s0(d),ifeq(l1(C,A),true,n1(A,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5061]) ).
cnf(c_5063,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),q0(e,d),ifeq(l1(C,A),true,n1(A,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5062]) ).
cnf(c_5064,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),true,n1(A,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5063]) ).
cnf(c_5065,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),s0(d),n1(A,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5064]) ).
cnf(c_5066,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),q0(e,d),n1(A,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5065]) ).
cnf(c_5067,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5066]) ).
cnf(c_5068,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),s0(d)),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5067]) ).
cnf(c_5069,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),q0(e,d)),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5068]) ).
cnf(c_5070,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5069]) ).
cnf(c_5071,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5070]) ).
cnf(c_5072,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5071]) ).
cnf(c_5073,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5072]) ).
cnf(c_5074,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5073]) ).
cnf(c_5075,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5074]) ).
cnf(c_5076,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5075]) ).
cnf(c_5077,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5076]) ).
cnf(c_5078,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5077]) ).
cnf(c_178,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(l1(C,A),p0(b,d),n1(A,B,B),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5078]) ).
fof(rule_059,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq(m0(VAR_0,VAR_1,VAR_1),true,ifeq(m0(VAR_2,VAR_0,VAR_3),true,n1(VAR_3,VAR_3,VAR_2),true),true) = true,
file('theBenchmark.p',rule_059) ).
cnf(c_187,plain,
ifeq(m0(A,B,B),true,ifeq(m0(C,A,D),true,n1(D,D,C),true),true) = true,
inference(clausify,[status(thm)],[rule_059]) ).
cnf(c_5079,plain,
ifeq(m0(A,B,B),s0(d),ifeq(m0(C,A,D),true,n1(D,D,C),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_187]) ).
cnf(c_5080,plain,
ifeq(m0(A,B,B),q0(e,d),ifeq(m0(C,A,D),true,n1(D,D,C),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5079]) ).
cnf(c_5081,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),true,n1(D,D,C),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5080]) ).
cnf(c_5082,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),s0(d),n1(D,D,C),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5081]) ).
cnf(c_5083,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),q0(e,d),n1(D,D,C),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5082]) ).
cnf(c_5084,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5083]) ).
cnf(c_5085,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5084]) ).
cnf(c_5086,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5085]) ).
cnf(c_5087,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5086]) ).
cnf(c_5088,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5087]) ).
cnf(c_5089,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5088]) ).
cnf(c_5090,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5089]) ).
cnf(c_5091,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5090]) ).
cnf(c_5092,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5091]) ).
cnf(c_188,plain,
ifeq(m0(A,B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),n1(D,D,C),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5092]) ).
fof(rule_080,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq(n1(VAR_0,VAR_1,VAR_2),true,ifeq(l0(VAR_3),true,ifeq(n0(VAR_0,VAR_0),true,p1(VAR_2,VAR_2,VAR_2),true),true),true) = true,
file('theBenchmark.p',rule_080) ).
cnf(c_227,plain,
ifeq(n1(A,B,C),true,ifeq(l0(D),true,ifeq(n0(A,A),true,p1(C,C,C),true),true),true) = true,
inference(clausify,[status(thm)],[rule_080]) ).
cnf(c_5093,plain,
ifeq(n1(A,B,C),s0(d),ifeq(l0(D),true,ifeq(n0(A,A),true,p1(C,C,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_227]) ).
cnf(c_5094,plain,
ifeq(n1(A,B,C),q0(e,d),ifeq(l0(D),true,ifeq(n0(A,A),true,p1(C,C,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5093]) ).
cnf(c_5095,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),true,ifeq(n0(A,A),true,p1(C,C,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5094]) ).
cnf(c_5096,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),s0(d),ifeq(n0(A,A),true,p1(C,C,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5095]) ).
cnf(c_5097,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),q0(e,d),ifeq(n0(A,A),true,p1(C,C,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5096]) ).
cnf(c_5098,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),true,p1(C,C,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5097]) ).
cnf(c_5099,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),s0(d),p1(C,C,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5098]) ).
cnf(c_5100,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),q0(e,d),p1(C,C,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5099]) ).
cnf(c_5101,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5100]) ).
cnf(c_5102,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),s0(d)),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5101]) ).
cnf(c_5103,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),q0(e,d)),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5102]) ).
cnf(c_5104,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5103]) ).
cnf(c_5105,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5104]) ).
cnf(c_5106,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5105]) ).
cnf(c_5107,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5106]) ).
cnf(c_5108,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5107]) ).
cnf(c_5109,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5108]) ).
cnf(c_5110,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5109]) ).
cnf(c_5111,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5110]) ).
cnf(c_5112,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5111]) ).
cnf(c_228,plain,
ifeq(n1(A,B,C),p0(b,d),ifeq(l0(D),p0(b,d),ifeq(n0(A,A),p0(b,d),p1(C,C,C),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5112]) ).
fof(rule_125,axiom,
! [VAR_0] : ifeq(p0(VAR_0,VAR_0),true,s1(VAR_0),true) = true,
file('theBenchmark.p',rule_125) ).
cnf(c_313,plain,
ifeq(p0(A,A),true,s1(A),true) = true,
inference(clausify,[status(thm)],[rule_125]) ).
cnf(c_5113,plain,
ifeq(p0(A,A),s0(d),s1(A),true) = true,
inference(paramod,[status(thm)],[c_3,c_313]) ).
cnf(c_5114,plain,
ifeq(p0(A,A),q0(e,d),s1(A),true) = true,
inference(paramod,[status(thm)],[c_5,c_5113]) ).
cnf(c_5115,plain,
ifeq(p0(A,A),p0(b,d),s1(A),true) = true,
inference(paramod,[status(thm)],[c_35,c_5114]) ).
cnf(c_5116,plain,
ifeq(p0(A,A),p0(b,d),s1(A),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5115]) ).
cnf(c_5117,plain,
ifeq(p0(A,A),p0(b,d),s1(A),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5116]) ).
cnf(c_5118,plain,
ifeq(p0(A,A),p0(b,d),s1(A),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5117]) ).
cnf(c_5119,plain,
ifeq(p0(A,A),p0(b,d),s1(A),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5118]) ).
cnf(c_5120,plain,
ifeq(p0(A,A),p0(b,d),s1(A),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5119]) ).
cnf(c_314,plain,
ifeq(p0(A,A),p0(b,d),s1(A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5120]) ).
fof(rule_126,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(s1(VAR_0),true,ifeq(q0(VAR_1,VAR_2),true,s1(VAR_1),true),true) = true,
file('theBenchmark.p',rule_126) ).
cnf(c_315,plain,
ifeq(s1(A),true,ifeq(q0(B,C),true,s1(B),true),true) = true,
inference(clausify,[status(thm)],[rule_126]) ).
cnf(c_5121,plain,
ifeq(s1(A),s0(d),ifeq(q0(B,C),true,s1(B),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_315]) ).
cnf(c_5122,plain,
ifeq(s1(A),q0(e,d),ifeq(q0(B,C),true,s1(B),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5121]) ).
cnf(c_5123,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),true,s1(B),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5122]) ).
cnf(c_5124,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),s0(d),s1(B),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5123]) ).
cnf(c_5125,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),q0(e,d),s1(B),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5124]) ).
cnf(c_5126,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5125]) ).
cnf(c_5127,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5126]) ).
cnf(c_5128,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5127]) ).
cnf(c_5129,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5128]) ).
cnf(c_5130,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5129]) ).
cnf(c_5131,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5130]) ).
cnf(c_5132,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5131]) ).
cnf(c_5133,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5132]) ).
cnf(c_5134,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5133]) ).
cnf(c_316,plain,
ifeq(s1(A),p0(b,d),ifeq(q0(B,C),p0(b,d),s1(B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5134]) ).
fof(rule_133,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq(s1(VAR_0),true,ifeq(p0(VAR_1,VAR_1),true,ifeq(m0(VAR_2,VAR_0,VAR_3),true,l2(VAR_3,VAR_3),true),true),true) = true,
file('theBenchmark.p',rule_133) ).
cnf(c_327,plain,
ifeq(s1(A),true,ifeq(p0(B,B),true,ifeq(m0(C,A,D),true,l2(D,D),true),true),true) = true,
inference(clausify,[status(thm)],[rule_133]) ).
cnf(c_5135,plain,
ifeq(s1(A),s0(d),ifeq(p0(B,B),true,ifeq(m0(C,A,D),true,l2(D,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_327]) ).
cnf(c_5136,plain,
ifeq(s1(A),q0(e,d),ifeq(p0(B,B),true,ifeq(m0(C,A,D),true,l2(D,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5135]) ).
cnf(c_5137,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),true,ifeq(m0(C,A,D),true,l2(D,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5136]) ).
cnf(c_5138,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),s0(d),ifeq(m0(C,A,D),true,l2(D,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5137]) ).
cnf(c_5139,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),q0(e,d),ifeq(m0(C,A,D),true,l2(D,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5138]) ).
cnf(c_5140,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),true,l2(D,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5139]) ).
cnf(c_5141,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),s0(d),l2(D,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5140]) ).
cnf(c_5142,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),q0(e,d),l2(D,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5141]) ).
cnf(c_5143,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5142]) ).
cnf(c_5144,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),s0(d)),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5143]) ).
cnf(c_5145,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),q0(e,d)),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5144]) ).
cnf(c_5146,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5145]) ).
cnf(c_5147,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5146]) ).
cnf(c_5148,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5147]) ).
cnf(c_5149,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5148]) ).
cnf(c_5150,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5149]) ).
cnf(c_5151,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5150]) ).
cnf(c_5152,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5151]) ).
cnf(c_5153,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5152]) ).
cnf(c_5154,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5153]) ).
cnf(c_328,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(B,B),p0(b,d),ifeq(m0(C,A,D),p0(b,d),l2(D,D),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5154]) ).
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_5155,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_5156,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_5155]) ).
cnf(c_5157,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_5156]) ).
cnf(c_5158,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_5157]) ).
cnf(c_5159,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_5158]) ).
cnf(c_5160,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_5159]) ).
cnf(c_5161,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_5160]) ).
cnf(c_5162,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_5161]) ).
cnf(c_5163,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_5162]) ).
cnf(c_5164,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_5163]) ).
cnf(c_5165,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_5164]) ).
cnf(c_5166,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_5165]) ).
cnf(c_5167,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_5166]) ).
cnf(c_5168,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_5167]) ).
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_5168]) ).
fof(rule_179,axiom,
! [VAR_0,VAR_1] : ifeq(n1(VAR_0,VAR_0,VAR_1),true,ifeq(k1(VAR_1),true,q2(VAR_0,VAR_0,VAR_0),true),true) = true,
file('theBenchmark.p',rule_179) ).
cnf(c_419,plain,
ifeq(n1(A,A,B),true,ifeq(k1(B),true,q2(A,A,A),true),true) = true,
inference(clausify,[status(thm)],[rule_179]) ).
cnf(c_5169,plain,
ifeq(n1(A,A,B),s0(d),ifeq(k1(B),true,q2(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_419]) ).
cnf(c_5170,plain,
ifeq(n1(A,A,B),q0(e,d),ifeq(k1(B),true,q2(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5169]) ).
cnf(c_5171,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),true,q2(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5170]) ).
cnf(c_5172,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),s0(d),q2(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5171]) ).
cnf(c_5173,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),q0(e,d),q2(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5172]) ).
cnf(c_5174,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5173]) ).
cnf(c_5175,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5174]) ).
cnf(c_5176,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5175]) ).
cnf(c_5177,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5176]) ).
cnf(c_5178,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5177]) ).
cnf(c_5179,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5178]) ).
cnf(c_5180,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5179]) ).
cnf(c_5181,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5180]) ).
cnf(c_5182,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5181]) ).
cnf(c_420,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5182]) ).
fof(rule_182,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(q2(VAR_0,VAR_1,VAR_2),true,ifeq(p1(VAR_2,VAR_2,VAR_1),true,ifeq(n1(VAR_0,VAR_2,VAR_1),true,q2(VAR_2,VAR_0,VAR_2),true),true),true) = true,
file('theBenchmark.p',rule_182) ).
cnf(c_425,plain,
ifeq(q2(A,B,C),true,ifeq(p1(C,C,B),true,ifeq(n1(A,C,B),true,q2(C,A,C),true),true),true) = true,
inference(clausify,[status(thm)],[rule_182]) ).
cnf(c_5183,plain,
ifeq(q2(A,B,C),s0(d),ifeq(p1(C,C,B),true,ifeq(n1(A,C,B),true,q2(C,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_425]) ).
cnf(c_5184,plain,
ifeq(q2(A,B,C),q0(e,d),ifeq(p1(C,C,B),true,ifeq(n1(A,C,B),true,q2(C,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5183]) ).
cnf(c_5185,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),true,ifeq(n1(A,C,B),true,q2(C,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5184]) ).
cnf(c_5186,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),s0(d),ifeq(n1(A,C,B),true,q2(C,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5185]) ).
cnf(c_5187,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),q0(e,d),ifeq(n1(A,C,B),true,q2(C,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5186]) ).
cnf(c_5188,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),true,q2(C,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5187]) ).
cnf(c_5189,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),s0(d),q2(C,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5188]) ).
cnf(c_5190,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),q0(e,d),q2(C,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5189]) ).
cnf(c_5191,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5190]) ).
cnf(c_5192,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),s0(d)),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5191]) ).
cnf(c_5193,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),q0(e,d)),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5192]) ).
cnf(c_5194,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5193]) ).
cnf(c_5195,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5194]) ).
cnf(c_5196,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5195]) ).
cnf(c_5197,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5196]) ).
cnf(c_5198,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5197]) ).
cnf(c_5199,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5198]) ).
cnf(c_5200,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5199]) ).
cnf(c_5201,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5200]) ).
cnf(c_5202,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5201]) ).
cnf(c_426,plain,
ifeq(q2(A,B,C),p0(b,d),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5202]) ).
fof(rule_189,axiom,
! [VAR_0] : ifeq(q2(b,VAR_0,b),true,ifeq(s1(b),true,s2(VAR_0),true),true) = true,
file('theBenchmark.p',rule_189) ).
cnf(c_439,plain,
ifeq(q2(b,A,b),true,ifeq(s1(b),true,s2(A),true),true) = true,
inference(clausify,[status(thm)],[rule_189]) ).
cnf(c_5203,plain,
ifeq(q2(b,A,b),s0(d),ifeq(s1(b),true,s2(A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_439]) ).
cnf(c_5204,plain,
ifeq(q2(b,A,b),q0(e,d),ifeq(s1(b),true,s2(A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5203]) ).
cnf(c_5205,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),true,s2(A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5204]) ).
cnf(c_5206,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),s0(d),s2(A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5205]) ).
cnf(c_5207,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),q0(e,d),s2(A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5206]) ).
cnf(c_5208,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5207]) ).
cnf(c_5209,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5208]) ).
cnf(c_5210,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5209]) ).
cnf(c_5211,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5210]) ).
cnf(c_5212,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5211]) ).
cnf(c_5213,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5212]) ).
cnf(c_5214,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5213]) ).
cnf(c_5215,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5214]) ).
cnf(c_5216,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5215]) ).
cnf(c_440,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5216]) ).
fof(rule_246,axiom,
! [VAR_0] : ifeq(l2(VAR_0,VAR_0),true,p3(VAR_0,VAR_0,VAR_0),true) = true,
file('theBenchmark.p',rule_246) ).
cnf(c_549,plain,
ifeq(l2(A,A),true,p3(A,A,A),true) = true,
inference(clausify,[status(thm)],[rule_246]) ).
cnf(c_5217,plain,
ifeq(l2(A,A),s0(d),p3(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_3,c_549]) ).
cnf(c_5218,plain,
ifeq(l2(A,A),q0(e,d),p3(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_5,c_5217]) ).
cnf(c_5219,plain,
ifeq(l2(A,A),p0(b,d),p3(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_35,c_5218]) ).
cnf(c_5220,plain,
ifeq(l2(A,A),p0(b,d),p3(A,A,A),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5219]) ).
cnf(c_5221,plain,
ifeq(l2(A,A),p0(b,d),p3(A,A,A),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5220]) ).
cnf(c_5222,plain,
ifeq(l2(A,A),p0(b,d),p3(A,A,A),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5221]) ).
cnf(c_5223,plain,
ifeq(l2(A,A),p0(b,d),p3(A,A,A),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5222]) ).
cnf(c_5224,plain,
ifeq(l2(A,A),p0(b,d),p3(A,A,A),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5223]) ).
cnf(c_550,plain,
ifeq(l2(A,A),p0(b,d),p3(A,A,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5224]) ).
fof(rule_273,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq(s2(VAR_0),true,ifeq(q2(VAR_1,VAR_0,VAR_1),true,ifeq(m0(VAR_1,VAR_2,VAR_3),true,s3(VAR_0,VAR_3),true),true),true) = true,
file('theBenchmark.p',rule_273) ).
cnf(c_603,plain,
ifeq(s2(A),true,ifeq(q2(B,A,B),true,ifeq(m0(B,C,D),true,s3(A,D),true),true),true) = true,
inference(clausify,[status(thm)],[rule_273]) ).
cnf(c_5225,plain,
ifeq(s2(A),s0(d),ifeq(q2(B,A,B),true,ifeq(m0(B,C,D),true,s3(A,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_603]) ).
cnf(c_5226,plain,
ifeq(s2(A),q0(e,d),ifeq(q2(B,A,B),true,ifeq(m0(B,C,D),true,s3(A,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5225]) ).
cnf(c_5227,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),true,ifeq(m0(B,C,D),true,s3(A,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5226]) ).
cnf(c_5228,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),s0(d),ifeq(m0(B,C,D),true,s3(A,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5227]) ).
cnf(c_5229,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),q0(e,d),ifeq(m0(B,C,D),true,s3(A,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5228]) ).
cnf(c_5230,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),true,s3(A,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5229]) ).
cnf(c_5231,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),s0(d),s3(A,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5230]) ).
cnf(c_5232,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),q0(e,d),s3(A,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5231]) ).
cnf(c_5233,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),true),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5232]) ).
cnf(c_5234,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),s0(d)),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5233]) ).
cnf(c_5235,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),q0(e,d)),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5234]) ).
cnf(c_5236,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5235]) ).
cnf(c_5237,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5236]) ).
cnf(c_5238,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5237]) ).
cnf(c_5239,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5238]) ).
cnf(c_5240,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5239]) ).
cnf(c_5241,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5240]) ).
cnf(c_5242,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5241]) ).
cnf(c_5243,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5242]) ).
cnf(c_5244,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5243]) ).
cnf(c_604,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(m0(B,C,D),p0(b,d),s3(A,D),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5244]) ).
fof(rule_279,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(s3(a,VAR_0),true,ifeq(l2(VAR_1,VAR_2),true,m4(VAR_0,VAR_2),true),true) = true,
file('theBenchmark.p',rule_279) ).
cnf(c_613,plain,
ifeq(s3(a,A),true,ifeq(l2(B,C),true,m4(A,C),true),true) = true,
inference(clausify,[status(thm)],[rule_279]) ).
cnf(c_5245,plain,
ifeq(s3(a,A),s0(d),ifeq(l2(B,C),true,m4(A,C),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_613]) ).
cnf(c_5246,plain,
ifeq(s3(a,A),q0(e,d),ifeq(l2(B,C),true,m4(A,C),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5245]) ).
cnf(c_5247,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),true,m4(A,C),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5246]) ).
cnf(c_5248,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),s0(d),m4(A,C),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5247]) ).
cnf(c_5249,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),q0(e,d),m4(A,C),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5248]) ).
cnf(c_5250,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5249]) ).
cnf(c_5251,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5250]) ).
cnf(c_5252,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5251]) ).
cnf(c_5253,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5252]) ).
cnf(c_5254,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5253]) ).
cnf(c_5255,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5254]) ).
cnf(c_5256,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5255]) ).
cnf(c_5257,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5256]) ).
cnf(c_5258,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5257]) ).
cnf(c_614,plain,
ifeq(s3(a,A),p0(b,d),ifeq(l2(B,C),p0(b,d),m4(A,C),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5258]) ).
fof(rule_299,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq(p3(VAR_0,VAR_1,VAR_2),true,ifeq(l1(VAR_3,VAR_1),true,s4(VAR_3),true),true) = true,
file('theBenchmark.p',rule_299) ).
cnf(c_651,plain,
ifeq(p3(A,B,C),true,ifeq(l1(D,B),true,s4(D),true),true) = true,
inference(clausify,[status(thm)],[rule_299]) ).
cnf(c_5259,plain,
ifeq(p3(A,B,C),s0(d),ifeq(l1(D,B),true,s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_651]) ).
cnf(c_5260,plain,
ifeq(p3(A,B,C),q0(e,d),ifeq(l1(D,B),true,s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5259]) ).
cnf(c_5261,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),true,s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5260]) ).
cnf(c_5262,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),s0(d),s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5261]) ).
cnf(c_5263,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),q0(e,d),s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5262]) ).
cnf(c_5264,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5263]) ).
cnf(c_5265,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5264]) ).
cnf(c_5266,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5265]) ).
cnf(c_5267,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5266]) ).
cnf(c_5268,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5267]) ).
cnf(c_5269,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5268]) ).
cnf(c_5270,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5269]) ).
cnf(c_5271,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5270]) ).
cnf(c_5272,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5271]) ).
cnf(c_652,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5272]) ).
fof(rule_305,axiom,
! [VAR_0] : ifeq(s4(VAR_0),true,ifeq(m4(e,e),true,m5(VAR_0,VAR_0),true),true) = true,
file('theBenchmark.p',rule_305) ).
cnf(c_663,plain,
ifeq(s4(A),true,ifeq(m4(e,e),true,m5(A,A),true),true) = true,
inference(clausify,[status(thm)],[rule_305]) ).
cnf(c_5273,plain,
ifeq(s4(A),s0(d),ifeq(m4(e,e),true,m5(A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_663]) ).
cnf(c_5274,plain,
ifeq(s4(A),q0(e,d),ifeq(m4(e,e),true,m5(A,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5273]) ).
cnf(c_5275,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),true,m5(A,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5274]) ).
cnf(c_5276,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),s0(d),m5(A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_5275]) ).
cnf(c_5277,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),q0(e,d),m5(A,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_5276]) ).
cnf(c_5278,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_5277]) ).
cnf(c_5279,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_5278]) ).
cnf(c_5280,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_5279]) ).
cnf(c_5281,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_5280]) ).
cnf(c_5282,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_5281]) ).
cnf(c_5283,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_5282]) ).
cnf(c_5284,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_5283]) ).
cnf(c_5285,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_5284]) ).
cnf(c_5286,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5285]) ).
cnf(c_664,plain,
ifeq(s4(A),p0(b,d),ifeq(m4(e,e),p0(b,d),m5(A,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5286]) ).
fof(prove_this,axiom,
m5(d,d) != true,
file('theBenchmark.p',prove_this) ).
cnf(c_715,plain,
m5(d,d) != true,
inference(clausify,[status(thm)],[prove_this]) ).
cnf(c_5287,plain,
m5(d,d) != s0(d),
inference(paramod,[status(thm)],[c_3,c_715]) ).
cnf(c_5288,plain,
m5(d,d) != q0(e,d),
inference(paramod,[status(thm)],[c_5,c_5287]) ).
cnf(c_716,plain,
m5(d,d) != p0(b,d),
inference(paramod,[status(thm)],[c_35,c_5288]) ).
cnf(c_725,plain,
p0(b,A) = p0(b,B),
inference(paramod,[status(thm)],[c_29,c_29]) ).
cnf(c_5289,plain,
ifeq(p0(b,d),p0(b,d),k1(b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_23,c_77]) ).
cnf(c_726,plain,
k1(b) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5289]) ).
cnf(c_5290,plain,
ifeq(p0(b,d),p0(b,d),l1(a,a),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_73,c_79]) ).
cnf(c_741,plain,
l1(a,a) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5290]) ).
cnf(c_5291,plain,
p0(b,d) = ifeq(r0(A),p0(b,d),ifeq(m0(B,d,b),p0(b,d),l1(d,B),p0(b,d)),p0(b,d)),
inference(paramod,[status(thm)],[c_81,c_1]) ).
cnf(c_5292,plain,
p0(b,d) = ifeq(r0(A),p0(b,d),ifeq(p0(b,d),p0(b,d),l1(d,B),p0(b,d)),p0(b,d)),
inference(paramod,[status(thm)],[c_39,c_5291]) ).
cnf(c_5293,plain,
p0(b,d) = ifeq(r0(A),p0(b,d),l1(d,B),p0(b,d)),
inference(paramod,[status(thm)],[c_1,c_5292]) ).
cnf(c_744,plain,
ifeq(r0(A),p0(b,d),l1(d,B),p0(b,d)) = p0(b,d),
inference(copy,[status(thm)],[c_5293]) ).
cnf(c_5294,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,A),p0(b,d),n1(a,A,a),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_41,c_170]) ).
cnf(c_832,plain,
ifeq(p0(b,A),p0(b,d),n1(a,A,a),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5294]) ).
cnf(c_5295,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(p0(b,d),p0(b,d),ifeq(l1(a,A),p0(b,d),n1(A,B,B),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_41,c_178]) ).
cnf(c_840,plain,
ifeq(n1(A,B,A),p0(b,d),ifeq(l1(a,A),p0(b,d),n1(A,B,B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5295]) ).
cnf(c_5296,plain,
ifeq(p0(b,d),p0(b,d),ifeq(m0(A,B,C),p0(b,d),n1(C,C,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_39,c_188]) ).
cnf(c_853,plain,
ifeq(m0(A,B,C),p0(b,d),n1(C,C,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5296]) ).
cnf(c_5297,plain,
ifeq(n1(e,A,B),p0(b,d),ifeq(l0(C),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(B,B,B),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_59,c_228]) ).
cnf(c_886,plain,
ifeq(n1(e,A,B),p0(b,d),ifeq(l0(C),p0(b,d),p1(B,B,B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5297]) ).
cnf(c_5298,plain,
ifeq(s1(A),p0(b,d),ifeq(p0(b,d),p0(b,d),s1(B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_316]) ).
cnf(c_994,plain,
ifeq(s1(A),p0(b,d),s1(B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5298]) ).
cnf(c_5299,plain,
ifeq(s1(d),p0(b,d),ifeq(p0(A,A),p0(b,d),ifeq(p0(b,d),p0(b,d),l2(B,B),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_39,c_328]) ).
cnf(c_1001,plain,
ifeq(s1(d),p0(b,d),ifeq(p0(A,A),p0(b,d),l2(B,B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5299]) ).
cnf(c_5300,plain,
ifeq(p1(A,A,A),p0(b,d),ifeq(p0(b,d),p0(b,d),q2(A,b,b),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_63,c_416]) ).
cnf(c_1028,plain,
ifeq(p1(A,A,A),p0(b,d),q2(A,b,b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5300]) ).
cnf(c_5301,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),ifeq(p0(b,d),p0(b,d),s3(A,C),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_39,c_604]) ).
cnf(c_1079,plain,
ifeq(s2(A),p0(b,d),ifeq(q2(B,A,B),p0(b,d),s3(A,C),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5301]) ).
cnf(c_1380,plain,
ifeq(p0(b,A),p0(b,d),s1(b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_314]) ).
cnf(c_1492,plain,
ifeq(n1(A,A,B),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),p0(b,C)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_420]) ).
cnf(c_1502,plain,
ifeq(q2(A,B,C),p0(b,D),ifeq(p1(C,C,B),p0(b,d),ifeq(n1(A,C,B),p0(b,d),q2(C,A,C),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_426]) ).
cnf(c_1525,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(s1(b),p0(b,d),s2(A),p0(b,d)),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_440]) ).
cnf(c_1693,plain,
ifeq(l2(A,A),p0(b,d),p3(A,A,A),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_550]) ).
cnf(c_1820,plain,
ifeq(s3(a,A),p0(b,B),ifeq(l2(C,D),p0(b,d),m4(A,D),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_614]) ).
cnf(c_1893,plain,
ifeq(p3(A,B,C),p0(b,D),ifeq(l1(E,B),p0(b,d),s4(E),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_652]) ).
cnf(c_1911,plain,
ifeq(s4(A),p0(b,B),ifeq(m4(e,e),p0(b,d),m5(A,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_664]) ).
cnf(c_2011,plain,
m5(d,d) != p0(b,A),
inference(paramod,[status(thm)],[c_725,c_716]) ).
cnf(c_5302,plain,
ifeq(p0(b,d),p0(b,d),l1(d,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_27,c_744]) ).
cnf(c_2039,plain,
l1(d,A) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5302]) ).
cnf(c_2099,plain,
ifeq(s1(A),p0(b,B),s1(C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_994]) ).
cnf(c_2120,plain,
ifeq(s1(A),p0(b,B),s1(C),p0(b,D)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_2099]) ).
cnf(c_5303,plain,
p0(b,d) = s1(b),
inference(paramod,[status(thm)],[c_1380,c_1]) ).
cnf(c_2188,plain,
s1(b) = p0(b,d),
inference(copy,[status(thm)],[c_5303]) ).
cnf(c_5304,plain,
ifeq(q2(b,A,b),p0(b,d),ifeq(p0(b,d),p0(b,d),s2(A),p0(b,d)),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_2188,c_1525]) ).
cnf(c_2191,plain,
ifeq(q2(b,A,b),p0(b,d),s2(A),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5304]) ).
cnf(c_2198,plain,
ifeq(p0(b,d),p0(b,A),s1(B),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_2188,c_2120]) ).
cnf(c_5305,plain,
p0(b,d) = s1(A),
inference(paramod,[status(thm)],[c_2198,c_1]) ).
cnf(c_2257,plain,
s1(A) = p0(b,d),
inference(copy,[status(thm)],[c_5305]) ).
cnf(c_5306,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(A,A),p0(b,d),l2(B,B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2257,c_1001]) ).
cnf(c_2326,plain,
ifeq(p0(A,A),p0(b,d),l2(B,B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5306]) ).
cnf(c_2497,plain,
ifeq(p0(b,A),p0(b,d),n1(a,B,a),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_832]) ).
cnf(c_5307,plain,
ifeq(n1(a,A,a),p0(b,d),ifeq(p0(b,d),p0(b,d),n1(a,A,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_741,c_840]) ).
cnf(c_2575,plain,
ifeq(n1(a,A,a),p0(b,d),n1(a,A,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5307]) ).
cnf(c_5308,plain,
ifeq(p0(b,d),p0(b,d),n1(A,A,B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_39,c_853]) ).
cnf(c_2608,plain,
n1(A,A,B) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5308]) ).
cnf(c_5309,plain,
ifeq(p0(b,d),p0(b,d),ifeq(k1(B),p0(b,d),q2(A,A,A),p0(b,C)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2608,c_1492]) ).
cnf(c_2617,plain,
ifeq(k1(A),p0(b,d),q2(B,B,B),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5309]) ).
cnf(c_5310,plain,
ifeq(p0(b,d),p0(b,d),ifeq(l0(A),p0(b,d),p1(B,B,B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2608,c_886]) ).
cnf(c_2680,plain,
ifeq(l0(A),p0(b,d),p1(B,B,B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5310]) ).
cnf(c_2686,plain,
ifeq(q2(b,A,b),p0(b,B),s2(A),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_2191]) ).
cnf(c_2726,plain,
ifeq(p0(b,A),p0(b,d),l2(B,B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_2326]) ).
cnf(c_5311,plain,
ifeq(p0(b,d),p0(b,d),q2(A,A,A),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_726,c_2617]) ).
cnf(c_2848,plain,
q2(A,A,A) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5311]) ).
cnf(c_5312,plain,
ifeq(p0(b,d),p0(b,d),p1(A,A,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_41,c_2680]) ).
cnf(c_2884,plain,
p1(A,A,A) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5312]) ).
cnf(c_5313,plain,
ifeq(p0(b,d),p0(b,d),q2(A,b,b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2884,c_1028]) ).
cnf(c_2888,plain,
q2(A,b,b) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5313]) ).
cnf(c_5314,plain,
p0(b,d) = l2(A,A),
inference(paramod,[status(thm)],[c_2726,c_1]) ).
cnf(c_2935,plain,
l2(A,A) = p0(b,d),
inference(copy,[status(thm)],[c_5314]) ).
cnf(c_5315,plain,
ifeq(p0(b,d),p0(b,d),p3(A,A,A),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_2935,c_1693]) ).
cnf(c_2952,plain,
p3(A,A,A) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5315]) ).
cnf(c_5316,plain,
ifeq(s2(A),p0(b,d),ifeq(p0(b,d),p0(b,d),s3(A,B),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2848,c_1079]) ).
cnf(c_3270,plain,
ifeq(s2(A),p0(b,d),s3(A,B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5316]) ).
cnf(c_3272,plain,
ifeq(s2(A),p0(b,B),s3(A,C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_3270]) ).
cnf(c_3275,plain,
ifeq(s2(A),p0(b,B),s3(A,C),p0(b,D)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_3272]) ).
cnf(c_5317,plain,
p0(b,d) = n1(a,A,a),
inference(paramod,[status(thm)],[c_2497,c_1]) ).
cnf(c_3369,plain,
n1(a,A,a) = p0(b,d),
inference(copy,[status(thm)],[c_5317]) ).
cnf(c_5318,plain,
ifeq(p0(b,d),p0(b,d),n1(a,A,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_3369,c_2575]) ).
cnf(c_3370,plain,
n1(a,A,A) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5318]) ).
cnf(c_5319,plain,
ifeq(q2(a,A,A),p0(b,B),ifeq(p1(A,A,A),p0(b,d),ifeq(p0(b,d),p0(b,d),q2(A,a,A),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_3370,c_1502]) ).
cnf(c_5320,plain,
ifeq(q2(a,A,A),p0(b,B),ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),q2(A,a,A),p0(b,d)),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2884,c_5319]) ).
cnf(c_5321,plain,
ifeq(q2(a,A,A),p0(b,B),ifeq(p0(b,d),p0(b,d),q2(A,a,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5320]) ).
cnf(c_3829,plain,
ifeq(q2(a,A,A),p0(b,B),q2(A,a,A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5321]) ).
cnf(c_5322,plain,
ifeq(s3(a,A),p0(b,B),ifeq(p0(b,d),p0(b,d),m4(A,C),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2935,c_1820]) ).
cnf(c_4090,plain,
ifeq(s3(a,A),p0(b,B),m4(A,C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5322]) ).
cnf(c_4091,plain,
ifeq(s3(a,A),p0(b,B),m4(A,C),p0(b,D)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_4090]) ).
cnf(c_5323,plain,
ifeq(p3(A,B,C),p0(b,D),ifeq(p0(b,d),p0(b,d),s4(d),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2039,c_1893]) ).
cnf(c_4129,plain,
ifeq(p3(A,B,C),p0(b,D),s4(d),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5323]) ).
cnf(c_4169,plain,
ifeq(s4(A),p0(b,B),ifeq(m4(e,e),p0(b,d),m5(A,A),p0(b,d)),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_1911]) ).
cnf(c_4198,plain,
ifeq(p0(b,d),p0(b,A),s4(d),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2952,c_4129]) ).
cnf(c_5324,plain,
p0(b,d) = s4(d),
inference(paramod,[status(thm)],[c_4198,c_1]) ).
cnf(c_4202,plain,
s4(d) = p0(b,d),
inference(copy,[status(thm)],[c_5324]) ).
cnf(c_4909,plain,
ifeq(p0(b,d),p0(b,A),q2(b,a,b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_2888,c_3829]) ).
cnf(c_5325,plain,
p0(b,d) = q2(b,a,b),
inference(paramod,[status(thm)],[c_4909,c_1]) ).
cnf(c_4916,plain,
q2(b,a,b) = p0(b,d),
inference(copy,[status(thm)],[c_5325]) ).
cnf(c_4917,plain,
ifeq(p0(b,d),p0(b,A),s2(a),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_4916,c_2686]) ).
cnf(c_5326,plain,
p0(b,d) = s2(a),
inference(paramod,[status(thm)],[c_4917,c_1]) ).
cnf(c_4919,plain,
s2(a) = p0(b,d),
inference(copy,[status(thm)],[c_5326]) ).
cnf(c_4920,plain,
ifeq(p0(b,d),p0(b,A),s3(a,B),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_4919,c_3275]) ).
cnf(c_5327,plain,
p0(b,d) = s3(a,A),
inference(paramod,[status(thm)],[c_4920,c_1]) ).
cnf(c_4944,plain,
s3(a,A) = p0(b,d),
inference(copy,[status(thm)],[c_5327]) ).
cnf(c_4945,plain,
ifeq(p0(b,d),p0(b,A),m4(B,C),p0(b,D)) = p0(b,d),
inference(paramod,[status(thm)],[c_4944,c_4091]) ).
cnf(c_5328,plain,
p0(b,d) = m4(A,B),
inference(paramod,[status(thm)],[c_4945,c_1]) ).
cnf(c_4951,plain,
m4(A,B) = p0(b,d),
inference(copy,[status(thm)],[c_5328]) ).
cnf(c_5329,plain,
ifeq(s4(A),p0(b,B),ifeq(p0(b,d),p0(b,d),m5(A,A),p0(b,d)),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_4951,c_4169]) ).
cnf(c_4959,plain,
ifeq(s4(A),p0(b,B),m5(A,A),p0(b,C)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_5329]) ).
cnf(c_4962,plain,
ifeq(p0(b,d),p0(b,A),m5(d,d),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_4202,c_4959]) ).
cnf(c_5330,plain,
p0(b,d) = m5(d,d),
inference(paramod,[status(thm)],[c_4962,c_1]) ).
cnf(c_4968,plain,
m5(d,d) = p0(b,d),
inference(copy,[status(thm)],[c_5330]) ).
cnf(c_4969,plain,
$false,
inference(resolve,[status(thm)],[c_4968,c_2011]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN143-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n026.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 26 17:18:25 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 1541386 was started by sandbox2 on n026,
% 0.08/0.35 % Sat Sep 26 17:18:25 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 34.14/4.76
% 34.14/4.76 % given #500 (T,wt=17): 868 ifeq(l0(A),p0(b,d),p1(A,A,A),p0(b,d)) = p0(b,d). [para(39(a,1),198(a,1,3,1)),rewrite([1(15)])].
% 34.14/4.76
% 34.14/4.76 % given #1000 (T,wt=18): 2579 ifeq(l1(a,b),p0(b,d),n1(b,a,a),p0(b,d)) = p0(b,d). [para(2382(a,1),840(a,1,1)),rewrite([1(24)])].
% 34.14/4.76
% 34.14/4.76 % given #1500 (T,wt=8): 4456 p5(A,A,c) = p0(b,d). [para(4177(a,1),1(a,1)),flip(a)].
% 34.14/4.76
% 34.14/4.76 % SZS status Unsatisfiable for theBenchmark
% 34.14/4.76
% 34.14/4.76 % Proof 1 at 3.95 (+ 0.39) seconds.
% 34.14/4.76 % Length of proof is 134.
% 34.14/4.76 % Level of proof is 23.
% 34.14/4.76 % Maximum clause weight is 41.000.
% 34.14/4.76 % Given clauses 1814.
% 34.14/4.76
% 34.14/4.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------