%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV565-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Thu Sep 24 02:49:05 PM UTC 2026
% Result : Unsatisfiable 17.34s 2.67s
% Output : CNFRefutation 17.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 23
% Syntax : Number of formulae : 211 ( 81 unt; 0 def)
% Number of atoms : 510 ( 509 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 311 ( 12 ~; 299 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 25 con; 0-3 aty)
% Number of variables : 46 ( 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,I,J] : store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,hypothesis,
a_20 = store(a1,i1,e_19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,hypothesis,
a_22 = store(a2,i1,e_21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
a_24 = store(a_20,i2,e_23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
a_26 = store(a_22,i2,e_25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
a_28 = store(a_24,i3,e_27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
a_30 = store(a_26,i3,e_29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
a_32 = store(a_28,i4,e_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
a_34 = store(a_30,i4,e_33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
e_19 = select(a2,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
e_21 = select(a1,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
e_23 = select(a_22,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
e_25 = select(a_20,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
e_27 = select(a_26,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
e_29 = select(a_24,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
e_31 = select(a_30,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
e_33 = select(a_28,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
e_36 = select(a1,i_35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
e_37 = select(a2,i_35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
a_32 = a_34,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
e_36 != e_37,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f26,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f27,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f28,plain,
! [X0,X1,X2] : store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)) = store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f29,plain,
a_20 = store(a1,i1,e_19),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f30,plain,
a_22 = store(a2,i1,e_21),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f31,plain,
a_24 = store(a_20,i2,e_23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f32,plain,
a_26 = store(a_22,i2,e_25),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f33,plain,
a_28 = store(a_24,i3,e_27),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f34,plain,
a_30 = store(a_26,i3,e_29),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f35,plain,
a_32 = store(a_28,i4,e_31),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f36,plain,
a_34 = store(a_30,i4,e_33),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f37,plain,
e_19 = select(a2,i1),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f38,plain,
e_21 = select(a1,i1),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f39,plain,
e_23 = select(a_22,i2),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f40,plain,
e_25 = select(a_20,i2),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f41,plain,
e_27 = select(a_26,i3),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f42,plain,
e_29 = select(a_24,i3),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f43,plain,
e_31 = select(a_30,i4),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f44,plain,
e_33 = select(a_28,i4),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f45,plain,
e_36 = select(a1,i_35),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f46,plain,
e_37 = select(a2,i_35),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f48,plain,
a_32 = a_34,
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f49,plain,
e_36 != e_37,
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f50,plain,
select(a_20,i1) = e_19,
inference(paramodulation,[status(thm)],[f29,f25]) ).
fof(f51,plain,
select(a_22,i1) = e_21,
inference(paramodulation,[status(thm)],[f30,f25]) ).
fof(f52,plain,
select(a_24,i2) = e_23,
inference(paramodulation,[status(thm)],[f31,f25]) ).
fof(f54,plain,
! [X0] :
( select(a_24,X0) = select(a_20,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f31,f27]) ).
fof(f55,plain,
! [X0] :
( select(a_22,X0) = select(a2,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f30,f27]) ).
fof(f56,plain,
! [X0] :
( select(a_20,X0) = select(a1,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f29,f27]) ).
fof(f71,plain,
! [X0] : store(store(a2,X0,e_37),i_35,select(a2,X0)) = store(store(a2,i_35,select(a2,X0)),X0,select(a2,i_35)),
inference(paramodulation,[status(thm)],[f46,f28]) ).
fof(f73,plain,
! [X0] : store(store(a1,X0,e_36),i_35,select(a1,X0)) = store(store(a1,i_35,select(a1,X0)),X0,select(a1,i_35)),
inference(paramodulation,[status(thm)],[f45,f28]) ).
fof(f132,plain,
! [X0] : store(store(a2,X0,e_37),i_35,select(a2,X0)) = store(store(a2,i_35,select(a2,X0)),X0,e_37),
inference(forward_demodulation,[status(thm)],[f46,f71]) ).
fof(f134,plain,
! [X0] : store(store(a1,X0,e_36),i_35,select(a1,X0)) = store(store(a1,i_35,select(a1,X0)),X0,e_36),
inference(forward_demodulation,[status(thm)],[f45,f73]) ).
fof(f182,plain,
! [X0] :
( select(a_26,X0) = select(a_22,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f32,f27]) ).
fof(f183,plain,
select(a_26,i2) = e_25,
inference(paramodulation,[status(thm)],[f32,f25]) ).
fof(f192,plain,
! [X0] :
( select(a_28,X0) = select(a_24,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f33,f27]) ).
fof(f193,plain,
select(a_28,i3) = e_27,
inference(paramodulation,[status(thm)],[f33,f25]) ).
fof(f202,plain,
! [X0] :
( select(a_30,X0) = select(a_26,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f34,f27]) ).
fof(f203,plain,
select(a_30,i3) = e_29,
inference(paramodulation,[status(thm)],[f34,f25]) ).
fof(f212,plain,
! [X0] :
( select(a_32,X0) = select(a_28,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f35,f27]) ).
fof(f213,plain,
select(a_32,i4) = e_31,
inference(paramodulation,[status(thm)],[f35,f25]) ).
fof(f222,plain,
a_32 = store(a_30,i4,e_33),
inference(forward_demodulation,[status(thm)],[f48,f36]) ).
fof(f223,plain,
! [X0] :
( select(a_32,X0) = select(a_30,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f222,f27]) ).
fof(f224,plain,
select(a_32,i4) = e_33,
inference(paramodulation,[status(thm)],[f222,f25]) ).
fof(f225,plain,
e_31 = e_33,
inference(forward_demodulation,[status(thm)],[f213,f224]) ).
fof(f227,plain,
e_31 = select(a_28,i4),
inference(backward_demodulation,[status(thm)],[f225,f44]) ).
fof(f239,plain,
( e_29 = select(a_20,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f42,f54]) ).
fof(f251,plain,
( select(a_22,i_35) = e_37
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f46,f55]) ).
fof(f263,plain,
( select(a_20,i_35) = e_36
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f45,f56]) ).
fof(f313,plain,
! [X0] : select(store(store(a2,X0,e_37),i_35,select(a2,X0)),X0) = e_37,
inference(paramodulation,[status(thm)],[f132,f25]) ).
fof(f318,plain,
select(store(store(a2,i1,e_37),i_35,e_19),i1) = e_37,
inference(paramodulation,[status(thm)],[f37,f313]) ).
fof(f348,plain,
! [X0] : select(store(store(a1,i_35,select(a1,X0)),X0,e_36),i_35) = select(a1,X0),
inference(paramodulation,[status(thm)],[f134,f25]) ).
fof(f476,plain,
( e_27 = select(a_22,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f41,f182]) ).
fof(f488,plain,
( e_31 = select(a_24,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f227,f192]) ).
fof(f498,plain,
( i2 = i4
| e_31 = select(a_20,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f54,f488]) ).
fof(f505,plain,
( e_31 = select(a_26,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f43,f202]) ).
fof(f514,plain,
( i2 = i4
| e_31 = select(a_22,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f182,f505]) ).
fof(f527,plain,
! [X0] :
( i4 = X0
| select(a_28,X0) = select(a_30,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f212,f223]) ).
fof(f534,plain,
! [X0] :
( select(a_28,X0) = select(a_30,X0)
| i4 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f527]) ).
fof(f536,plain,
( select(a_28,i3) = e_29
| i4 = i3 ),
inference(paramodulation,[status(thm)],[f203,f534]) ).
fof(f538,plain,
! [X0] :
( i3 = X0
| select(a_28,X0) = select(a_26,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f202,f534]) ).
fof(f548,plain,
( e_27 = e_29
| i4 = i3 ),
inference(forward_demodulation,[status(thm)],[f193,f536]) ).
fof(f557,plain,
( e_27 = e_29
| e_31 = select(a_28,i3) ),
inference(paramodulation,[status(thm)],[f548,f227]) ).
fof(f560,plain,
( e_27 = e_29
| e_31 = select(a_30,i3) ),
inference(paramodulation,[status(thm)],[f548,f43]) ).
fof(f563,plain,
( e_27 = e_29
| e_31 = e_27 ),
inference(forward_demodulation,[status(thm)],[f193,f557]) ).
fof(f564,plain,
( e_27 = e_29
| e_31 = e_29 ),
inference(forward_demodulation,[status(thm)],[f203,f560]) ).
fof(f571,plain,
( e_27 = e_29
| e_27 = e_29
| e_27 = e_29 ),
inference(paramodulation,[status(thm)],[f563,f564]) ).
fof(f579,plain,
e_27 = e_29,
inference(duplicate_literals_removal,[status(thm)],[f571]) ).
fof(f584,plain,
( e_27 = select(a_20,i3)
| i2 = i3 ),
inference(backward_demodulation,[status(thm)],[f579,f239]) ).
fof(f587,plain,
e_27 = select(a_24,i3),
inference(backward_demodulation,[status(thm)],[f579,f42]) ).
fof(f1056,plain,
! [X0] :
( i3 = X0
| i3 = X0
| select(a_24,X0) = select(a_26,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f192,f538]) ).
fof(f1066,plain,
! [X0] :
( i3 = X0
| select(a_24,X0) = select(a_26,X0)
| i4 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f1056]) ).
fof(f1069,plain,
( i3 = i2
| select(a_24,i2) = e_25
| i4 = i2 ),
inference(paramodulation,[status(thm)],[f183,f1066]) ).
fof(f1071,plain,
! [X0] :
( i2 = X0
| i3 = X0
| select(a_24,X0) = select(a_22,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f182,f1066]) ).
fof(f1082,plain,
( i3 = i2
| e_23 = e_25
| i4 = i2 ),
inference(forward_demodulation,[status(thm)],[f52,f1069]) ).
fof(f1090,plain,
( i3 = i2
| e_23 = e_25
| e_31 = select(a_26,i2)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f1082,f505]) ).
fof(f1091,plain,
( i3 = i2
| e_23 = e_25
| e_31 = select(a_24,i2)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f1082,f488]) ).
fof(f1103,plain,
( i3 = i2
| e_23 = e_25
| e_31 = e_25
| i3 = i4 ),
inference(forward_demodulation,[status(thm)],[f183,f1090]) ).
fof(f1104,plain,
( i3 = i2
| e_23 = e_25
| e_31 = e_23
| i3 = i4 ),
inference(forward_demodulation,[status(thm)],[f52,f1091]) ).
fof(f1115,plain,
( i3 = i2
| e_23 = e_25
| i3 = i4
| i3 = i2
| e_23 = e_25
| e_25 = e_23
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f1103,f1104]) ).
fof(f1125,plain,
( i3 = i2
| e_25 = e_23
| i3 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f1115]) ).
fof(f1129,plain,
( i3 = i2
| e_23 = e_25
| i3 = i2
| e_25 = e_23
| i3 = i2 ),
inference(paramodulation,[status(thm)],[f1082,f1125]) ).
fof(f1148,plain,
( e_25 = e_23
| i3 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1129]) ).
fof(f1168,plain,
( e_25 = e_23
| e_27 = select(a_24,i2) ),
inference(paramodulation,[status(thm)],[f1148,f587]) ).
fof(f1173,plain,
( e_25 = e_23
| e_27 = select(a_26,i2) ),
inference(paramodulation,[status(thm)],[f1148,f41]) ).
fof(f1175,plain,
( e_25 = e_23
| e_27 = e_23 ),
inference(forward_demodulation,[status(thm)],[f52,f1168]) ).
fof(f1177,plain,
( e_25 = e_23
| e_27 = e_25 ),
inference(forward_demodulation,[status(thm)],[f183,f1173]) ).
fof(f1188,plain,
( e_25 = e_23
| e_25 = e_23
| e_23 = e_25 ),
inference(paramodulation,[status(thm)],[f1175,f1177]) ).
fof(f1200,plain,
e_23 = e_25,
inference(duplicate_literals_removal,[status(thm)],[f1188]) ).
fof(f1212,plain,
e_23 = select(a_20,i2),
inference(backward_demodulation,[status(thm)],[f1200,f40]) ).
fof(f2868,plain,
! [X0] :
( i2 = X0
| i2 = X0
| i3 = X0
| select(a_20,X0) = select(a_22,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f54,f1071]) ).
fof(f2879,plain,
! [X0] :
( i2 = X0
| i3 = X0
| select(a_20,X0) = select(a_22,X0)
| i4 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f2868]) ).
fof(f2883,plain,
( i1 = i_35
| i2 = i_35
| i3 = i_35
| select(a_20,i_35) = e_37
| i4 = i_35 ),
inference(paramodulation,[status(thm)],[f251,f2879]) ).
fof(f2884,plain,
( i2 = i1
| i3 = i1
| select(a_20,i1) = e_21
| i4 = i1 ),
inference(paramodulation,[status(thm)],[f51,f2879]) ).
fof(f2906,plain,
( i2 = i1
| i3 = i1
| e_19 = e_21
| i4 = i1 ),
inference(forward_demodulation,[status(thm)],[f50,f2884]) ).
fof(f2921,plain,
( i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = select(a_28,i1) ),
inference(paramodulation,[status(thm)],[f2906,f227]) ).
fof(f2924,plain,
( i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = select(a_30,i1) ),
inference(paramodulation,[status(thm)],[f2906,f43]) ).
fof(f2928,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = select(a_24,i1) ),
inference(paramodulation,[status(thm)],[f192,f2921]) ).
fof(f2937,plain,
( i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = select(a_24,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2928]) ).
fof(f2950,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = select(a_26,i1) ),
inference(paramodulation,[status(thm)],[f202,f2924]) ).
fof(f2958,plain,
( i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = select(a_26,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2950]) ).
fof(f2962,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = select(a_20,i1) ),
inference(paramodulation,[status(thm)],[f54,f2937]) ).
fof(f2972,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = e_19 ),
inference(forward_demodulation,[status(thm)],[f50,f2962]) ).
fof(f2973,plain,
( i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = e_19 ),
inference(duplicate_literals_removal,[status(thm)],[f2972]) ).
fof(f2987,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = select(a_22,i1) ),
inference(paramodulation,[status(thm)],[f182,f2958]) ).
fof(f2996,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = e_21 ),
inference(forward_demodulation,[status(thm)],[f51,f2987]) ).
fof(f2997,plain,
( i2 = i1
| i3 = i1
| e_19 = e_21
| e_31 = e_21 ),
inference(duplicate_literals_removal,[status(thm)],[f2996]) ).
fof(f3001,plain,
( i2 = i1
| i3 = i1
| e_19 = e_21
| i2 = i1
| i3 = i1
| e_19 = e_21
| e_19 = e_21 ),
inference(paramodulation,[status(thm)],[f2973,f2997]) ).
fof(f3011,plain,
( i2 = i1
| i3 = i1
| e_19 = e_21 ),
inference(duplicate_literals_removal,[status(thm)],[f3001]) ).
fof(f3029,plain,
( i2 = i1
| e_19 = e_21
| e_27 = select(a_24,i1) ),
inference(paramodulation,[status(thm)],[f3011,f587]) ).
fof(f3031,plain,
( i2 = i1
| e_19 = e_21
| e_27 = select(a_22,i1)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f3011,f476]) ).
fof(f3038,plain,
( i2 = i1
| e_19 = e_21
| e_27 = e_21
| i2 = i3 ),
inference(forward_demodulation,[status(thm)],[f51,f3031]) ).
fof(f3072,plain,
( i1 = i_35
| i1 = i_35
| i2 = i_35
| i3 = i_35
| e_36 = e_37
| i4 = i_35 ),
inference(paramodulation,[status(thm)],[f263,f2883]) ).
fof(f3086,plain,
( i1 = i_35
| i2 = i_35
| i3 = i_35
| e_36 = e_37
| i4 = i_35 ),
inference(duplicate_literals_removal,[status(thm)],[f3072]) ).
fof(f3087,plain,
( i1 = i_35
| i2 = i_35
| i3 = i_35
| i4 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f3086,f49]) ).
fof(f3195,plain,
( i1 = i_35
| i2 = i_35
| i3 = i_35
| select(a_20,i4) = e_36
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f3087,f263]) ).
fof(f3196,plain,
( i1 = i_35
| i2 = i_35
| i3 = i_35
| select(a_22,i4) = e_37
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f3087,f251]) ).
fof(f3199,plain,
( i_35 = i3
| i4 != i3
| i1 = i_35
| i2 = i_35 ),
inference(equality_factoring,[status(thm)],[f3087]) ).
fof(f3200,plain,
( i_35 = i2
| i4 != i2
| i1 = i_35
| i3 = i_35 ),
inference(equality_factoring,[status(thm)],[f3087]) ).
fof(f3204,plain,
( i2 = i_35
| i3 = i_35
| select(a_20,i4) = e_36
| i1 = i_35 ),
inference(duplicate_literals_removal,[status(thm)],[f3195]) ).
fof(f3205,plain,
( i2 = i_35
| i3 = i_35
| select(a_22,i4) = e_37
| i1 = i_35 ),
inference(duplicate_literals_removal,[status(thm)],[f3196]) ).
fof(f3513,plain,
( i2 = i1
| i2 = i1
| e_19 = e_21
| e_27 = select(a_20,i1) ),
inference(paramodulation,[status(thm)],[f54,f3029]) ).
fof(f3523,plain,
( i2 = i1
| i2 = i1
| e_19 = e_21
| e_27 = e_19 ),
inference(forward_demodulation,[status(thm)],[f50,f3513]) ).
fof(f3524,plain,
( i2 = i1
| e_19 = e_21
| e_27 = e_19 ),
inference(duplicate_literals_removal,[status(thm)],[f3523]) ).
fof(f3542,plain,
( i2 = i1
| e_19 = e_21
| i2 = i1
| e_19 = e_21
| e_19 = e_21
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f3524,f3038]) ).
fof(f3556,plain,
( i2 = i1
| e_19 = e_21
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f3542]) ).
fof(f3564,plain,
( i2 = i1
| e_19 = e_21
| i2 = i1
| e_19 = e_21
| i2 = i1 ),
inference(paramodulation,[status(thm)],[f3011,f3556]) ).
fof(f3588,plain,
( e_19 = e_21
| i2 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f3564]) ).
fof(f3606,plain,
( e_19 = e_21
| e_23 = select(a_20,i1) ),
inference(paramodulation,[status(thm)],[f3588,f1212]) ).
fof(f3615,plain,
( e_19 = e_21
| e_23 = select(a_22,i1) ),
inference(paramodulation,[status(thm)],[f3588,f39]) ).
fof(f3618,plain,
( e_19 = e_21
| e_23 = e_19 ),
inference(forward_demodulation,[status(thm)],[f50,f3606]) ).
fof(f3619,plain,
( e_19 = e_21
| e_23 = e_21 ),
inference(forward_demodulation,[status(thm)],[f51,f3615]) ).
fof(f3636,plain,
( e_19 = e_21
| e_19 = e_21
| e_19 = e_21 ),
inference(paramodulation,[status(thm)],[f3618,f3619]) ).
fof(f3654,plain,
e_19 = e_21,
inference(duplicate_literals_removal,[status(thm)],[f3636]) ).
fof(f3666,plain,
e_19 = select(a1,i1),
inference(backward_demodulation,[status(thm)],[f3654,f38]) ).
fof(f3710,plain,
select(store(store(a1,i_35,e_19),i1,e_36),i_35) = select(a1,i1),
inference(paramodulation,[status(thm)],[f3666,f348]) ).
fof(f3788,plain,
select(store(store(a1,i_35,e_19),i1,e_36),i_35) = e_19,
inference(forward_demodulation,[status(thm)],[f3666,f3710]) ).
fof(f4252,plain,
( i2 = i4
| i3 = i4
| i2 = i_35
| i3 = i_35
| e_31 = e_36
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f498,f3204]) ).
fof(f4266,plain,
( i2 = i4
| i2 = i_35
| i3 = i_35
| e_31 = e_36
| i1 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f4252,f3199]) ).
fof(f4275,plain,
( i2 = i4
| i3 = i4
| i2 = i_35
| i3 = i_35
| e_31 = e_37
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f514,f3205]) ).
fof(f4291,plain,
( i2 = i4
| i2 = i_35
| i3 = i_35
| e_31 = e_37
| i1 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f4275,f3199]) ).
fof(f4362,plain,
( i2 = i_35
| i3 = i_35
| e_31 = e_36
| i1 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f4266,f3200]) ).
fof(f4646,plain,
( i2 = i_35
| i3 = i_35
| e_31 = e_37
| i1 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f4291,f3200]) ).
fof(f4685,plain,
( i2 = i_35
| i3 = i_35
| i1 = i_35
| e_36 != e_31 ),
inference(paramodulation,[status(thm)],[f4646,f49]) ).
fof(f4687,plain,
( i2 = i_35
| i3 = i_35
| i1 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f4685,f4362]) ).
fof(f4803,plain,
( i2 = i_35
| i1 = i_35
| select(a_20,i3) = e_36
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f4687,f263]) ).
fof(f4804,plain,
( i2 = i_35
| i1 = i_35
| select(a_22,i3) = e_37
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f4687,f251]) ).
fof(f4808,plain,
( i_35 = i2
| i3 != i2
| i1 = i_35 ),
inference(equality_factoring,[status(thm)],[f4687]) ).
fof(f4820,plain,
( i2 = i_35
| select(a_20,i3) = e_36
| i1 = i_35 ),
inference(duplicate_literals_removal,[status(thm)],[f4803]) ).
fof(f4821,plain,
( i2 = i_35
| select(a_22,i3) = e_37
| i1 = i_35 ),
inference(duplicate_literals_removal,[status(thm)],[f4804]) ).
fof(f4988,plain,
( i2 = i3
| i2 = i_35
| e_27 = e_36
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f584,f4820]) ).
fof(f5002,plain,
( i2 = i_35
| e_27 = e_36
| i1 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f4988,f4808]) ).
fof(f5123,plain,
( e_27 = e_36
| i1 = i_35
| select(a_20,i2) = e_36
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f5002,f263]) ).
fof(f5124,plain,
( e_27 = e_36
| i1 = i_35
| select(a_22,i2) = e_37
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f5002,f251]) ).
fof(f5136,plain,
( e_27 = e_36
| i1 = i_35
| e_23 = e_36
| i1 = i_35 ),
inference(forward_demodulation,[status(thm)],[f1212,f5123]) ).
fof(f5137,plain,
( e_27 = e_36
| e_23 = e_36
| i1 = i_35 ),
inference(duplicate_literals_removal,[status(thm)],[f5136]) ).
fof(f5138,plain,
( e_27 = e_36
| i1 = i_35
| e_23 = e_37
| i1 = i_35 ),
inference(forward_demodulation,[status(thm)],[f39,f5124]) ).
fof(f5139,plain,
( e_27 = e_36
| e_23 = e_37
| i1 = i_35 ),
inference(duplicate_literals_removal,[status(thm)],[f5138]) ).
fof(f5351,plain,
( e_27 = e_36
| i1 = i_35
| e_36 != e_23 ),
inference(paramodulation,[status(thm)],[f5139,f49]) ).
fof(f5352,plain,
( e_27 = e_36
| i1 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f5351,f5137]) ).
fof(f5365,plain,
( e_27 = e_36
| select(store(store(a1,i_35,e_19),i1,e_36),i1) = e_19 ),
inference(paramodulation,[status(thm)],[f5352,f3788]) ).
fof(f5461,plain,
( e_27 = e_36
| select(store(store(a2,i1,e_37),i1,e_19),i1) = e_37 ),
inference(paramodulation,[status(thm)],[f5352,f318]) ).
fof(f5469,plain,
( e_27 = e_36
| e_36 = e_19 ),
inference(forward_demodulation,[status(thm)],[f25,f5365]) ).
fof(f5474,plain,
( e_27 = e_36
| e_19 = e_37 ),
inference(forward_demodulation,[status(thm)],[f25,f5461]) ).
fof(f5563,plain,
( e_27 = e_36
| e_36 != e_19 ),
inference(paramodulation,[status(thm)],[f5474,f49]) ).
fof(f5566,plain,
e_27 = e_36,
inference(forward_subsumption_resolution,[status(thm)],[f5563,f5469]) ).
fof(f5602,plain,
( select(a_20,i_35) = e_27
| i1 = i_35 ),
inference(backward_demodulation,[status(thm)],[f5566,f263]) ).
fof(f5603,plain,
e_27 = select(a1,i_35),
inference(backward_demodulation,[status(thm)],[f5566,f45]) ).
fof(f5604,plain,
e_27 != e_37,
inference(backward_demodulation,[status(thm)],[f5566,f49]) ).
fof(f5705,plain,
( i2 = i3
| i2 = i_35
| e_27 = e_37
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f476,f4821]) ).
fof(f5721,plain,
( i2 = i3
| i2 = i_35
| i1 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f5705,f5604]) ).
fof(f5730,plain,
( i2 = i_35
| i1 = i_35 ),
inference(forward_subsumption_resolution,[status(thm)],[f5721,f4808]) ).
fof(f5731,plain,
( i1 = i_35
| select(a_20,i2) = e_27
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f5730,f5602]) ).
fof(f5790,plain,
( i1 = i_35
| select(a_22,i2) = e_37
| i1 = i_35 ),
inference(paramodulation,[status(thm)],[f5730,f251]) ).
fof(f5793,plain,
( i1 = i_35
| e_23 = e_27
| i1 = i_35 ),
inference(forward_demodulation,[status(thm)],[f1212,f5731]) ).
fof(f5794,plain,
( e_23 = e_27
| i1 = i_35 ),
inference(duplicate_literals_removal,[status(thm)],[f5793]) ).
fof(f5798,plain,
( i1 = i_35
| e_23 = e_37
| i1 = i_35 ),
inference(forward_demodulation,[status(thm)],[f39,f5790]) ).
fof(f5799,plain,
( e_23 = e_37
| i1 = i_35 ),
inference(duplicate_literals_removal,[status(thm)],[f5798]) ).
fof(f5870,plain,
( i1 = i_35
| e_27 != e_23 ),
inference(paramodulation,[status(thm)],[f5799,f5604]) ).
fof(f5912,plain,
i1 = i_35,
inference(forward_subsumption_resolution,[status(thm)],[f5870,f5794]) ).
fof(f5918,plain,
e_27 = select(a1,i1),
inference(backward_demodulation,[status(thm)],[f5912,f5603]) ).
fof(f5954,plain,
select(store(store(a2,i1,e_37),i1,e_19),i1) = e_37,
inference(backward_demodulation,[status(thm)],[f5912,f318]) ).
fof(f5961,plain,
e_27 = e_19,
inference(forward_demodulation,[status(thm)],[f3666,f5918]) ).
fof(f6010,plain,
e_19 = e_37,
inference(forward_demodulation,[status(thm)],[f25,f5954]) ).
fof(f6013,plain,
e_19 != e_37,
inference(backward_demodulation,[status(thm)],[f5961,f5604]) ).
fof(f6028,plain,
e_19 != e_19,
inference(forward_demodulation,[status(thm)],[f6010,f6013]) ).
fof(f6029,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f6028]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV565-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:14:52 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 17.34/2.67 % Refutation found
% 17.34/2.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 17.34/2.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.60/2.73 % Elapsed time: 2.353265 seconds
% 2.60/2.73 % CPU time: 18.156927 seconds
% 2.60/2.73 % Total memory used: 288.948 MB
% 2.60/2.73 % Net memory used: 281.310 MB
%------------------------------------------------------------------------------