%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV537-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:08:14 AM UTC 2026
% Result : Unsatisfiable 2.23s 0.77s
% Output : CNFRefutation 2.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 120
% Number of leaves : 27
% Syntax : Number of formulae : 371 ( 124 unt; 0 def)
% Number of atoms : 941 ( 940 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 614 ( 44 ~; 570 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 29 con; 0-3 aty)
% Number of variables : 38 ( 2 sgn 7 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(a1,axiom,
! [VAR_0,VAR_1,VAR_2] : select(store(VAR_0,VAR_1,VAR_2),VAR_1) = VAR_2,
file('theBenchmark.p',a1) ).
cnf(c_1,plain,
select(store(A,B,C),B) = C,
inference(clausify,[status(thm)],[a1]) ).
fof(a2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( select(store(VAR_2,VAR_0,VAR_3),VAR_1) = select(VAR_2,VAR_1)
| VAR_0 = VAR_1 ),
file('theBenchmark.p',a2) ).
cnf(c_2,plain,
( select(store(C,A,D),B) = select(C,B)
| A = B ),
inference(clausify,[status(thm)],[a2]) ).
fof(hyp2,axiom,
a_469 = store(a_467,i0,e_468),
file('theBenchmark.p',hyp2) ).
cnf(c_7,plain,
a_469 = store(a_467,i0,e_468),
inference(clausify,[status(thm)],[hyp2]) ).
cnf(c_8,plain,
store(a_467,i0,e_468) = a_469,
inference(copy,[status(thm)],[c_7]) ).
fof(hyp3,axiom,
a_471 = store(a_469,i3,e_470),
file('theBenchmark.p',hyp3) ).
cnf(c_9,plain,
a_471 = store(a_469,i3,e_470),
inference(clausify,[status(thm)],[hyp3]) ).
cnf(c_10,plain,
store(a_469,i3,e_470) = a_471,
inference(copy,[status(thm)],[c_9]) ).
fof(hyp4,axiom,
a_473 = store(a_471,i3,e_472),
file('theBenchmark.p',hyp4) ).
cnf(c_11,plain,
a_473 = store(a_471,i3,e_472),
inference(clausify,[status(thm)],[hyp4]) ).
cnf(c_12,plain,
store(a_471,i3,e_472) = a_473,
inference(copy,[status(thm)],[c_11]) ).
fof(hyp5,axiom,
a_475 = store(a_473,i2,e_474),
file('theBenchmark.p',hyp5) ).
cnf(c_13,plain,
a_475 = store(a_473,i2,e_474),
inference(clausify,[status(thm)],[hyp5]) ).
cnf(c_14,plain,
store(a_473,i2,e_474) = a_475,
inference(copy,[status(thm)],[c_13]) ).
fof(hyp6,axiom,
a_477 = store(a_475,i2,e_476),
file('theBenchmark.p',hyp6) ).
cnf(c_15,plain,
a_477 = store(a_475,i2,e_476),
inference(clausify,[status(thm)],[hyp6]) ).
cnf(c_16,plain,
store(a_475,i2,e_476) = a_477,
inference(copy,[status(thm)],[c_15]) ).
fof(hyp7,axiom,
a_479 = store(a_477,i0,e_478),
file('theBenchmark.p',hyp7) ).
cnf(c_17,plain,
a_479 = store(a_477,i0,e_478),
inference(clausify,[status(thm)],[hyp7]) ).
cnf(c_18,plain,
store(a_477,i0,e_478) = a_479,
inference(copy,[status(thm)],[c_17]) ).
fof(hyp8,axiom,
a_480 = store(a_467,i3,e_470),
file('theBenchmark.p',hyp8) ).
cnf(c_19,plain,
a_480 = store(a_467,i3,e_470),
inference(clausify,[status(thm)],[hyp8]) ).
cnf(c_20,plain,
store(a_467,i3,e_470) = a_480,
inference(copy,[status(thm)],[c_19]) ).
fof(hyp9,axiom,
a_481 = store(a_480,i0,e_468),
file('theBenchmark.p',hyp9) ).
cnf(c_21,plain,
a_481 = store(a_480,i0,e_468),
inference(clausify,[status(thm)],[hyp9]) ).
cnf(c_22,plain,
store(a_480,i0,e_468) = a_481,
inference(copy,[status(thm)],[c_21]) ).
fof(hyp10,axiom,
a_483 = store(a_481,i3,e_482),
file('theBenchmark.p',hyp10) ).
cnf(c_23,plain,
a_483 = store(a_481,i3,e_482),
inference(clausify,[status(thm)],[hyp10]) ).
cnf(c_24,plain,
store(a_481,i3,e_482) = a_483,
inference(copy,[status(thm)],[c_23]) ).
fof(hyp11,axiom,
a_485 = store(a_483,i2,e_484),
file('theBenchmark.p',hyp11) ).
cnf(c_25,plain,
a_485 = store(a_483,i2,e_484),
inference(clausify,[status(thm)],[hyp11]) ).
cnf(c_26,plain,
store(a_483,i2,e_484) = a_485,
inference(copy,[status(thm)],[c_25]) ).
fof(hyp12,axiom,
a_487 = store(a_485,i0,e_486),
file('theBenchmark.p',hyp12) ).
cnf(c_27,plain,
a_487 = store(a_485,i0,e_486),
inference(clausify,[status(thm)],[hyp12]) ).
cnf(c_28,plain,
store(a_485,i0,e_486) = a_487,
inference(copy,[status(thm)],[c_27]) ).
fof(hyp13,axiom,
a_489 = store(a_487,i2,e_488),
file('theBenchmark.p',hyp13) ).
cnf(c_29,plain,
a_489 = store(a_487,i2,e_488),
inference(clausify,[status(thm)],[hyp13]) ).
cnf(c_30,plain,
store(a_487,i2,e_488) = a_489,
inference(copy,[status(thm)],[c_29]) ).
fof(hyp15,axiom,
e_468 = select(a_467,i3),
file('theBenchmark.p',hyp15) ).
cnf(c_33,plain,
e_468 = select(a_467,i3),
inference(clausify,[status(thm)],[hyp15]) ).
cnf(c_34,plain,
select(a_467,i3) = e_468,
inference(copy,[status(thm)],[c_33]) ).
fof(hyp16,axiom,
e_470 = select(a_467,i0),
file('theBenchmark.p',hyp16) ).
cnf(c_35,plain,
e_470 = select(a_467,i0),
inference(clausify,[status(thm)],[hyp16]) ).
cnf(c_36,plain,
select(a_467,i0) = e_470,
inference(copy,[status(thm)],[c_35]) ).
fof(hyp17,axiom,
e_472 = select(a_471,i2),
file('theBenchmark.p',hyp17) ).
cnf(c_37,plain,
e_472 = select(a_471,i2),
inference(clausify,[status(thm)],[hyp17]) ).
cnf(c_38,plain,
select(a_471,i2) = e_472,
inference(copy,[status(thm)],[c_37]) ).
fof(hyp18,axiom,
e_474 = select(a_471,i3),
file('theBenchmark.p',hyp18) ).
cnf(c_39,plain,
e_474 = select(a_471,i3),
inference(clausify,[status(thm)],[hyp18]) ).
cnf(c_40,plain,
select(a_471,i3) = e_474,
inference(copy,[status(thm)],[c_39]) ).
fof(hyp19,axiom,
e_476 = select(a_475,i0),
file('theBenchmark.p',hyp19) ).
cnf(c_41,plain,
e_476 = select(a_475,i0),
inference(clausify,[status(thm)],[hyp19]) ).
cnf(c_42,plain,
select(a_475,i0) = e_476,
inference(copy,[status(thm)],[c_41]) ).
fof(hyp20,axiom,
e_478 = select(a_475,i2),
file('theBenchmark.p',hyp20) ).
cnf(c_43,plain,
e_478 = select(a_475,i2),
inference(clausify,[status(thm)],[hyp20]) ).
cnf(c_44,plain,
select(a_475,i2) = e_478,
inference(copy,[status(thm)],[c_43]) ).
fof(hyp21,axiom,
e_482 = select(a_481,i2),
file('theBenchmark.p',hyp21) ).
cnf(c_45,plain,
e_482 = select(a_481,i2),
inference(clausify,[status(thm)],[hyp21]) ).
cnf(c_46,plain,
select(a_481,i2) = e_482,
inference(copy,[status(thm)],[c_45]) ).
fof(hyp22,axiom,
e_484 = select(a_481,i3),
file('theBenchmark.p',hyp22) ).
cnf(c_47,plain,
e_484 = select(a_481,i3),
inference(clausify,[status(thm)],[hyp22]) ).
cnf(c_48,plain,
select(a_481,i3) = e_484,
inference(copy,[status(thm)],[c_47]) ).
fof(hyp23,axiom,
e_486 = select(a_485,i2),
file('theBenchmark.p',hyp23) ).
cnf(c_49,plain,
e_486 = select(a_485,i2),
inference(clausify,[status(thm)],[hyp23]) ).
cnf(c_50,plain,
select(a_485,i2) = e_486,
inference(copy,[status(thm)],[c_49]) ).
fof(hyp24,axiom,
e_488 = select(a_485,i0),
file('theBenchmark.p',hyp24) ).
cnf(c_51,plain,
e_488 = select(a_485,i0),
inference(clausify,[status(thm)],[hyp24]) ).
cnf(c_52,plain,
select(a_485,i0) = e_488,
inference(copy,[status(thm)],[c_51]) ).
fof(hyp25,axiom,
e_491 = select(a_479,i_490),
file('theBenchmark.p',hyp25) ).
cnf(c_53,plain,
e_491 = select(a_479,i_490),
inference(clausify,[status(thm)],[hyp25]) ).
cnf(c_54,plain,
select(a_479,i_490) = e_491,
inference(copy,[status(thm)],[c_53]) ).
fof(hyp26,axiom,
e_492 = select(a_489,i_490),
file('theBenchmark.p',hyp26) ).
cnf(c_55,plain,
e_492 = select(a_489,i_490),
inference(clausify,[status(thm)],[hyp26]) ).
cnf(c_56,plain,
select(a_489,i_490) = e_492,
inference(copy,[status(thm)],[c_55]) ).
fof(goal,axiom,
e_491 != e_492,
file('theBenchmark.p',goal) ).
cnf(c_59,plain,
e_491 != e_492,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_60,plain,
e_492 != e_491,
inference(copy,[status(thm)],[c_59]) ).
cnf(c_68,plain,
select(a_469,i0) = e_468,
inference(paramod,[status(thm)],[c_8,c_1]) ).
cnf(c_69,plain,
( select(a_469,A) = select(a_467,A)
| i0 = A ),
inference(paramod,[status(thm)],[c_8,c_2]) ).
cnf(c_70,plain,
select(a_471,i3) = e_470,
inference(paramod,[status(thm)],[c_10,c_1]) ).
cnf(c_1333,plain,
( select(a_471,A) = select(a_469,A)
| i3 = A ),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_71,plain,
( select(a_469,A) = select(a_471,A)
| i3 = A ),
inference(copy,[status(thm)],[c_1333]) ).
cnf(c_72,plain,
select(a_473,i3) = e_472,
inference(paramod,[status(thm)],[c_12,c_1]) ).
cnf(c_73,plain,
( select(a_473,A) = select(a_471,A)
| i3 = A ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_74,plain,
select(a_475,i2) = e_474,
inference(paramod,[status(thm)],[c_14,c_1]) ).
cnf(c_1334,plain,
( select(a_475,A) = select(a_473,A)
| i2 = A ),
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_75,plain,
( select(a_473,A) = select(a_475,A)
| i2 = A ),
inference(copy,[status(thm)],[c_1334]) ).
cnf(c_76,plain,
select(a_477,i2) = e_476,
inference(paramod,[status(thm)],[c_16,c_1]) ).
cnf(c_77,plain,
( select(a_477,A) = select(a_475,A)
| i2 = A ),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_78,plain,
select(a_479,i0) = e_478,
inference(paramod,[status(thm)],[c_18,c_1]) ).
cnf(c_1335,plain,
( select(a_479,A) = select(a_477,A)
| i0 = A ),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_79,plain,
( select(a_477,A) = select(a_479,A)
| i0 = A ),
inference(copy,[status(thm)],[c_1335]) ).
cnf(c_80,plain,
select(a_480,i3) = e_470,
inference(paramod,[status(thm)],[c_20,c_1]) ).
cnf(c_81,plain,
( select(a_480,A) = select(a_467,A)
| i3 = A ),
inference(paramod,[status(thm)],[c_20,c_2]) ).
cnf(c_82,plain,
select(a_481,i0) = e_468,
inference(paramod,[status(thm)],[c_22,c_1]) ).
cnf(c_1336,plain,
( select(a_481,A) = select(a_480,A)
| i0 = A ),
inference(paramod,[status(thm)],[c_22,c_2]) ).
cnf(c_83,plain,
( select(a_480,A) = select(a_481,A)
| i0 = A ),
inference(copy,[status(thm)],[c_1336]) ).
cnf(c_84,plain,
select(a_483,i3) = e_482,
inference(paramod,[status(thm)],[c_24,c_1]) ).
cnf(c_85,plain,
( select(a_483,A) = select(a_481,A)
| i3 = A ),
inference(paramod,[status(thm)],[c_24,c_2]) ).
cnf(c_86,plain,
select(a_485,i2) = e_484,
inference(paramod,[status(thm)],[c_26,c_1]) ).
cnf(c_1337,plain,
( select(a_485,A) = select(a_483,A)
| i2 = A ),
inference(paramod,[status(thm)],[c_26,c_2]) ).
cnf(c_87,plain,
( select(a_483,A) = select(a_485,A)
| i2 = A ),
inference(copy,[status(thm)],[c_1337]) ).
cnf(c_88,plain,
select(a_487,i0) = e_486,
inference(paramod,[status(thm)],[c_28,c_1]) ).
cnf(c_89,plain,
( select(a_487,A) = select(a_485,A)
| i0 = A ),
inference(paramod,[status(thm)],[c_28,c_2]) ).
cnf(c_90,plain,
select(a_489,i2) = e_488,
inference(paramod,[status(thm)],[c_30,c_1]) ).
cnf(c_1338,plain,
( select(a_489,A) = select(a_487,A)
| i2 = A ),
inference(paramod,[status(thm)],[c_30,c_2]) ).
cnf(c_91,plain,
( select(a_487,A) = select(a_489,A)
| i2 = A ),
inference(copy,[status(thm)],[c_1338]) ).
cnf(c_1339,plain,
e_470 = e_474,
inference(paramod,[status(thm)],[c_70,c_40]) ).
cnf(c_109,plain,
e_474 = e_470,
inference(copy,[status(thm)],[c_1339]) ).
cnf(c_1340,plain,
e_474 = e_478,
inference(paramod,[status(thm)],[c_74,c_44]) ).
cnf(c_113,plain,
e_478 = e_474,
inference(copy,[status(thm)],[c_1340]) ).
cnf(c_116,plain,
e_478 = e_470,
inference(paramod,[status(thm)],[c_109,c_113]) ).
cnf(c_121,plain,
select(a_479,i0) = e_470,
inference(paramod,[status(thm)],[c_116,c_78]) ).
cnf(c_1341,plain,
e_484 = e_486,
inference(paramod,[status(thm)],[c_86,c_50]) ).
cnf(c_126,plain,
e_486 = e_484,
inference(copy,[status(thm)],[c_1341]) ).
cnf(c_129,plain,
select(a_487,i0) = e_484,
inference(paramod,[status(thm)],[c_126,c_88]) ).
cnf(c_157,plain,
( select(a_469,i2) = e_472
| i3 = i2 ),
inference(paramod,[status(thm)],[c_38,c_71]) ).
cnf(c_158,plain,
( select(a_471,i0) = e_468
| i3 = i0 ),
inference(paramod,[status(thm)],[c_71,c_68]) ).
cnf(c_159,plain,
( select(a_471,A) = select(a_467,A)
| i0 = A
| i3 = A ),
inference(paramod,[status(thm)],[c_71,c_69]) ).
cnf(c_1342,plain,
( e_472 = select(a_467,i2)
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_157,c_69]) ).
cnf(c_163,plain,
( select(a_467,i2) = e_472
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1342]) ).
cnf(c_1343,plain,
( select(a_473,i0) = e_468
| i3 = i0
| i3 = i0 ),
inference(paramod,[status(thm)],[c_158,c_73]) ).
cnf(c_167,plain,
( select(a_473,i0) = e_468
| i3 = i0 ),
inference(copy,[status(thm)],[c_1343]) ).
cnf(c_1344,plain,
( select(a_473,i0) = e_476
| i2 = i0 ),
inference(paramod,[status(thm)],[c_42,c_75]) ).
cnf(c_172,plain,
( select(a_473,i0) = e_476
| i0 = i2 ),
inference(copy,[status(thm)],[c_1344]) ).
cnf(c_1345,plain,
( select(a_475,i3) = e_472
| i2 = i3 ),
inference(paramod,[status(thm)],[c_75,c_72]) ).
cnf(c_173,plain,
( select(a_475,i3) = e_472
| i3 = i2 ),
inference(copy,[status(thm)],[c_1345]) ).
cnf(c_179,plain,
( e_476 = e_468
| i3 = i0
| i0 = i2 ),
inference(paramod,[status(thm)],[c_172,c_167]) ).
cnf(c_1346,plain,
( select(a_477,i3) = e_472
| i2 = i3
| i3 = i2 ),
inference(paramod,[status(thm)],[c_173,c_77]) ).
cnf(c_1347,plain,
( select(a_477,i3) = e_472
| i3 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1346]) ).
cnf(c_187,plain,
( select(a_477,i3) = e_472
| i3 = i2 ),
inference(copy,[status(thm)],[c_1347]) ).
cnf(c_1348,plain,
( select(a_477,i_490) = e_491
| i0 = i_490 ),
inference(paramod,[status(thm)],[c_54,c_79]) ).
cnf(c_195,plain,
( select(a_477,i_490) = e_491
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1348]) ).
cnf(c_196,plain,
( select(a_479,i2) = e_476
| i0 = i2 ),
inference(paramod,[status(thm)],[c_79,c_76]) ).
cnf(c_1349,plain,
( e_491 = select(a_475,i_490)
| i2 = i_490
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_195,c_77]) ).
cnf(c_1350,plain,
( e_491 = select(a_475,i_490)
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1349]) ).
cnf(c_201,plain,
( select(a_475,i_490) = e_491
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1350]) ).
cnf(c_1351,plain,
( select(a_479,i2) = e_468
| i0 = i2
| i3 = i0
| i0 = i2 ),
inference(paramod,[status(thm)],[c_179,c_196]) ).
cnf(c_204,plain,
( select(a_479,i2) = e_468
| i3 = i0
| i0 = i2 ),
inference(copy,[status(thm)],[c_1351]) ).
cnf(c_213,plain,
( select(a_480,i2) = e_482
| i0 = i2 ),
inference(paramod,[status(thm)],[c_46,c_83]) ).
cnf(c_1352,plain,
( select(a_480,i3) = e_484
| i0 = i3 ),
inference(paramod,[status(thm)],[c_48,c_83]) ).
cnf(c_214,plain,
( select(a_480,i3) = e_484
| i3 = i0 ),
inference(copy,[status(thm)],[c_1352]) ).
cnf(c_216,plain,
( select(a_481,A) = select(a_467,A)
| i3 = A
| i0 = A ),
inference(paramod,[status(thm)],[c_83,c_81]) ).
cnf(c_1353,plain,
( e_482 = select(a_467,i2)
| i3 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_213,c_81]) ).
cnf(c_220,plain,
( select(a_467,i2) = e_482
| i3 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1353]) ).
cnf(c_222,plain,
( e_484 = e_470
| i3 = i0 ),
inference(paramod,[status(thm)],[c_214,c_80]) ).
cnf(c_225,plain,
( select(a_485,i2) = e_470
| i3 = i0 ),
inference(paramod,[status(thm)],[c_222,c_86]) ).
cnf(c_226,plain,
( e_486 = e_470
| i3 = i0 ),
inference(paramod,[status(thm)],[c_222,c_126]) ).
cnf(c_235,plain,
( select(a_483,i0) = e_468
| i3 = i0 ),
inference(paramod,[status(thm)],[c_82,c_85]) ).
cnf(c_1354,plain,
( select(a_483,i0) = e_488
| i2 = i0 ),
inference(paramod,[status(thm)],[c_52,c_87]) ).
cnf(c_240,plain,
( select(a_483,i0) = e_488
| i0 = i2 ),
inference(copy,[status(thm)],[c_1354]) ).
cnf(c_1355,plain,
( select(a_485,i3) = e_482
| i2 = i3 ),
inference(paramod,[status(thm)],[c_87,c_84]) ).
cnf(c_241,plain,
( select(a_485,i3) = e_482
| i3 = i2 ),
inference(copy,[status(thm)],[c_1355]) ).
cnf(c_247,plain,
( e_488 = e_468
| i3 = i0
| i0 = i2 ),
inference(paramod,[status(thm)],[c_240,c_235]) ).
cnf(c_250,plain,
( select(a_489,i2) = e_468
| i3 = i0
| i0 = i2 ),
inference(paramod,[status(thm)],[c_247,c_90]) ).
cnf(c_1356,plain,
( select(a_487,i_490) = e_492
| i2 = i_490 ),
inference(paramod,[status(thm)],[c_56,c_91]) ).
cnf(c_262,plain,
( select(a_487,i_490) = e_492
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1356]) ).
cnf(c_1357,plain,
( select(a_489,i0) = e_486
| i2 = i0 ),
inference(paramod,[status(thm)],[c_91,c_88]) ).
cnf(c_263,plain,
( select(a_489,i0) = e_486
| i0 = i2 ),
inference(copy,[status(thm)],[c_1357]) ).
cnf(c_1358,plain,
( select(a_489,i0) = e_484
| i2 = i0 ),
inference(paramod,[status(thm)],[c_91,c_129]) ).
cnf(c_264,plain,
( select(a_489,i0) = e_484
| i0 = i2 ),
inference(copy,[status(thm)],[c_1358]) ).
cnf(c_1359,plain,
( e_492 = select(a_485,i_490)
| i0 = i_490
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_262,c_89]) ).
cnf(c_1360,plain,
( e_492 = select(a_485,i_490)
| i_490 = i0
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1359]) ).
cnf(c_269,plain,
( select(a_485,i_490) = e_492
| i_490 = i0
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1360]) ).
cnf(c_1361,plain,
( select(a_473,i_490) = e_491
| i2 = i_490
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_201,c_75]) ).
cnf(c_1362,plain,
( select(a_473,i_490) = e_491
| i_490 = i2
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1361]) ).
cnf(c_297,plain,
( select(a_473,i_490) = e_491
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1362]) ).
cnf(c_1363,plain,
( e_482 = e_472
| i0 = i2
| i3 = i2
| i3 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_220,c_163]) ).
cnf(c_1364,plain,
( e_482 = e_472
| i0 = i2
| i3 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1363]) ).
cnf(c_309,plain,
( e_482 = e_472
| i3 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1364]) ).
cnf(c_1365,plain,
( select(a_483,i_490) = e_492
| i2 = i_490
| i_490 = i0
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_269,c_87]) ).
cnf(c_1366,plain,
( select(a_483,i_490) = e_492
| i_490 = i2
| i_490 = i0
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1365]) ).
cnf(c_329,plain,
( select(a_483,i_490) = e_492
| i_490 = i0
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1366]) ).
cnf(c_1367,plain,
( select(a_473,A) = select(a_467,A)
| i3 = A
| i0 = A
| i3 = A ),
inference(paramod,[status(thm)],[c_159,c_73]) ).
cnf(c_367,plain,
( select(a_473,A) = select(a_467,A)
| i0 = A
| i3 = A ),
inference(copy,[status(thm)],[c_1367]) ).
cnf(c_1368,plain,
( select(a_483,A) = select(a_467,A)
| i3 = A
| i3 = A
| i0 = A ),
inference(paramod,[status(thm)],[c_216,c_85]) ).
cnf(c_380,plain,
( select(a_483,A) = select(a_467,A)
| i3 = A
| i0 = A ),
inference(copy,[status(thm)],[c_1368]) ).
cnf(c_1369,plain,
( select(a_467,i_490) = e_491
| i_490 = i2
| i_490 = i0
| i0 = i_490
| i3 = i_490 ),
inference(paramod,[status(thm)],[c_367,c_297]) ).
cnf(c_1370,plain,
( select(a_467,i_490) = e_491
| i_490 = i2
| i_490 = i0
| i0 = i_490
| i_490 = i3 ),
inference(copy,[status(thm)],[c_1369]) ).
cnf(c_1371,plain,
( select(a_467,i_490) = e_491
| i_490 = i2
| i_490 = i0
| i_490 = i0
| i_490 = i3 ),
inference(copy,[status(thm)],[c_1370]) ).
cnf(c_393,plain,
( select(a_467,i_490) = e_491
| i_490 = i2
| i_490 = i0
| i_490 = i3 ),
inference(copy,[status(thm)],[c_1371]) ).
cnf(c_1372,plain,
( select(a_467,i_490) = e_492
| i_490 = i0
| i_490 = i2
| i3 = i_490
| i0 = i_490 ),
inference(paramod,[status(thm)],[c_380,c_329]) ).
cnf(c_1373,plain,
( select(a_467,i_490) = e_492
| i_490 = i0
| i_490 = i2
| i3 = i_490
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1372]) ).
cnf(c_1374,plain,
( select(a_467,i_490) = e_492
| i_490 = i0
| i_490 = i2
| i_490 = i3
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1373]) ).
cnf(c_402,plain,
( select(a_467,i_490) = e_492
| i_490 = i2
| i_490 = i3
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1374]) ).
cnf(c_1375,plain,
( e_492 = e_491
| i_490 = i2
| i_490 = i0
| i_490 = i3
| i_490 = i2
| i_490 = i3
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_402,c_393]) ).
cnf(c_1376,plain,
( e_492 = e_491
| i_490 = i2
| i_490 = i0
| i_490 = i2
| i_490 = i3
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1375]) ).
cnf(c_1377,plain,
( e_492 = e_491
| i_490 = i2
| i_490 = i2
| i_490 = i3
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1376]) ).
cnf(c_1378,plain,
( e_492 = e_491
| i_490 = i2
| i_490 = i3
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1377]) ).
cnf(c_455,plain,
( i_490 = i2
| i_490 = i3
| i_490 = i0 ),
inference(resolve,[status(thm)],[c_60,c_1378]) ).
cnf(c_1379,plain,
( select(a_477,i3) = e_491
| i_490 = i0
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_455,c_195]) ).
cnf(c_459,plain,
( select(a_477,i3) = e_491
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1379]) ).
cnf(c_1380,plain,
( select(a_485,i3) = e_492
| i_490 = i0
| i_490 = i2
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_455,c_269]) ).
cnf(c_1381,plain,
( select(a_485,i3) = e_492
| i_490 = i0
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1380]) ).
cnf(c_462,plain,
( select(a_485,i3) = e_492
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1381]) ).
cnf(c_1382,plain,
( select(a_473,i3) = e_491
| i_490 = i2
| i_490 = i0
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_455,c_297]) ).
cnf(c_1383,plain,
( select(a_473,i3) = e_491
| i_490 = i2
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1382]) ).
cnf(c_463,plain,
( select(a_473,i3) = e_491
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1383]) ).
cnf(c_1384,plain,
( select(a_483,i3) = e_492
| i_490 = i0
| i_490 = i2
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_455,c_329]) ).
cnf(c_1385,plain,
( select(a_483,i3) = e_492
| i_490 = i0
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1384]) ).
cnf(c_464,plain,
( select(a_483,i3) = e_492
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1385]) ).
cnf(c_488,plain,
( e_491 = e_472
| i3 = i2
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_459,c_187]) ).
cnf(c_490,plain,
( e_492 != e_472
| i3 = i2
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_488,c_60]) ).
cnf(c_498,plain,
( e_492 = e_482
| i3 = i2
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_462,c_241]) ).
cnf(c_1386,plain,
( e_482 != e_472
| i3 = i2
| i_490 = i2
| i_490 = i0
| i3 = i2
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_498,c_490]) ).
cnf(c_1387,plain,
( e_482 != e_472
| i3 = i2
| i_490 = i2
| i3 = i2
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1386]) ).
cnf(c_1388,plain,
( e_482 != e_472
| i3 = i2
| i3 = i2
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1387]) ).
cnf(c_506,plain,
( e_482 != e_472
| i3 = i2
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1388]) ).
cnf(c_1389,plain,
( i3 = i2
| i0 = i2
| i3 = i2
| i_490 = i2
| i_490 = i0 ),
inference(resolve,[status(thm)],[c_506,c_309]) ).
cnf(c_509,plain,
( i0 = i2
| i3 = i2
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1389]) ).
cnf(c_510,plain,
( select(a_479,i0) = e_491
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_509,c_54]) ).
cnf(c_511,plain,
( select(a_489,i0) = e_492
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_509,c_56]) ).
cnf(c_515,plain,
( e_491 = e_472
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_463,c_72]) ).
cnf(c_517,plain,
( e_492 != e_472
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_515,c_60]) ).
cnf(c_525,plain,
( e_492 = e_482
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_464,c_84]) ).
cnf(c_1390,plain,
( e_482 != e_472
| i_490 = i2
| i_490 = i0
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_525,c_517]) ).
cnf(c_1391,plain,
( e_482 != e_472
| i_490 = i2
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1390]) ).
cnf(c_534,plain,
( e_482 != e_472
| i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1391]) ).
cnf(c_578,plain,
( e_491 = e_478
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_510,c_78]) ).
cnf(c_580,plain,
( e_491 = e_470
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_510,c_121]) ).
cnf(c_583,plain,
( e_492 != e_478
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_578,c_60]) ).
cnf(c_587,plain,
( e_492 != e_470
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_580,c_60]) ).
cnf(c_1392,plain,
( e_492 = e_486
| i0 = i2
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_511,c_263]) ).
cnf(c_589,plain,
( e_492 = e_486
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1392]) ).
cnf(c_1393,plain,
( e_492 = e_484
| i0 = i2
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_511,c_264]) ).
cnf(c_590,plain,
( e_492 = e_484
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1393]) ).
cnf(c_1394,plain,
( e_486 != e_478
| i0 = i2
| i3 = i2
| i_490 = i2
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_589,c_583]) ).
cnf(c_1395,plain,
( e_486 != e_478
| i0 = i2
| i3 = i2
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1394]) ).
cnf(c_1396,plain,
( e_486 != e_478
| i0 = i2
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1395]) ).
cnf(c_596,plain,
( e_486 != e_478
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1396]) ).
cnf(c_1397,plain,
( e_484 != e_470
| i0 = i2
| i3 = i2
| i_490 = i2
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_590,c_587]) ).
cnf(c_1398,plain,
( e_484 != e_470
| i0 = i2
| i3 = i2
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1397]) ).
cnf(c_1399,plain,
( e_484 != e_470
| i0 = i2
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1398]) ).
cnf(c_604,plain,
( e_484 != e_470
| i0 = i2
| i3 = i2
| i_490 = i2 ),
inference(copy,[status(thm)],[c_1399]) ).
cnf(c_1400,plain,
( e_470 != e_478
| i0 = i2
| i3 = i2
| i_490 = i2
| i3 = i0 ),
inference(paramod,[status(thm)],[c_226,c_596]) ).
cnf(c_1401,plain,
( e_478 != e_470
| i0 = i2
| i3 = i2
| i_490 = i2
| i3 = i0 ),
inference(copy,[status(thm)],[c_1400]) ).
cnf(c_606,plain,
( i0 = i2
| i3 = i2
| i_490 = i2
| i3 = i0 ),
inference(resolve,[status(thm)],[c_116,c_1401]) ).
cnf(c_607,plain,
( select(a_479,i2) = e_491
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(paramod,[status(thm)],[c_606,c_54]) ).
cnf(c_608,plain,
( select(a_489,i2) = e_492
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(paramod,[status(thm)],[c_606,c_56]) ).
cnf(c_1402,plain,
( e_491 = e_468
| i3 = i0
| i0 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(paramod,[status(thm)],[c_607,c_204]) ).
cnf(c_1403,plain,
( e_491 = e_468
| i3 = i0
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(copy,[status(thm)],[c_1402]) ).
cnf(c_630,plain,
( e_491 = e_468
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(copy,[status(thm)],[c_1403]) ).
cnf(c_635,plain,
( e_492 != e_468
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(paramod,[status(thm)],[c_630,c_60]) ).
cnf(c_1404,plain,
( e_492 = e_468
| i3 = i0
| i0 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(paramod,[status(thm)],[c_608,c_250]) ).
cnf(c_1405,plain,
( e_492 = e_468
| i3 = i0
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(copy,[status(thm)],[c_1404]) ).
cnf(c_639,plain,
( e_492 = e_468
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(copy,[status(thm)],[c_1405]) ).
cnf(c_1406,plain,
( i0 = i2
| i3 = i2
| i3 = i0
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(resolve,[status(thm)],[c_639,c_635]) ).
cnf(c_1407,plain,
( i0 = i2
| i3 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(copy,[status(thm)],[c_1406]) ).
cnf(c_1408,plain,
( i0 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(copy,[status(thm)],[c_1407]) ).
cnf(c_644,plain,
( i0 = i2
| i3 = i2
| i3 = i0 ),
inference(copy,[status(thm)],[c_1408]) ).
cnf(c_649,plain,
( select(a_467,i0) = e_468
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_644,c_34]) ).
cnf(c_651,plain,
( select(a_481,i0) = e_484
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_644,c_48]) ).
cnf(c_653,plain,
( select(a_473,i0) = e_472
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_644,c_72]) ).
cnf(c_655,plain,
( select(a_483,i0) = e_482
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_644,c_84]) ).
cnf(c_1409,plain,
( e_468 = e_470
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_649,c_36]) ).
cnf(c_665,plain,
( e_470 = e_468
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1409]) ).
cnf(c_1410,plain,
( e_484 != e_468
| i0 = i2
| i3 = i2
| i_490 = i2
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_665,c_604]) ).
cnf(c_1411,plain,
( e_484 != e_468
| i0 = i2
| i_490 = i2
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1410]) ).
cnf(c_682,plain,
( e_484 != e_468
| i_490 = i2
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1411]) ).
cnf(c_688,plain,
( e_484 = e_468
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_651,c_82]) ).
cnf(c_1412,plain,
( i_490 = i2
| i0 = i2
| i3 = i2
| i0 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_688,c_682]) ).
cnf(c_1413,plain,
( i_490 = i2
| i0 = i2
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1412]) ).
cnf(c_690,plain,
( i_490 = i2
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1413]) ).
cnf(c_699,plain,
( select(a_479,i2) = e_491
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_690,c_54]) ).
cnf(c_700,plain,
( select(a_489,i2) = e_492
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_690,c_56]) ).
cnf(c_1414,plain,
( e_472 = e_476
| i0 = i2
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_653,c_172]) ).
cnf(c_1415,plain,
( e_476 = e_472
| i0 = i2
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1414]) ).
cnf(c_706,plain,
( e_476 = e_472
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1415]) ).
cnf(c_1416,plain,
( e_482 = e_488
| i0 = i2
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_655,c_240]) ).
cnf(c_1417,plain,
( e_488 = e_482
| i0 = i2
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1416]) ).
cnf(c_715,plain,
( e_488 = e_482
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1417]) ).
cnf(c_1418,plain,
( e_488 = e_472
| i0 = i2
| i3 = i2
| i3 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_309,c_715]) ).
cnf(c_1419,plain,
( e_488 = e_472
| i0 = i2
| i3 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1418]) ).
cnf(c_719,plain,
( e_488 = e_472
| i3 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1419]) ).
cnf(c_1420,plain,
( e_491 = e_476
| i0 = i2
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_699,c_196]) ).
cnf(c_751,plain,
( e_491 = e_476
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1420]) ).
cnf(c_753,plain,
( e_492 != e_476
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_751,c_60]) ).
cnf(c_1421,plain,
( e_492 != e_472
| i0 = i2
| i3 = i2
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_706,c_753]) ).
cnf(c_1422,plain,
( e_492 != e_472
| i0 = i2
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1421]) ).
cnf(c_756,plain,
( e_492 != e_472
| i0 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1422]) ).
cnf(c_760,plain,
( e_492 = e_488
| i0 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_700,c_90]) ).
cnf(c_1423,plain,
( e_492 = e_472
| i0 = i2
| i3 = i2
| i3 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_719,c_760]) ).
cnf(c_1424,plain,
( e_492 = e_472
| i0 = i2
| i3 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1423]) ).
cnf(c_764,plain,
( e_492 = e_472
| i3 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1424]) ).
cnf(c_1425,plain,
( i0 = i2
| i3 = i2
| i3 = i2
| i0 = i2 ),
inference(resolve,[status(thm)],[c_764,c_756]) ).
cnf(c_1426,plain,
( i0 = i2
| i3 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1425]) ).
cnf(c_772,plain,
( i3 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1426]) ).
cnf(c_779,plain,
( select(a_481,i2) = e_484
| i0 = i2 ),
inference(paramod,[status(thm)],[c_772,c_48]) ).
cnf(c_782,plain,
( select(a_480,i2) = e_470
| i0 = i2 ),
inference(paramod,[status(thm)],[c_772,c_80]) ).
cnf(c_1427,plain,
( i_490 = i2
| i_490 = i2
| i_490 = i0
| i0 = i2 ),
inference(paramod,[status(thm)],[c_772,c_455]) ).
cnf(c_789,plain,
( i_490 = i2
| i_490 = i0
| i0 = i2 ),
inference(copy,[status(thm)],[c_1427]) ).
cnf(c_790,plain,
( select(a_479,i0) = e_491
| i_490 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_789,c_54]) ).
cnf(c_791,plain,
( select(a_489,i0) = e_492
| i_490 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_789,c_56]) ).
cnf(c_810,plain,
( e_484 = e_482
| i0 = i2 ),
inference(paramod,[status(thm)],[c_779,c_46]) ).
cnf(c_1428,plain,
( e_470 = e_482
| i0 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_782,c_213]) ).
cnf(c_1429,plain,
( e_482 = e_470
| i0 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1428]) ).
cnf(c_829,plain,
( e_482 = e_470
| i0 = i2 ),
inference(copy,[status(thm)],[c_1429]) ).
cnf(c_1430,plain,
( e_484 = e_470
| i0 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_829,c_810]) ).
cnf(c_832,plain,
( e_484 = e_470
| i0 = i2 ),
inference(copy,[status(thm)],[c_1430]) ).
cnf(c_1431,plain,
( select(a_489,i0) = e_470
| i0 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_832,c_264]) ).
cnf(c_840,plain,
( select(a_489,i0) = e_470
| i0 = i2 ),
inference(copy,[status(thm)],[c_1431]) ).
cnf(c_879,plain,
( e_491 = e_470
| i_490 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_790,c_121]) ).
cnf(c_887,plain,
( e_492 != e_470
| i_490 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_879,c_60]) ).
cnf(c_1432,plain,
( e_492 = e_470
| i0 = i2
| i_490 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_791,c_840]) ).
cnf(c_894,plain,
( e_492 = e_470
| i_490 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1432]) ).
cnf(c_1433,plain,
( i_490 = i2
| i0 = i2
| i_490 = i2
| i0 = i2 ),
inference(resolve,[status(thm)],[c_894,c_887]) ).
cnf(c_1434,plain,
( i_490 = i2
| i_490 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1433]) ).
cnf(c_917,plain,
( i_490 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1434]) ).
cnf(c_918,plain,
( select(a_479,i2) = e_491
| i0 = i2 ),
inference(paramod,[status(thm)],[c_917,c_54]) ).
cnf(c_919,plain,
( select(a_489,i2) = e_492
| i0 = i2 ),
inference(paramod,[status(thm)],[c_917,c_56]) ).
cnf(c_1435,plain,
( e_491 = e_476
| i0 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_918,c_196]) ).
cnf(c_924,plain,
( e_491 = e_476
| i0 = i2 ),
inference(copy,[status(thm)],[c_1435]) ).
cnf(c_927,plain,
( e_492 != e_476
| i0 = i2 ),
inference(paramod,[status(thm)],[c_924,c_60]) ).
cnf(c_1436,plain,
( e_492 != e_468
| i0 = i2
| i3 = i0
| i0 = i2 ),
inference(paramod,[status(thm)],[c_179,c_927]) ).
cnf(c_929,plain,
( e_492 != e_468
| i3 = i0
| i0 = i2 ),
inference(copy,[status(thm)],[c_1436]) ).
cnf(c_1437,plain,
( e_492 = e_468
| i3 = i0
| i0 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_919,c_250]) ).
cnf(c_934,plain,
( e_492 = e_468
| i3 = i0
| i0 = i2 ),
inference(copy,[status(thm)],[c_1437]) ).
cnf(c_1438,plain,
( i3 = i0
| i0 = i2
| i3 = i0
| i0 = i2 ),
inference(resolve,[status(thm)],[c_934,c_929]) ).
cnf(c_1439,plain,
( i3 = i0
| i3 = i0
| i0 = i2 ),
inference(copy,[status(thm)],[c_1438]) ).
cnf(c_941,plain,
( i3 = i0
| i0 = i2 ),
inference(copy,[status(thm)],[c_1439]) ).
cnf(c_1440,plain,
( i0 = i2
| i0 = i2
| i0 = i2 ),
inference(paramod,[status(thm)],[c_941,c_772]) ).
cnf(c_1441,plain,
( i0 = i2
| i0 = i2 ),
inference(copy,[status(thm)],[c_1440]) ).
cnf(c_955,plain,
i0 = i2,
inference(copy,[status(thm)],[c_1441]) ).
cnf(c_960,plain,
select(a_467,i2) = e_470,
inference(paramod,[status(thm)],[c_955,c_36]) ).
cnf(c_962,plain,
select(a_485,i2) = e_488,
inference(paramod,[status(thm)],[c_955,c_52]) ).
cnf(c_963,plain,
select(a_469,i2) = e_468,
inference(paramod,[status(thm)],[c_955,c_68]) ).
cnf(c_964,plain,
select(a_479,i2) = e_478,
inference(paramod,[status(thm)],[c_955,c_78]) ).
cnf(c_965,plain,
select(a_481,i2) = e_468,
inference(paramod,[status(thm)],[c_955,c_82]) ).
cnf(c_999,plain,
e_488 = e_484,
inference(paramod,[status(thm)],[c_962,c_86]) ).
cnf(c_1000,plain,
( e_488 = e_470
| i3 = i0 ),
inference(paramod,[status(thm)],[c_962,c_225]) ).
cnf(c_1442,plain,
( e_468 = e_472
| i3 = i2 ),
inference(paramod,[status(thm)],[c_963,c_157]) ).
cnf(c_1012,plain,
( e_472 = e_468
| i3 = i2 ),
inference(copy,[status(thm)],[c_1442]) ).
cnf(c_1021,plain,
( e_482 != e_468
| i_490 = i2
| i_490 = i0
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1012,c_534]) ).
cnf(c_1443,plain,
e_468 = e_482,
inference(paramod,[status(thm)],[c_965,c_46]) ).
cnf(c_1030,plain,
e_482 = e_468,
inference(copy,[status(thm)],[c_1443]) ).
cnf(c_1032,plain,
( i_490 = i2
| i_490 = i0
| i3 = i2 ),
inference(resolve,[status(thm)],[c_1030,c_1021]) ).
cnf(c_1444,plain,
( i_490 = i2
| i_490 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_955,c_1032]) ).
cnf(c_1052,plain,
( i_490 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_1444]) ).
cnf(c_1053,plain,
( select(a_479,i2) = e_491
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1052,c_54]) ).
cnf(c_1054,plain,
( select(a_489,i2) = e_492
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1052,c_56]) ).
cnf(c_1114,plain,
( e_491 = e_478
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1053,c_964]) ).
cnf(c_1119,plain,
( e_492 != e_478
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1114,c_60]) ).
cnf(c_1131,plain,
( e_492 = e_488
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1054,c_90]) ).
cnf(c_1445,plain,
( e_488 != e_478
| i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1131,c_1119]) ).
cnf(c_1137,plain,
( e_488 != e_478
| i3 = i2 ),
inference(copy,[status(thm)],[c_1445]) ).
cnf(c_1446,plain,
( e_470 != e_478
| i3 = i2
| i3 = i0 ),
inference(paramod,[status(thm)],[c_1000,c_1137]) ).
cnf(c_1447,plain,
( e_478 != e_470
| i3 = i2
| i3 = i0 ),
inference(copy,[status(thm)],[c_1446]) ).
cnf(c_1154,plain,
( i3 = i2
| i3 = i0 ),
inference(resolve,[status(thm)],[c_116,c_1447]) ).
cnf(c_1448,plain,
( i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_955,c_1154]) ).
cnf(c_1171,plain,
i3 = i2,
inference(copy,[status(thm)],[c_1448]) ).
cnf(c_1176,plain,
select(a_467,i2) = e_468,
inference(paramod,[status(thm)],[c_1171,c_34]) ).
cnf(c_1178,plain,
select(a_481,i2) = e_484,
inference(paramod,[status(thm)],[c_1171,c_48]) ).
cnf(c_1449,plain,
( i_490 = i2
| i_490 = i2
| i_490 = i0 ),
inference(paramod,[status(thm)],[c_1171,c_455]) ).
cnf(c_1187,plain,
( i_490 = i2
| i_490 = i0 ),
inference(copy,[status(thm)],[c_1449]) ).
cnf(c_1450,plain,
( i_490 = i2
| i_490 = i2 ),
inference(paramod,[status(thm)],[c_955,c_1187]) ).
cnf(c_1194,plain,
i_490 = i2,
inference(copy,[status(thm)],[c_1450]) ).
cnf(c_1195,plain,
select(a_479,i2) = e_491,
inference(paramod,[status(thm)],[c_1194,c_54]) ).
cnf(c_1196,plain,
select(a_489,i2) = e_492,
inference(paramod,[status(thm)],[c_1194,c_56]) ).
cnf(c_1451,plain,
e_468 = e_470,
inference(paramod,[status(thm)],[c_1176,c_960]) ).
cnf(c_1202,plain,
e_470 = e_468,
inference(copy,[status(thm)],[c_1451]) ).
cnf(c_1208,plain,
e_478 = e_468,
inference(paramod,[status(thm)],[c_1202,c_116]) ).
cnf(c_1261,plain,
e_484 = e_468,
inference(paramod,[status(thm)],[c_1178,c_965]) ).
cnf(c_1282,plain,
e_488 = e_468,
inference(paramod,[status(thm)],[c_1261,c_999]) ).
cnf(c_1300,plain,
e_491 = e_478,
inference(paramod,[status(thm)],[c_1195,c_964]) ).
cnf(c_1305,plain,
e_492 != e_478,
inference(paramod,[status(thm)],[c_1300,c_60]) ).
cnf(c_1318,plain,
e_492 != e_468,
inference(paramod,[status(thm)],[c_1208,c_1305]) ).
cnf(c_1325,plain,
e_492 = e_488,
inference(paramod,[status(thm)],[c_1196,c_90]) ).
cnf(c_1452,plain,
e_492 = e_468,
inference(paramod,[status(thm)],[c_1282,c_1325]) ).
cnf(c_1332,plain,
$false,
inference(resolve,[status(thm)],[c_1318,c_1452]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV537-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n002.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 14:21:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 1937264 was started by sandbox2 on n002,
% 0.09/0.37 % Sat Sep 26 14:21:20 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 2.23/0.77
% 2.23/0.77 % given #500 (T,wt=15): 1179 select(a_471,i2) = e_470. [para(1171(a,1),70(a,1,2))].
% 2.23/0.77
% 2.23/0.77 % SZS status Unsatisfiable for theBenchmark
% 2.23/0.77
% 2.23/0.77 % Proof 1 at 0.31 (+ 0.07) seconds.
% 2.23/0.77 % Length of proof is 224.
% 2.23/0.77 % Level of proof is 60.
% 2.23/0.77 % Maximum clause weight is 28.000.
% 2.23/0.77 % Given clauses 518.
% 2.23/0.77
% 2.23/0.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------