%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWV565-1.007 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Wed Jul 20 16:26:43 EDT 2022
% Result : Unsatisfiable 7.40s 7.83s
% Output : Refutation 7.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV565-1.007 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n017.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Thu Jun 16 03:38:40 EDT 2022
% 0.13/0.34 % CPUTime :
% 7.40/7.83 *** allocated 10000 integers for termspace/termends
% 7.40/7.83 *** allocated 10000 integers for clauses
% 7.40/7.83 *** allocated 10000 integers for justifications
% 7.40/7.83 Bliksem 1.12
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 Automatic Strategy Selection
% 7.40/7.83
% 7.40/7.83 Clauses:
% 7.40/7.83 [
% 7.40/7.83 [ =( select( store( X, Y, Z ), Y ), Z ) ],
% 7.40/7.83 [ =( X, Y ), =( select( store( Z, X, T ), Y ), select( Z, Y ) ) ],
% 7.40/7.83 [ =( store( store( X, Y, select( X, Z ) ), Z, select( X, Y ) ), store(
% 7.40/7.83 store( X, Z, select( X, Y ) ), Y, select( X, Z ) ) ) ],
% 7.40/7.83 [ =( 'a_32', store( a1, i1, 'e_31' ) ) ],
% 7.40/7.83 [ =( 'a_34', store( a2, i1, 'e_33' ) ) ],
% 7.40/7.83 [ =( 'a_36', store( 'a_32', i2, 'e_35' ) ) ],
% 7.40/7.83 [ =( 'a_38', store( 'a_34', i2, 'e_37' ) ) ],
% 7.40/7.83 [ =( 'a_40', store( 'a_36', i3, 'e_39' ) ) ],
% 7.40/7.83 [ =( 'a_42', store( 'a_38', i3, 'e_41' ) ) ],
% 7.40/7.83 [ =( 'a_44', store( 'a_40', i4, 'e_43' ) ) ],
% 7.40/7.83 [ =( 'a_46', store( 'a_42', i4, 'e_45' ) ) ],
% 7.40/7.83 [ =( 'a_48', store( 'a_44', i5, 'e_47' ) ) ],
% 7.40/7.83 [ =( 'a_50', store( 'a_46', i5, 'e_49' ) ) ],
% 7.40/7.83 [ =( 'a_52', store( 'a_48', i6, 'e_51' ) ) ],
% 7.40/7.83 [ =( 'a_54', store( 'a_50', i6, 'e_53' ) ) ],
% 7.40/7.83 [ =( 'a_56', store( 'a_52', i7, 'e_55' ) ) ],
% 7.40/7.83 [ =( 'a_58', store( 'a_54', i7, 'e_57' ) ) ],
% 7.40/7.83 [ =( 'e_31', select( a2, i1 ) ) ],
% 7.40/7.83 [ =( 'e_33', select( a1, i1 ) ) ],
% 7.40/7.83 [ =( 'e_35', select( 'a_34', i2 ) ) ],
% 7.40/7.83 [ =( 'e_37', select( 'a_32', i2 ) ) ],
% 7.40/7.83 [ =( 'e_39', select( 'a_38', i3 ) ) ],
% 7.40/7.83 [ =( 'e_41', select( 'a_36', i3 ) ) ],
% 7.40/7.83 [ =( 'e_43', select( 'a_42', i4 ) ) ],
% 7.40/7.83 [ =( 'e_45', select( 'a_40', i4 ) ) ],
% 7.40/7.83 [ =( 'e_47', select( 'a_46', i5 ) ) ],
% 7.40/7.83 [ =( 'e_49', select( 'a_44', i5 ) ) ],
% 7.40/7.83 [ =( 'e_51', select( 'a_50', i6 ) ) ],
% 7.40/7.83 [ =( 'e_53', select( 'a_48', i6 ) ) ],
% 7.40/7.83 [ =( 'e_55', select( 'a_54', i7 ) ) ],
% 7.40/7.83 [ =( 'e_57', select( 'a_52', i7 ) ) ],
% 7.40/7.83 [ =( 'e_60', select( a1, 'i_59' ) ) ],
% 7.40/7.83 [ =( 'e_61', select( a2, 'i_59' ) ) ],
% 7.40/7.83 [ =( 'i_59', sk( a1, a2 ) ) ],
% 7.40/7.83 [ =( 'a_56', 'a_58' ) ],
% 7.40/7.83 [ ~( =( 'e_60', 'e_61' ) ) ]
% 7.40/7.83 ] .
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 percentage equality = 1.000000, percentage horn = 0.972222
% 7.40/7.83 This is a pure equality problem
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 Options Used:
% 7.40/7.83
% 7.40/7.83 useres = 1
% 7.40/7.83 useparamod = 1
% 7.40/7.83 useeqrefl = 1
% 7.40/7.83 useeqfact = 1
% 7.40/7.83 usefactor = 1
% 7.40/7.83 usesimpsplitting = 0
% 7.40/7.83 usesimpdemod = 5
% 7.40/7.83 usesimpres = 3
% 7.40/7.83
% 7.40/7.83 resimpinuse = 1000
% 7.40/7.83 resimpclauses = 20000
% 7.40/7.83 substype = eqrewr
% 7.40/7.83 backwardsubs = 1
% 7.40/7.83 selectoldest = 5
% 7.40/7.83
% 7.40/7.83 litorderings [0] = split
% 7.40/7.83 litorderings [1] = extend the termordering, first sorting on arguments
% 7.40/7.83
% 7.40/7.83 termordering = kbo
% 7.40/7.83
% 7.40/7.83 litapriori = 0
% 7.40/7.83 termapriori = 1
% 7.40/7.83 litaposteriori = 0
% 7.40/7.83 termaposteriori = 0
% 7.40/7.83 demodaposteriori = 0
% 7.40/7.83 ordereqreflfact = 0
% 7.40/7.83
% 7.40/7.83 litselect = negord
% 7.40/7.83
% 7.40/7.83 maxweight = 15
% 7.40/7.83 maxdepth = 30000
% 7.40/7.83 maxlength = 115
% 7.40/7.83 maxnrvars = 195
% 7.40/7.83 excuselevel = 1
% 7.40/7.83 increasemaxweight = 1
% 7.40/7.83
% 7.40/7.83 maxselected = 10000000
% 7.40/7.83 maxnrclauses = 10000000
% 7.40/7.83
% 7.40/7.83 showgenerated = 0
% 7.40/7.83 showkept = 0
% 7.40/7.83 showselected = 0
% 7.40/7.83 showdeleted = 0
% 7.40/7.83 showresimp = 1
% 7.40/7.83 showstatus = 2000
% 7.40/7.83
% 7.40/7.83 prologoutput = 1
% 7.40/7.83 nrgoals = 5000000
% 7.40/7.83 totalproof = 1
% 7.40/7.83
% 7.40/7.83 Symbols occurring in the translation:
% 7.40/7.83
% 7.40/7.83 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 7.40/7.83 . [1, 2] (w:1, o:58, a:1, s:1, b:0),
% 7.40/7.83 ! [4, 1] (w:0, o:53, a:1, s:1, b:0),
% 7.40/7.83 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.40/7.83 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.40/7.83 store [42, 3] (w:1, o:85, a:1, s:1, b:0),
% 7.40/7.83 select [43, 2] (w:1, o:83, a:1, s:1, b:0),
% 7.40/7.83 'a_32' [45, 0] (w:1, o:13, a:1, s:1, b:0),
% 7.40/7.83 a1 [46, 0] (w:1, o:14, a:1, s:1, b:0),
% 7.40/7.83 i1 [47, 0] (w:1, o:15, a:1, s:1, b:0),
% 7.40/7.83 'e_31' [48, 0] (w:1, o:16, a:1, s:1, b:0),
% 7.40/7.83 'a_34' [49, 0] (w:1, o:17, a:1, s:1, b:0),
% 7.40/7.83 a2 [50, 0] (w:1, o:18, a:1, s:1, b:0),
% 7.40/7.83 'e_33' [51, 0] (w:1, o:19, a:1, s:1, b:0),
% 7.40/7.83 'a_36' [52, 0] (w:1, o:20, a:1, s:1, b:0),
% 7.40/7.83 i2 [53, 0] (w:1, o:21, a:1, s:1, b:0),
% 7.40/7.83 'e_35' [54, 0] (w:1, o:22, a:1, s:1, b:0),
% 7.40/7.83 'a_38' [55, 0] (w:1, o:23, a:1, s:1, b:0),
% 7.40/7.83 'e_37' [56, 0] (w:1, o:24, a:1, s:1, b:0),
% 7.40/7.83 'a_40' [57, 0] (w:1, o:25, a:1, s:1, b:0),
% 7.40/7.83 i3 [58, 0] (w:1, o:26, a:1, s:1, b:0),
% 7.40/7.83 'e_39' [59, 0] (w:1, o:27, a:1, s:1, b:0),
% 7.40/7.83 'a_42' [60, 0] (w:1, o:28, a:1, s:1, b:0),
% 7.40/7.83 'e_41' [61, 0] (w:1, o:29, a:1, s:1, b:0),
% 7.40/7.83 'a_44' [62, 0] (w:1, o:30, a:1, s:1, b:0),
% 7.40/7.83 i4 [63, 0] (w:1, o:31, a:1, s:1, b:0),
% 7.40/7.83 'e_43' [64, 0] (w:1, o:32, a:1, s:1, b:0),
% 7.40/7.83 'a_46' [65, 0] (w:1, o:33, a:1, s:1, b:0),
% 7.40/7.83 'e_45' [66, 0] (w:1, o:34, a:1, s:1, b:0),
% 7.40/7.83 'a_48' [67, 0] (w:1, o:35, a:1, s:1, b:0),
% 7.40/7.83 i5 [68, 0] (w:1, o:36, a:1, s:1, b:0),
% 7.40/7.83 'e_47' [69, 0] (w:1, o:37, a:1, s:1, b:0),
% 7.40/7.83 'a_50' [70, 0] (w:1, o:38, a:1, s:1, b:0),
% 7.40/7.83 'e_49' [71, 0] (w:1, o:39, a:1, s:1, b:0),
% 7.40/7.83 'a_52' [72, 0] (w:1, o:40, a:1, s:1, b:0),
% 7.40/7.83 i6 [73, 0] (w:1, o:41, a:1, s:1, b:0),
% 7.40/7.83 'e_51' [74, 0] (w:1, o:42, a:1, s:1, b:0),
% 7.40/7.83 'a_54' [75, 0] (w:1, o:43, a:1, s:1, b:0),
% 7.40/7.83 'e_53' [76, 0] (w:1, o:44, a:1, s:1, b:0),
% 7.40/7.83 'a_56' [77, 0] (w:1, o:45, a:1, s:1, b:0),
% 7.40/7.83 i7 [78, 0] (w:1, o:46, a:1, s:1, b:0),
% 7.40/7.83 'e_55' [79, 0] (w:1, o:47, a:1, s:1, b:0),
% 7.40/7.83 'a_58' [80, 0] (w:1, o:48, a:1, s:1, b:0),
% 7.40/7.83 'e_57' [81, 0] (w:1, o:49, a:1, s:1, b:0),
% 7.40/7.83 'e_60' [82, 0] (w:1, o:50, a:1, s:1, b:0),
% 7.40/7.83 'i_59' [83, 0] (w:1, o:51, a:1, s:1, b:0),
% 7.40/7.83 'e_61' [84, 0] (w:1, o:52, a:1, s:1, b:0),
% 7.40/7.83 sk [85, 2] (w:1, o:84, a:1, s:1, b:0).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 Starting Search:
% 7.40/7.83
% 7.40/7.83 Resimplifying inuse:
% 7.40/7.83 Done
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 Intermediate Status:
% 7.40/7.83 Generated: 18079
% 7.40/7.83 Kept: 2005
% 7.40/7.83 Inuse: 200
% 7.40/7.83 Deleted: 11
% 7.40/7.83 Deletedinuse: 3
% 7.40/7.83
% 7.40/7.83 Resimplifying inuse:
% 7.40/7.83 Done
% 7.40/7.83
% 7.40/7.83 Resimplifying inuse:
% 7.40/7.83 Done
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 Intermediate Status:
% 7.40/7.83 Generated: 39017
% 7.40/7.83 Kept: 4154
% 7.40/7.83 Inuse: 317
% 7.40/7.83 Deleted: 28
% 7.40/7.83 Deletedinuse: 15
% 7.40/7.83
% 7.40/7.83 Resimplifying inuse:
% 7.40/7.83 Done
% 7.40/7.83
% 7.40/7.83 Resimplifying inuse:
% 7.40/7.83 Done
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 Intermediate Status:
% 7.40/7.83 Generated: 79488
% 7.40/7.83 Kept: 6165
% 7.40/7.83 Inuse: 448
% 7.40/7.83 Deleted: 170
% 7.40/7.83 Deletedinuse: 110
% 7.40/7.83
% 7.40/7.83 Resimplifying inuse:
% 7.40/7.83 Done
% 7.40/7.83
% 7.40/7.83 Resimplifying inuse:
% 7.40/7.83 Done
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 Intermediate Status:
% 7.40/7.83 Generated: 121542
% 7.40/7.83 Kept: 8176
% 7.40/7.83 Inuse: 617
% 7.40/7.83 Deleted: 440
% 7.40/7.83 Deletedinuse: 314
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 Bliksems!, er is een bewijs:
% 7.40/7.83 % SZS status Unsatisfiable
% 7.40/7.83 % SZS output start Refutation
% 7.40/7.83
% 7.40/7.83 clause( 0, [ =( select( store( X, Y, Z ), Y ), Z ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1, [ =( X, Y ), =( select( store( Z, X, T ), Y ), select( Z, Y ) )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 3, [ =( store( a1, i1, 'e_31' ), 'a_32' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4, [ =( store( a2, i1, 'e_33' ), 'a_34' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 5, [ =( store( 'a_32', i2, 'e_35' ), 'a_36' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6, [ =( store( 'a_34', i2, 'e_37' ), 'a_38' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 7, [ =( store( 'a_36', i3, 'e_39' ), 'a_40' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 8, [ =( store( 'a_38', i3, 'e_41' ), 'a_42' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 9, [ =( store( 'a_40', i4, 'e_43' ), 'a_44' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 10, [ =( store( 'a_42', i4, 'e_45' ), 'a_46' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 11, [ =( store( 'a_44', i5, 'e_47' ), 'a_48' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 12, [ =( store( 'a_46', i5, 'e_49' ), 'a_50' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 13, [ =( store( 'a_48', i6, 'e_51' ), 'a_52' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 14, [ =( store( 'a_50', i6, 'e_53' ), 'a_54' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 15, [ =( store( 'a_52', i7, 'e_55' ), 'a_56' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 16, [ =( store( 'a_54', i7, 'e_57' ), 'a_58' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 17, [ =( select( a2, i1 ), 'e_31' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 18, [ =( select( a1, i1 ), 'e_33' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 19, [ =( select( 'a_34', i2 ), 'e_35' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 20, [ =( select( 'a_32', i2 ), 'e_37' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 21, [ =( select( 'a_38', i3 ), 'e_39' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 22, [ =( select( 'a_36', i3 ), 'e_41' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 23, [ =( select( 'a_42', i4 ), 'e_43' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 24, [ =( select( 'a_40', i4 ), 'e_45' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 25, [ =( select( 'a_46', i5 ), 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 26, [ =( select( 'a_44', i5 ), 'e_49' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 27, [ =( select( 'a_50', i6 ), 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 28, [ =( select( 'a_48', i6 ), 'e_53' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 29, [ =( select( 'a_54', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 30, [ =( select( 'a_52', i7 ), 'e_57' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 31, [ =( select( a1, 'i_59' ), 'e_60' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 32, [ =( select( a2, 'i_59' ), 'e_61' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 34, [ =( 'a_58', 'a_56' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 35, [ ~( =( 'e_61', 'e_60' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 40, [ =( select( 'a_50', X ), 'e_51' ), =( select( store( Y, i6, Z
% 7.40/7.83 ), X ), select( Y, X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 41, [ =( select( 'a_50', X ), 'e_51' ), =( select( store( Y, X, Z )
% 7.40/7.83 , i6 ), select( Y, i6 ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 44, [ =( select( 'a_48', X ), 'e_53' ), =( select( store( Y, i6, Z
% 7.40/7.83 ), X ), select( Y, X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 45, [ =( select( 'a_48', X ), 'e_53' ), =( select( store( Y, X, Z )
% 7.40/7.83 , i6 ), select( Y, i6 ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 49, [ =( select( 'a_54', X ), 'e_55' ), =( select( store( Y, X, Z )
% 7.40/7.83 , i7 ), select( Y, i7 ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 59, [ =( select( a1, X ), 'e_60' ), =( select( store( Y, X, Z ),
% 7.40/7.83 'i_59' ), select( Y, 'i_59' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 63, [ =( select( a2, X ), 'e_61' ), =( select( store( Y, X, Z ),
% 7.40/7.83 'i_59' ), select( Y, 'i_59' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 135, [ =( select( 'a_32', i1 ), 'e_31' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 148, [ =( select( a2, X ), 'e_31' ), =( select( store( Y, i1, Z ),
% 7.40/7.83 X ), select( Y, X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 150, [ =( store( 'a_54', i7, 'e_57' ), 'a_56' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 158, [ =( select( 'a_34', i1 ), 'e_33' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 163, [ =( i7, X ), =( select( 'a_56', X ), select( 'a_54', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 164, [ =( select( 'a_56', i7 ), 'e_57' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 175, [ =( i7, X ), =( select( 'a_54', X ), select( 'a_52', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 176, [ =( 'e_57', 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 183, [ =( i2, X ), =( select( 'a_36', X ), select( 'a_32', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 184, [ =( select( 'a_36', i2 ), 'e_35' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 185, [ =( store( 'a_54', i7, 'e_55' ), 'a_56' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 196, [ =( i6, X ), =( select( 'a_54', X ), select( 'a_50', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 197, [ =( select( 'a_54', i6 ), 'e_53' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 204, [ =( i2, X ), =( select( 'a_38', X ), select( 'a_34', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 205, [ =( select( 'a_38', i2 ), 'e_37' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 220, [ =( i6, X ), =( select( 'a_52', X ), select( 'a_48', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 221, [ =( select( 'a_52', i6 ), 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 232, [ =( i3, X ), =( select( 'a_40', X ), select( 'a_36', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 233, [ =( select( 'a_40', i3 ), 'e_39' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 244, [ =( i5, X ), =( select( 'a_50', X ), select( 'a_46', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 245, [ =( select( 'a_50', i5 ), 'e_49' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 256, [ =( i5, X ), =( select( 'a_48', X ), select( 'a_44', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 257, [ =( select( 'a_48', i5 ), 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 264, [ =( i3, X ), =( select( 'a_42', X ), select( 'a_38', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 265, [ =( select( 'a_42', i3 ), 'e_41' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 280, [ =( i4, X ), =( select( 'a_46', X ), select( 'a_42', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 281, [ =( select( 'a_46', i4 ), 'e_45' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 292, [ =( i4, X ), =( select( 'a_44', X ), select( 'a_40', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 293, [ =( select( 'a_44', i4 ), 'e_43' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 299, [ =( select( 'a_44', X ), 'e_43' ), =( select( 'a_44', X ),
% 7.40/7.83 select( 'a_40', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 311, [ =( 'e_43', 'e_41' ), =( select( 'a_44', i3 ), 'e_39' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 324, [ =( 'e_45', 'e_39' ), =( select( 'a_44', i3 ), 'e_39' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 381, [ =( select( 'a_40', X ), 'e_45' ), =( select( 'a_44', X ),
% 7.40/7.83 select( 'a_40', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 385, [ =( 'e_49', 'e_43' ), =( select( 'a_40', i5 ), 'e_49' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 402, [ =( select( 'a_44', X ), select( 'a_40', X ) ), ~( =( 'e_45'
% 7.40/7.83 , 'e_43' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 462, [ =( select( 'a_50', X ), 'e_51' ), =( select( 'a_54', X ),
% 7.40/7.83 select( 'a_50', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 493, [ =( select( 'a_46', X ), 'e_45' ), =( select( 'a_46', X ),
% 7.40/7.83 select( 'a_42', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 500, [ =( 'e_43', 'e_41' ), =( select( 'a_46', i3 ), 'e_41' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 513, [ =( 'e_45', 'e_39' ), =( select( 'a_46', i3 ), 'e_41' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 568, [ =( select( 'a_42', X ), 'e_43' ), =( select( 'a_46', X ),
% 7.40/7.83 select( 'a_42', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 575, [ =( 'e_49', 'e_43' ), =( select( 'a_42', i5 ), 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 590, [ =( select( 'a_46', X ), select( 'a_42', X ) ), ~( =( 'e_45'
% 7.40/7.83 , 'e_43' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 591, [ ~( =( select( 'a_42', X ), 'e_45' ) ), =( select( 'a_46', X
% 7.40/7.83 ), 'e_45' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 610, [ =( select( 'a_50', i7 ), 'e_51' ), =( select( 'a_56', i6 ),
% 7.40/7.83 'e_53' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 612, [ =( select( 'a_50', i7 ), 'e_51' ), =( 'e_53', 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 678, [ =( 'e_45', 'e_39' ), =( 'e_45', 'e_41' ), ~( =( 'e_45',
% 7.40/7.83 'e_41' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 693, [ =( select( 'a_48', X ), 'e_53' ), =( select( 'a_52', X ),
% 7.40/7.83 select( 'a_48', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 714, [ =( select( 'a_48', i7 ), 'e_53' ), =( select( 'a_56', i6 ),
% 7.40/7.83 'e_53' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 716, [ =( select( 'a_48', i7 ), 'e_53' ), =( 'e_53', 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 864, [ =( select( 'a_42', X ), 'e_41' ), =( select( 'a_42', X ),
% 7.40/7.83 select( 'a_38', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 928, [ =( select( 'a_38', X ), 'e_39' ), =( select( 'a_42', X ),
% 7.40/7.83 select( 'a_38', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 932, [ =( 'e_43', 'e_41' ), =( select( 'a_38', i4 ), 'e_43' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 950, [ =( select( 'a_42', X ), select( 'a_38', X ) ), ~( =( 'e_41'
% 7.40/7.83 , 'e_39' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 951, [ ~( =( select( 'a_38', X ), 'e_41' ) ), =( select( 'a_42', X
% 7.40/7.83 ), 'e_41' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1011, [ =( select( 'a_52', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1021, [ =( 'e_55', 'e_53' ), =( select( 'a_48', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1024, [ =( 'e_55', 'e_53' ), =( select( 'a_50', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1035, [ =( 'e_55', 'e_53' ), =( 'e_53', 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1102, [ ~( =( 'e_41', 'e_39' ) ), =( 'e_41', 'e_39' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1133, [ =( 'e_43', 'e_41' ), ~( =( 'e_43', 'e_41' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1234, [ =( 'e_55', 'e_53' ), =( 'e_55', 'e_49' ), =( select( 'a_44'
% 7.40/7.83 , i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1238, [ =( 'e_55', 'e_53' ), =( select( 'a_44', i7 ), 'e_55' ), =(
% 7.40/7.83 'e_49', 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1325, [ =( select( 'a_48', X ), 'e_47' ), =( select( 'a_48', X ),
% 7.40/7.83 select( 'a_44', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1399, [ =( select( 'a_44', X ), 'e_49' ), =( select( 'a_48', X ),
% 7.40/7.83 select( 'a_44', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1407, [ =( select( 'a_48', X ), select( 'a_44', X ) ), ~( =( 'e_49'
% 7.40/7.83 , 'e_47' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1444, [ =( 'e_55', 'e_53' ), =( select( 'a_44', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1447, [ ~( =( 'e_49', 'e_47' ) ), =( 'e_49', 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1477, [ =( 'e_60', 'e_33' ), =( select( 'a_34', 'i_59' ), 'e_61' )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1479, [ =( 'e_60', 'e_33' ), =( select( 'a_32', 'i_59' ), 'e_60' )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1514, [ =( select( 'a_40', i7 ), 'e_55' ), ~( =( 'e_45', 'e_43' ) )
% 7.40/7.83 , =( 'e_55', 'e_53' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1517, [ =( 'e_55', 'e_53' ), =( 'e_55', 'e_43' ), =( select( 'a_40'
% 7.40/7.83 , i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1641, [ =( 'e_61', 'e_31' ), =( select( 'a_34', 'i_59' ), 'e_61' )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1643, [ =( 'e_61', 'e_31' ), =( select( 'a_32', 'i_59' ), 'e_60' )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1658, [ =( select( 'a_34', 'i_59' ), 'e_61' ), ~( =( 'e_33', 'e_31'
% 7.40/7.83 ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1683, [ =( select( 'a_32', 'i_59' ), 'e_60' ), ~( =( 'e_33', 'e_31'
% 7.40/7.83 ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1761, [ =( 'e_55', 'e_53' ), =( 'e_55', 'e_49' ), =( select( 'a_46'
% 7.40/7.83 , i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1795, [ =( 'e_55', 'e_53' ), =( select( 'a_46', i7 ), 'e_55' ), =(
% 7.40/7.83 'e_49', 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1891, [ =( select( 'a_50', X ), 'e_49' ), =( select( 'a_50', X ),
% 7.40/7.83 select( 'a_46', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1952, [ =( select( 'a_46', X ), 'e_47' ), =( select( 'a_50', X ),
% 7.40/7.83 select( 'a_46', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 1958, [ =( select( 'a_50', X ), select( 'a_46', X ) ), ~( =( 'e_49'
% 7.40/7.83 , 'e_47' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 2000, [ =( 'e_55', 'e_53' ), =( select( 'a_46', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 2052, [ =( 'e_55', 'e_53' ), =( select( 'a_40', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 2353, [ =( select( 'a_40', X ), 'e_39' ), =( select( 'a_40', X ),
% 7.40/7.83 select( 'a_36', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 2404, [ =( select( 'a_36', X ), 'e_41' ), =( select( 'a_40', X ),
% 7.40/7.83 select( 'a_36', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 2414, [ =( select( 'a_40', X ), select( 'a_36', X ) ), ~( =( 'e_41'
% 7.40/7.83 , 'e_39' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 2910, [ =( select( 'a_52', X ), 'e_51' ), =( select( 'a_52', X ),
% 7.40/7.83 select( 'a_48', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 2962, [ =( select( 'a_52', X ), select( 'a_48', X ) ), ~( =( 'e_53'
% 7.40/7.83 , 'e_51' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 3143, [ =( select( 'a_48', i7 ), 'e_55' ), ~( =( 'e_53', 'e_51' ) )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 3144, [ ~( =( 'e_53', 'e_51' ) ), =( 'e_53', 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 3506, [ =( select( 'a_38', X ), 'e_37' ), =( select( 'a_38', X ),
% 7.40/7.83 select( 'a_34', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 3525, [ =( 'e_35', 'e_33' ), =( select( 'a_38', i1 ), 'e_33' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 3534, [ =( 'e_37', 'e_31' ), =( select( 'a_38', i1 ), 'e_33' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 3539, [ =( select( 'a_34', X ), 'e_35' ), =( select( 'a_38', X ),
% 7.40/7.83 select( 'a_34', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 3549, [ =( select( 'a_38', X ), select( 'a_34', X ) ), ~( =( 'e_37'
% 7.40/7.83 , 'e_35' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4005, [ =( 'e_53', 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4106, [ =( select( 'a_54', X ), select( 'a_50', X ) ), =( select(
% 7.40/7.83 'a_54', X ), 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4150, [ =( select( 'a_54', X ), select( 'a_50', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4156, [ =( select( 'a_48', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4157, [ =( select( 'a_52', X ), select( 'a_48', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4161, [ =( select( 'a_40', i7 ), 'e_55' ), =( 'e_55', 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4162, [ =( select( 'a_46', i7 ), 'e_55' ), =( 'e_55', 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4166, [ =( select( 'a_44', i7 ), 'e_55' ), =( 'e_55', 'e_51' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4180, [ =( select( 'a_50', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4188, [ =( select( 'a_46', i7 ), 'e_55' ), =( 'e_51', 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4190, [ =( select( 'a_44', i7 ), 'e_55' ), ~( =( 'e_49', 'e_47' ) )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4192, [ =( select( 'a_44', i7 ), 'e_55' ), =( 'e_51', 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4231, [ =( select( 'a_46', i7 ), 'e_55' ), ~( =( 'e_49', 'e_47' ) )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4233, [ =( select( 'a_46', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4235, [ =( select( 'a_44', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4258, [ =( select( 'a_42', i7 ), 'e_55' ), ~( =( 'e_45', 'e_43' ) )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4260, [ =( 'e_55', 'e_45' ), =( select( 'a_42', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4263, [ =( select( 'a_40', i7 ), 'e_55' ), =( 'e_51', 'e_45' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4280, [ =( select( 'a_42', i7 ), 'e_55' ), =( 'e_45', 'e_43' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4282, [ =( select( 'a_40', i7 ), 'e_55' ), ~( =( 'e_45', 'e_43' ) )
% 7.40/7.83 ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4284, [ =( select( 'a_40', i7 ), 'e_55' ), =( 'e_45', 'e_43' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4350, [ =( select( 'a_42', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 4463, [ =( select( 'a_40', i7 ), 'e_55' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 5566, [ =( select( 'a_36', X ), 'e_35' ), =( select( 'a_36', X ),
% 7.40/7.83 select( 'a_32', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 5590, [ =( select( 'a_32', X ), 'e_37' ), =( select( 'a_36', X ),
% 7.40/7.83 select( 'a_32', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 5592, [ =( select( 'a_36', X ), select( 'a_32', X ) ), ~( =( 'e_37'
% 7.40/7.83 , 'e_35' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6165, [ =( i7, X ), =( select( 'a_50', X ), select( 'a_48', X ) ) ]
% 7.40/7.83 )
% 7.40/7.83 .
% 7.40/7.83 clause( 6218, [ =( select( 'a_50', X ), 'e_55' ), =( select( 'a_50', X ),
% 7.40/7.83 select( 'a_48', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6222, [ =( select( 'a_48', X ), 'e_55' ), =( select( 'a_50', X ),
% 7.40/7.83 select( 'a_48', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6328, [ =( 'e_49', 'e_43' ), =( 'e_55', 'e_47' ), =( 'e_49', 'e_47'
% 7.40/7.83 ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6349, [ =( 'e_49', 'e_43' ), =( 'e_49', 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6367, [ =( 'e_55', 'e_47' ), =( 'e_49', 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6376, [ =( 'e_49', 'e_47' ), =( 'e_47', 'e_43' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6429, [ =( 'e_49', 'e_47' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6439, [ =( select( 'a_50', X ), select( 'a_48', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6448, [ =( select( 'a_48', X ), select( 'a_46', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6453, [ =( select( 'a_46', X ), select( 'a_44', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6456, [ ~( =( 'e_45', 'e_43' ) ), =( select( 'a_42', X ), select(
% 7.40/7.83 'a_40', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6458, [ =( 'e_45', 'e_39' ), =( 'e_41', 'e_39' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6459, [ =( 'e_43', 'e_41' ), =( 'e_41', 'e_39' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6466, [ =( 'e_45', 'e_43' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6489, [ =( 'e_41', 'e_39' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6492, [ =( select( 'a_40', X ), select( 'a_36', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 6495, [ =( select( 'a_42', X ), select( 'a_38', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 7224, [ =( select( a2, X ), 'e_31' ), =( select( a2, X ), select(
% 7.40/7.83 'a_34', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 7225, [ ~( =( select( 'a_34', X ), 'e_31' ) ), =( select( a2, X ),
% 7.40/7.83 select( 'a_34', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 7226, [ ~( =( select( 'a_34', X ), 'e_31' ) ), =( select( 'a_34', X
% 7.40/7.83 ), 'e_31' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 7304, [ =( 'e_33', 'e_31' ), ~( =( 'e_33', 'e_31' ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 8344, [ =( select( 'a_38', X ), select( 'a_36', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 8369, [ =( 'e_37', 'e_35' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 8370, [ =( select( 'a_36', X ), select( 'a_32', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 8372, [ =( select( 'a_34', X ), select( 'a_32', X ) ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 8380, [ =( 'e_33', 'e_31' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 8384, [ =( select( 'a_32', 'i_59' ), 'e_60' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 8385, [ =( 'e_61', 'e_60' ) ] )
% 7.40/7.83 .
% 7.40/7.83 clause( 8387, [] )
% 7.40/7.83 .
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 % SZS output end Refutation
% 7.40/7.83 found a proof!
% 7.40/7.83
% 7.40/7.83 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 7.40/7.83
% 7.40/7.83 initialclauses(
% 7.40/7.83 [ clause( 8389, [ =( select( store( X, Y, Z ), Y ), Z ) ] )
% 7.40/7.83 , clause( 8390, [ =( X, Y ), =( select( store( Z, X, T ), Y ), select( Z, Y
% 7.40/7.83 ) ) ] )
% 7.40/7.83 , clause( 8391, [ =( store( store( X, Y, select( X, Z ) ), Z, select( X, Y
% 7.40/7.83 ) ), store( store( X, Z, select( X, Y ) ), Y, select( X, Z ) ) ) ] )
% 7.40/7.83 , clause( 8392, [ =( 'a_32', store( a1, i1, 'e_31' ) ) ] )
% 7.40/7.83 , clause( 8393, [ =( 'a_34', store( a2, i1, 'e_33' ) ) ] )
% 7.40/7.83 , clause( 8394, [ =( 'a_36', store( 'a_32', i2, 'e_35' ) ) ] )
% 7.40/7.83 , clause( 8395, [ =( 'a_38', store( 'a_34', i2, 'e_37' ) ) ] )
% 7.40/7.83 , clause( 8396, [ =( 'a_40', store( 'a_36', i3, 'e_39' ) ) ] )
% 7.40/7.83 , clause( 8397, [ =( 'a_42', store( 'a_38', i3, 'e_41' ) ) ] )
% 7.40/7.83 , clause( 8398, [ =( 'a_44', store( 'a_40', i4, 'e_43' ) ) ] )
% 7.40/7.83 , clause( 8399, [ =( 'a_46', store( 'a_42', i4, 'e_45' ) ) ] )
% 7.40/7.83 , clause( 8400, [ =( 'a_48', store( 'a_44', i5, 'e_47' ) ) ] )
% 7.40/7.83 , clause( 8401, [ =( 'a_50', store( 'a_46', i5, 'e_49' ) ) ] )
% 7.40/7.83 , clause( 8402, [ =( 'a_52', store( 'a_48', i6, 'e_51' ) ) ] )
% 7.40/7.83 , clause( 8403, [ =( 'a_54', store( 'a_50', i6, 'e_53' ) ) ] )
% 7.40/7.83 , clause( 8404, [ =( 'a_56', store( 'a_52', i7, 'e_55' ) ) ] )
% 7.40/7.83 , clause( 8405, [ =( 'a_58', store( 'a_54', i7, 'e_57' ) ) ] )
% 7.40/7.83 , clause( 8406, [ =( 'e_31', select( a2, i1 ) ) ] )
% 7.40/7.83 , clause( 8407, [ =( 'e_33', select( a1, i1 ) ) ] )
% 7.40/7.83 , clause( 8408, [ =( 'e_35', select( 'a_34', i2 ) ) ] )
% 7.40/7.83 , clause( 8409, [ =( 'e_37', select( 'a_32', i2 ) ) ] )
% 7.40/7.83 , clause( 8410, [ =( 'e_39', select( 'a_38', i3 ) ) ] )
% 7.40/7.83 , clause( 8411, [ =( 'e_41', select( 'a_36', i3 ) ) ] )
% 7.40/7.83 , clause( 8412, [ =( 'e_43', select( 'a_42', i4 ) ) ] )
% 7.40/7.83 , clause( 8413, [ =( 'e_45', select( 'a_40', i4 ) ) ] )
% 7.40/7.83 , clause( 8414, [ =( 'e_47', select( 'a_46', i5 ) ) ] )
% 7.40/7.83 , clause( 8415, [ =( 'e_49', select( 'a_44', i5 ) ) ] )
% 7.40/7.83 , clause( 8416, [ =( 'e_51', select( 'a_50', i6 ) ) ] )
% 7.40/7.83 , clause( 8417, [ =( 'e_53', select( 'a_48', i6 ) ) ] )
% 7.40/7.83 , clause( 8418, [ =( 'e_55', select( 'a_54', i7 ) ) ] )
% 7.40/7.83 , clause( 8419, [ =( 'e_57', select( 'a_52', i7 ) ) ] )
% 7.40/7.83 , clause( 8420, [ =( 'e_60', select( a1, 'i_59' ) ) ] )
% 7.40/7.83 , clause( 8421, [ =( 'e_61', select( a2, 'i_59' ) ) ] )
% 7.40/7.83 , clause( 8422, [ =( 'i_59', sk( a1, a2 ) ) ] )
% 7.40/7.83 , clause( 8423, [ =( 'a_56', 'a_58' ) ] )
% 7.40/7.83 , clause( 8424, [ ~( =( 'e_60', 'e_61' ) ) ] )
% 7.40/7.83 ] ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 0, [ =( select( store( X, Y, Z ), Y ), Z ) ] )
% 7.40/7.83 , clause( 8389, [ =( select( store( X, Y, Z ), Y ), Z ) ] )
% 7.40/7.83 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 7.40/7.83 permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 1, [ =( X, Y ), =( select( store( Z, X, T ), Y ), select( Z, Y ) )
% 7.40/7.83 ] )
% 7.40/7.83 , clause( 8390, [ =( X, Y ), =( select( store( Z, X, T ), Y ), select( Z, Y
% 7.40/7.83 ) ) ] )
% 7.40/7.83 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 7.40/7.83 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8434, [ =( store( a1, i1, 'e_31' ), 'a_32' ) ] )
% 7.40/7.83 , clause( 8392, [ =( 'a_32', store( a1, i1, 'e_31' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 3, [ =( store( a1, i1, 'e_31' ), 'a_32' ) ] )
% 7.40/7.83 , clause( 8434, [ =( store( a1, i1, 'e_31' ), 'a_32' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8440, [ =( store( a2, i1, 'e_33' ), 'a_34' ) ] )
% 7.40/7.83 , clause( 8393, [ =( 'a_34', store( a2, i1, 'e_33' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 4, [ =( store( a2, i1, 'e_33' ), 'a_34' ) ] )
% 7.40/7.83 , clause( 8440, [ =( store( a2, i1, 'e_33' ), 'a_34' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8447, [ =( store( 'a_32', i2, 'e_35' ), 'a_36' ) ] )
% 7.40/7.83 , clause( 8394, [ =( 'a_36', store( 'a_32', i2, 'e_35' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 5, [ =( store( 'a_32', i2, 'e_35' ), 'a_36' ) ] )
% 7.40/7.83 , clause( 8447, [ =( store( 'a_32', i2, 'e_35' ), 'a_36' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8455, [ =( store( 'a_34', i2, 'e_37' ), 'a_38' ) ] )
% 7.40/7.83 , clause( 8395, [ =( 'a_38', store( 'a_34', i2, 'e_37' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 6, [ =( store( 'a_34', i2, 'e_37' ), 'a_38' ) ] )
% 7.40/7.83 , clause( 8455, [ =( store( 'a_34', i2, 'e_37' ), 'a_38' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8464, [ =( store( 'a_36', i3, 'e_39' ), 'a_40' ) ] )
% 7.40/7.83 , clause( 8396, [ =( 'a_40', store( 'a_36', i3, 'e_39' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 7, [ =( store( 'a_36', i3, 'e_39' ), 'a_40' ) ] )
% 7.40/7.83 , clause( 8464, [ =( store( 'a_36', i3, 'e_39' ), 'a_40' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8474, [ =( store( 'a_38', i3, 'e_41' ), 'a_42' ) ] )
% 7.40/7.83 , clause( 8397, [ =( 'a_42', store( 'a_38', i3, 'e_41' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 8, [ =( store( 'a_38', i3, 'e_41' ), 'a_42' ) ] )
% 7.40/7.83 , clause( 8474, [ =( store( 'a_38', i3, 'e_41' ), 'a_42' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8485, [ =( store( 'a_40', i4, 'e_43' ), 'a_44' ) ] )
% 7.40/7.83 , clause( 8398, [ =( 'a_44', store( 'a_40', i4, 'e_43' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 9, [ =( store( 'a_40', i4, 'e_43' ), 'a_44' ) ] )
% 7.40/7.83 , clause( 8485, [ =( store( 'a_40', i4, 'e_43' ), 'a_44' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8497, [ =( store( 'a_42', i4, 'e_45' ), 'a_46' ) ] )
% 7.40/7.83 , clause( 8399, [ =( 'a_46', store( 'a_42', i4, 'e_45' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 10, [ =( store( 'a_42', i4, 'e_45' ), 'a_46' ) ] )
% 7.40/7.83 , clause( 8497, [ =( store( 'a_42', i4, 'e_45' ), 'a_46' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8510, [ =( store( 'a_44', i5, 'e_47' ), 'a_48' ) ] )
% 7.40/7.83 , clause( 8400, [ =( 'a_48', store( 'a_44', i5, 'e_47' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 11, [ =( store( 'a_44', i5, 'e_47' ), 'a_48' ) ] )
% 7.40/7.83 , clause( 8510, [ =( store( 'a_44', i5, 'e_47' ), 'a_48' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8524, [ =( store( 'a_46', i5, 'e_49' ), 'a_50' ) ] )
% 7.40/7.83 , clause( 8401, [ =( 'a_50', store( 'a_46', i5, 'e_49' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 12, [ =( store( 'a_46', i5, 'e_49' ), 'a_50' ) ] )
% 7.40/7.83 , clause( 8524, [ =( store( 'a_46', i5, 'e_49' ), 'a_50' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8539, [ =( store( 'a_48', i6, 'e_51' ), 'a_52' ) ] )
% 7.40/7.83 , clause( 8402, [ =( 'a_52', store( 'a_48', i6, 'e_51' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 13, [ =( store( 'a_48', i6, 'e_51' ), 'a_52' ) ] )
% 7.40/7.83 , clause( 8539, [ =( store( 'a_48', i6, 'e_51' ), 'a_52' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8555, [ =( store( 'a_50', i6, 'e_53' ), 'a_54' ) ] )
% 7.40/7.83 , clause( 8403, [ =( 'a_54', store( 'a_50', i6, 'e_53' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 14, [ =( store( 'a_50', i6, 'e_53' ), 'a_54' ) ] )
% 7.40/7.83 , clause( 8555, [ =( store( 'a_50', i6, 'e_53' ), 'a_54' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8572, [ =( store( 'a_52', i7, 'e_55' ), 'a_56' ) ] )
% 7.40/7.83 , clause( 8404, [ =( 'a_56', store( 'a_52', i7, 'e_55' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 15, [ =( store( 'a_52', i7, 'e_55' ), 'a_56' ) ] )
% 7.40/7.83 , clause( 8572, [ =( store( 'a_52', i7, 'e_55' ), 'a_56' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8590, [ =( store( 'a_54', i7, 'e_57' ), 'a_58' ) ] )
% 7.40/7.83 , clause( 8405, [ =( 'a_58', store( 'a_54', i7, 'e_57' ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 16, [ =( store( 'a_54', i7, 'e_57' ), 'a_58' ) ] )
% 7.40/7.83 , clause( 8590, [ =( store( 'a_54', i7, 'e_57' ), 'a_58' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8609, [ =( select( a2, i1 ), 'e_31' ) ] )
% 7.40/7.83 , clause( 8406, [ =( 'e_31', select( a2, i1 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 17, [ =( select( a2, i1 ), 'e_31' ) ] )
% 7.40/7.83 , clause( 8609, [ =( select( a2, i1 ), 'e_31' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8629, [ =( select( a1, i1 ), 'e_33' ) ] )
% 7.40/7.83 , clause( 8407, [ =( 'e_33', select( a1, i1 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 18, [ =( select( a1, i1 ), 'e_33' ) ] )
% 7.40/7.83 , clause( 8629, [ =( select( a1, i1 ), 'e_33' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8650, [ =( select( 'a_34', i2 ), 'e_35' ) ] )
% 7.40/7.83 , clause( 8408, [ =( 'e_35', select( 'a_34', i2 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 19, [ =( select( 'a_34', i2 ), 'e_35' ) ] )
% 7.40/7.83 , clause( 8650, [ =( select( 'a_34', i2 ), 'e_35' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8672, [ =( select( 'a_32', i2 ), 'e_37' ) ] )
% 7.40/7.83 , clause( 8409, [ =( 'e_37', select( 'a_32', i2 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 20, [ =( select( 'a_32', i2 ), 'e_37' ) ] )
% 7.40/7.83 , clause( 8672, [ =( select( 'a_32', i2 ), 'e_37' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8695, [ =( select( 'a_38', i3 ), 'e_39' ) ] )
% 7.40/7.83 , clause( 8410, [ =( 'e_39', select( 'a_38', i3 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 21, [ =( select( 'a_38', i3 ), 'e_39' ) ] )
% 7.40/7.83 , clause( 8695, [ =( select( 'a_38', i3 ), 'e_39' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8719, [ =( select( 'a_36', i3 ), 'e_41' ) ] )
% 7.40/7.83 , clause( 8411, [ =( 'e_41', select( 'a_36', i3 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 22, [ =( select( 'a_36', i3 ), 'e_41' ) ] )
% 7.40/7.83 , clause( 8719, [ =( select( 'a_36', i3 ), 'e_41' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8744, [ =( select( 'a_42', i4 ), 'e_43' ) ] )
% 7.40/7.83 , clause( 8412, [ =( 'e_43', select( 'a_42', i4 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 23, [ =( select( 'a_42', i4 ), 'e_43' ) ] )
% 7.40/7.83 , clause( 8744, [ =( select( 'a_42', i4 ), 'e_43' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8770, [ =( select( 'a_40', i4 ), 'e_45' ) ] )
% 7.40/7.83 , clause( 8413, [ =( 'e_45', select( 'a_40', i4 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 24, [ =( select( 'a_40', i4 ), 'e_45' ) ] )
% 7.40/7.83 , clause( 8770, [ =( select( 'a_40', i4 ), 'e_45' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8797, [ =( select( 'a_46', i5 ), 'e_47' ) ] )
% 7.40/7.83 , clause( 8414, [ =( 'e_47', select( 'a_46', i5 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 25, [ =( select( 'a_46', i5 ), 'e_47' ) ] )
% 7.40/7.83 , clause( 8797, [ =( select( 'a_46', i5 ), 'e_47' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8825, [ =( select( 'a_44', i5 ), 'e_49' ) ] )
% 7.40/7.83 , clause( 8415, [ =( 'e_49', select( 'a_44', i5 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 26, [ =( select( 'a_44', i5 ), 'e_49' ) ] )
% 7.40/7.83 , clause( 8825, [ =( select( 'a_44', i5 ), 'e_49' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8854, [ =( select( 'a_50', i6 ), 'e_51' ) ] )
% 7.40/7.83 , clause( 8416, [ =( 'e_51', select( 'a_50', i6 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 27, [ =( select( 'a_50', i6 ), 'e_51' ) ] )
% 7.40/7.83 , clause( 8854, [ =( select( 'a_50', i6 ), 'e_51' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8884, [ =( select( 'a_48', i6 ), 'e_53' ) ] )
% 7.40/7.83 , clause( 8417, [ =( 'e_53', select( 'a_48', i6 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 28, [ =( select( 'a_48', i6 ), 'e_53' ) ] )
% 7.40/7.83 , clause( 8884, [ =( select( 'a_48', i6 ), 'e_53' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 clause( 8915, [ =( select( 'a_54', i7 ), 'e_55' ) ] )
% 7.40/7.83 , clause( 8418, [ =( 'e_55', select( 'a_54', i7 ) ) ] )
% 7.40/7.83 , 0, substitution( 0, [] )).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 subsumption(
% 7.40/7.83 clause( 29, [ =( select( 'a_54', i7 ), 'e_55' ) ] )
% 7.40/7.83 , clause( 8915, [ =( select( 'a_54', i7 ), 'e_55' ) ] )
% 7.40/7.83 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.40/7.83
% 7.40/7.83
% 7.40/7.83 eqswap(
% 7.40/7.83 claCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------