%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWV249-2 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n015.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:23:11 EDT 2022
% Result : Unsatisfiable 26.73s 27.17s
% Output : Refutation 26.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SWV249-2 : TPTP v8.1.0. Released v3.2.0.
% 0.10/0.13 % Command : bliksem %s
% 0.14/0.34 % Computer : n015.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % DateTime : Tue Jun 14 22:36:54 EDT 2022
% 0.14/0.34 % CPUTime :
% 26.73/27.17 *** allocated 10000 integers for termspace/termends
% 26.73/27.17 *** allocated 10000 integers for clauses
% 26.73/27.17 *** allocated 10000 integers for justifications
% 26.73/27.17 Bliksem 1.12
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Automatic Strategy Selection
% 26.73/27.17
% 26.73/27.17 Clauses:
% 26.73/27.17 [
% 26.73/27.17 [ 'c_in'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ),
% 26.73/27.17 'tc_Message_Omsg' ) ],
% 26.73/27.17 [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X', 'v_H',
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Osynth'( 'c_Message_Oanalz'(
% 26.73/27.17 'v_G' ) ), 'c_Message_Oanalz'( 'c_union'( 'v_G', 'v_H', 'tc_Message_Omsg'
% 26.73/27.17 ) ), 'tc_Message_Omsg' ), 'tc_set'( 'tc_Message_Omsg' ) ) ) ],
% 26.73/27.17 [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Oanalz'( X ), Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ],
% 26.73/27.17 [ ~( 'c_lessequals'( X, Y, 'tc_set'( 'tc_Message_Omsg' ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_Message_Oanalz'( X ), 'c_Message_Oanalz'( Y ),
% 26.73/27.17 'tc_set'( 'tc_Message_Omsg' ) ) ],
% 26.73/27.17 [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'( X ), Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' ) ) ]
% 26.73/27.17 ,
% 26.73/27.17 [ ~( 'class_Orderings_Oorder'( X ) ), 'c_lessequals'( Y, Y, X ) ],
% 26.73/27.17 [ =( 'c_union'( 'c_minus'( X, Y, 'tc_set'( Z ) ), Y, Z ), 'c_union'( X,
% 26.73/27.17 Y, Z ) ) ],
% 26.73/27.17 [ =( 'c_union'( X, 'c_minus'( Y, X, 'tc_set'( Z ) ), Z ), 'c_union'( X,
% 26.73/27.17 Y, Z ) ) ],
% 26.73/27.17 [ =( 'c_union'( 'c_insert'( X, Y, Z ), T, Z ), 'c_insert'( X, 'c_union'(
% 26.73/27.17 Y, T, Z ), Z ) ) ],
% 26.73/27.17 [ =( 'c_union'( X, 'c_insert'( Y, Z, T ), T ), 'c_insert'( Y, 'c_union'(
% 26.73/27.17 X, Z, T ), T ) ) ],
% 26.73/27.17 [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( X, T, 'tc_set'( Z ) ) ],
% 26.73/27.17 [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ],
% 26.73/27.17 [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~( 'c_lessequals'( T, Y,
% 26.73/27.17 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_union'( T, X, Z ), Y, 'tc_set'( Z )
% 26.73/27.17 ) ],
% 26.73/27.17 [ ~( 'c_lessequals'( 'c_insert'( X, Y, Z ), T, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ],
% 26.73/27.17 [ ~( 'c_in'( X, Y, Z ) ), ~( 'c_lessequals'( T, Y, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_insert'( X, T, Z ), Y, 'tc_set'( Z ) ) ],
% 26.73/27.17 [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ), =( Y, X ) ],
% 26.73/27.17 [ 'class_Orderings_Oorder'( 'tc_set'( X ) ) ]
% 26.73/27.17 ] .
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 percentage equality = 0.250000, percentage horn = 1.000000
% 26.73/27.17 This is a problem with some equality
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Options Used:
% 26.73/27.17
% 26.73/27.17 useres = 1
% 26.73/27.17 useparamod = 1
% 26.73/27.17 useeqrefl = 1
% 26.73/27.17 useeqfact = 1
% 26.73/27.17 usefactor = 1
% 26.73/27.17 usesimpsplitting = 0
% 26.73/27.17 usesimpdemod = 5
% 26.73/27.17 usesimpres = 3
% 26.73/27.17
% 26.73/27.17 resimpinuse = 1000
% 26.73/27.17 resimpclauses = 20000
% 26.73/27.17 substype = eqrewr
% 26.73/27.17 backwardsubs = 1
% 26.73/27.17 selectoldest = 5
% 26.73/27.17
% 26.73/27.17 litorderings [0] = split
% 26.73/27.17 litorderings [1] = extend the termordering, first sorting on arguments
% 26.73/27.17
% 26.73/27.17 termordering = kbo
% 26.73/27.17
% 26.73/27.17 litapriori = 0
% 26.73/27.17 termapriori = 1
% 26.73/27.17 litaposteriori = 0
% 26.73/27.17 termaposteriori = 0
% 26.73/27.17 demodaposteriori = 0
% 26.73/27.17 ordereqreflfact = 0
% 26.73/27.17
% 26.73/27.17 litselect = negord
% 26.73/27.17
% 26.73/27.17 maxweight = 15
% 26.73/27.17 maxdepth = 30000
% 26.73/27.17 maxlength = 115
% 26.73/27.17 maxnrvars = 195
% 26.73/27.17 excuselevel = 1
% 26.73/27.17 increasemaxweight = 1
% 26.73/27.17
% 26.73/27.17 maxselected = 10000000
% 26.73/27.17 maxnrclauses = 10000000
% 26.73/27.17
% 26.73/27.17 showgenerated = 0
% 26.73/27.17 showkept = 0
% 26.73/27.17 showselected = 0
% 26.73/27.17 showdeleted = 0
% 26.73/27.17 showresimp = 1
% 26.73/27.17 showstatus = 2000
% 26.73/27.17
% 26.73/27.17 prologoutput = 1
% 26.73/27.17 nrgoals = 5000000
% 26.73/27.17 totalproof = 1
% 26.73/27.17
% 26.73/27.17 Symbols occurring in the translation:
% 26.73/27.17
% 26.73/27.17 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 26.73/27.17 . [1, 2] (w:1, o:31, a:1, s:1, b:0),
% 26.73/27.17 ! [4, 1] (w:0, o:22, a:1, s:1, b:0),
% 26.73/27.17 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 26.73/27.17 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 26.73/27.17 'v_X' [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 26.73/27.17 'v_G' [40, 0] (w:1, o:10, a:1, s:1, b:0),
% 26.73/27.17 'c_Message_Oanalz' [41, 1] (w:1, o:27, a:1, s:1, b:0),
% 26.73/27.17 'c_Message_Osynth' [42, 1] (w:1, o:28, a:1, s:1, b:0),
% 26.73/27.17 'tc_Message_Omsg' [43, 0] (w:1, o:11, a:1, s:1, b:0),
% 26.73/27.17 'c_in' [44, 3] (w:1, o:56, a:1, s:1, b:0),
% 26.73/27.17 'v_H' [45, 0] (w:1, o:12, a:1, s:1, b:0),
% 26.73/27.17 'c_insert' [46, 3] (w:1, o:57, a:1, s:1, b:0),
% 26.73/27.17 'c_union' [47, 3] (w:1, o:58, a:1, s:1, b:0),
% 26.73/27.17 'tc_set' [48, 1] (w:1, o:29, a:1, s:1, b:0),
% 26.73/27.17 'c_lessequals' [49, 3] (w:1, o:59, a:1, s:1, b:0),
% 26.73/27.17 'class_Orderings_Oorder' [53, 1] (w:1, o:30, a:1, s:1, b:0),
% 26.73/27.17 'c_minus' [57, 3] (w:1, o:60, a:1, s:1, b:0).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Starting Search:
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 123168
% 26.73/27.17 Kept: 2003
% 26.73/27.17 Inuse: 663
% 26.73/27.17 Deleted: 86
% 26.73/27.17 Deletedinuse: 21
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 290251
% 26.73/27.17 Kept: 4006
% 26.73/27.17 Inuse: 1306
% 26.73/27.17 Deleted: 186
% 26.73/27.17 Deletedinuse: 80
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 432749
% 26.73/27.17 Kept: 6007
% 26.73/27.17 Inuse: 1873
% 26.73/27.17 Deleted: 280
% 26.73/27.17 Deletedinuse: 97
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 1093679
% 26.73/27.17 Kept: 8017
% 26.73/27.17 Inuse: 3986
% 26.73/27.17 Deleted: 379
% 26.73/27.17 Deletedinuse: 108
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 1667508
% 26.73/27.17 Kept: 10017
% 26.73/27.17 Inuse: 5859
% 26.73/27.17 Deleted: 412
% 26.73/27.17 Deletedinuse: 108
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Failed to find proof!
% 26.73/27.17 maxweight = 15
% 26.73/27.17 maxnrclauses = 10000000
% 26.73/27.17 Generated: 2965521
% 26.73/27.17 Kept: 10521
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 The strategy used was not complete!
% 26.73/27.17
% 26.73/27.17 Increased maxweight to 16
% 26.73/27.17
% 26.73/27.17 Starting Search:
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 22455
% 26.73/27.17 Kept: 2005
% 26.73/27.17 Inuse: 389
% 26.73/27.17 Deleted: 54
% 26.73/27.17 Deletedinuse: 21
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 164785
% 26.73/27.17 Kept: 4007
% 26.73/27.17 Inuse: 843
% 26.73/27.17 Deleted: 120
% 26.73/27.17 Deletedinuse: 46
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 263113
% 26.73/27.17 Kept: 6187
% 26.73/27.17 Inuse: 1258
% 26.73/27.17 Deleted: 195
% 26.73/27.17 Deletedinuse: 80
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 358031
% 26.73/27.17 Kept: 8244
% 26.73/27.17 Inuse: 1609
% 26.73/27.17 Deleted: 230
% 26.73/27.17 Deletedinuse: 96
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 462590
% 26.73/27.17 Kept: 10250
% 26.73/27.17 Inuse: 1988
% 26.73/27.17 Deleted: 329
% 26.73/27.17 Deletedinuse: 138
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 544245
% 26.73/27.17 Kept: 12341
% 26.73/27.17 Inuse: 2328
% 26.73/27.17 Deleted: 388
% 26.73/27.17 Deletedinuse: 159
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 747156
% 26.73/27.17 Kept: 14343
% 26.73/27.17 Inuse: 2994
% 26.73/27.17 Deleted: 463
% 26.73/27.17 Deletedinuse: 163
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 995568
% 26.73/27.17 Kept: 16343
% 26.73/27.17 Inuse: 3766
% 26.73/27.17 Deleted: 520
% 26.73/27.17 Deletedinuse: 163
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Intermediate Status:
% 26.73/27.17 Generated: 1389736
% 26.73/27.17 Kept: 18343
% 26.73/27.17 Inuse: 4784
% 26.73/27.17 Deleted: 591
% 26.73/27.17 Deletedinuse: 166
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying inuse:
% 26.73/27.17 Done
% 26.73/27.17
% 26.73/27.17 Resimplifying clauses:
% 26.73/27.17
% 26.73/27.17 Bliksems!, er is een bewijs:
% 26.73/27.17 % SZS status Unsatisfiable
% 26.73/27.17 % SZS output start Refutation
% 26.73/27.17
% 26.73/27.17 clause( 0, [ 'c_in'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' )
% 26.73/27.17 ), 'tc_Message_Omsg' ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 1, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'c_Message_Oanalz'( 'c_union'( 'v_G',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'tc_Message_Omsg' ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 2, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Oanalz'( X ), Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 3, [ ~( 'c_lessequals'( X, Y, 'tc_set'( 'tc_Message_Omsg' ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_Message_Oanalz'( X ), 'c_Message_Oanalz'( Y ),
% 26.73/27.17 'tc_set'( 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 4, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' ),
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'( X ), Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 5, [ ~( 'class_Orderings_Oorder'( X ) ), 'c_lessequals'( Y, Y, X )
% 26.73/27.17 ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 6, [ =( 'c_union'( 'c_minus'( X, Y, 'tc_set'( Z ) ), Y, Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 7, [ =( 'c_union'( X, 'c_minus'( Y, X, 'tc_set'( Z ) ), Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 8, [ =( 'c_union'( 'c_insert'( X, Y, Z ), T, Z ), 'c_insert'( X,
% 26.73/27.17 'c_union'( Y, T, Z ), Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 9, [ =( 'c_union'( X, 'c_insert'( Y, Z, T ), T ), 'c_insert'( Y,
% 26.73/27.17 'c_union'( X, Z, T ), T ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 10, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ) )
% 26.73/27.17 , 'c_lessequals'( X, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 11, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ) )
% 26.73/27.17 , 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 12, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~( 'c_lessequals'(
% 26.73/27.17 T, Y, 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_union'( T, X, Z ), Y,
% 26.73/27.17 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 13, [ ~( 'c_lessequals'( 'c_insert'( X, Y, Z ), T, 'tc_set'( Z ) )
% 26.73/27.17 ), 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 14, [ ~( 'c_in'( X, Y, Z ) ), ~( 'c_lessequals'( T, Y, 'tc_set'( Z
% 26.73/27.17 ) ) ), 'c_lessequals'( 'c_insert'( X, T, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 15, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~( 'c_lessequals'(
% 26.73/27.17 Y, X, 'tc_set'( Z ) ) ), =( Y, X ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 16, [ 'class_Orderings_Oorder'( 'tc_set'( X ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 18, [ 'c_lessequals'( X, X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 26, [ 'c_lessequals'( X, 'c_insert'( Y, X, Z ), 'tc_set'( Z ) ) ]
% 26.73/27.17 )
% 26.73/27.17 .
% 26.73/27.17 clause( 32, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( 'c_Message_Oanalz'( X ) ),
% 26.73/27.17 'tc_Message_Omsg' ), 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( X ) ), Y, 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 42, [ 'c_lessequals'( X, 'c_union'( Y, X, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 45, [ 'c_lessequals'( 'c_Message_Oanalz'( X ), 'c_Message_Oanalz'(
% 26.73/27.17 'c_union'( Y, X, 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg' ) ) ]
% 26.73/27.17 )
% 26.73/27.17 .
% 26.73/27.17 clause( 79, [ 'c_lessequals'( X, 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 85, [ 'c_lessequals'( 'c_minus'( X, Y, 'tc_set'( Z ) ), 'c_union'(
% 26.73/27.17 X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 115, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( Y, Z,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_insert'( Y, 'c_union'( X, Z
% 26.73/27.17 , 'tc_Message_Omsg' ), 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg'
% 26.73/27.17 ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 127, [ 'c_lessequals'( 'c_minus'( 'c_minus'( X, Y, 'tc_set'( Z ) )
% 26.73/27.17 , Y, 'tc_set'( Z ) ), 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 143, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), 'c_lessequals'(
% 26.73/27.17 'c_union'( X, Y, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 144, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), 'c_lessequals'(
% 26.73/27.17 'c_union'( Y, X, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 147, [ ~( 'c_lessequals'( 'c_minus'( Y, X, 'tc_set'( Z ) ), T,
% 26.73/27.17 'tc_set'( Z ) ) ), ~( 'c_lessequals'( X, T, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 180, [ ~( 'c_in'( X, Y, Z ) ), 'c_lessequals'( 'c_insert'( X, Y, Z
% 26.73/27.17 ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 190, [ =( 'c_insert'( Y, X, Z ), X ), ~( 'c_in'( Y, X, Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 195, [ =( 'c_union'( Y, X, Z ), X ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 269, [ =( 'c_insert'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'(
% 26.73/27.17 'v_G' ) ), 'tc_Message_Omsg' ), 'c_Message_Osynth'( 'c_Message_Oanalz'(
% 26.73/27.17 'v_G' ) ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 313, [ =( 'c_insert'( 'v_X', 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' ), 'tc_Message_Omsg'
% 26.73/27.17 ), 'c_union'( 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), X,
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 458, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), =( 'c_union'( Y
% 26.73/27.17 , X, Z ), Y ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 2457, [ 'c_lessequals'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z )
% 26.73/27.17 , 'tc_set'( Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 2475, [ =( 'c_union'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z ), Z
% 26.73/27.17 ), 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 2477, [ =( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 2500, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'(
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), 'v_H',
% 26.73/27.17 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 4758, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X', X,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' ) ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 .
% 26.73/27.17 clause( 20000, [] )
% 26.73/27.17 .
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 % SZS output end Refutation
% 26.73/27.17 found a proof!
% 26.73/27.17
% 26.73/27.17 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 26.73/27.17
% 26.73/27.17 initialclauses(
% 26.73/27.17 [ clause( 20002, [ 'c_in'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'(
% 26.73/27.17 'v_G' ) ), 'tc_Message_Omsg' ) ] )
% 26.73/27.17 , clause( 20003, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X'
% 26.73/27.17 , 'v_H', 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'c_Message_Oanalz'( 'c_union'( 'v_G',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'tc_Message_Omsg' ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 20004, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Oanalz'( X
% 26.73/27.17 ), Y, 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 20005, [ ~( 'c_lessequals'( X, Y, 'tc_set'( 'tc_Message_Omsg' ) )
% 26.73/27.17 ), 'c_lessequals'( 'c_Message_Oanalz'( X ), 'c_Message_Oanalz'( Y ),
% 26.73/27.17 'tc_set'( 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , clause( 20006, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'( X
% 26.73/27.17 ), Y, 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Oanalz'( 'c_union'( X
% 26.73/27.17 , Y, 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' )
% 26.73/27.17 ) ] )
% 26.73/27.17 , clause( 20007, [ ~( 'class_Orderings_Oorder'( X ) ), 'c_lessequals'( Y, Y
% 26.73/27.17 , X ) ] )
% 26.73/27.17 , clause( 20008, [ =( 'c_union'( 'c_minus'( X, Y, 'tc_set'( Z ) ), Y, Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , clause( 20009, [ =( 'c_union'( X, 'c_minus'( Y, X, 'tc_set'( Z ) ), Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , clause( 20010, [ =( 'c_union'( 'c_insert'( X, Y, Z ), T, Z ), 'c_insert'(
% 26.73/27.17 X, 'c_union'( Y, T, Z ), Z ) ) ] )
% 26.73/27.17 , clause( 20011, [ =( 'c_union'( X, 'c_insert'( Y, Z, T ), T ), 'c_insert'(
% 26.73/27.17 Y, 'c_union'( X, Z, T ), T ) ) ] )
% 26.73/27.17 , clause( 20012, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z
% 26.73/27.17 ) ) ), 'c_lessequals'( X, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20013, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z
% 26.73/27.17 ) ) ), 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20014, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( T, Y, 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_union'( T, X
% 26.73/27.17 , Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20015, [ ~( 'c_lessequals'( 'c_insert'( X, Y, Z ), T, 'tc_set'( Z
% 26.73/27.17 ) ) ), 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20016, [ ~( 'c_in'( X, Y, Z ) ), ~( 'c_lessequals'( T, Y,
% 26.73/27.17 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_insert'( X, T, Z ), Y, 'tc_set'( Z
% 26.73/27.17 ) ) ] )
% 26.73/27.17 , clause( 20017, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( Y, X, 'tc_set'( Z ) ) ), =( Y, X ) ] )
% 26.73/27.17 , clause( 20018, [ 'class_Orderings_Oorder'( 'tc_set'( X ) ) ] )
% 26.73/27.17 ] ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 0, [ 'c_in'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' )
% 26.73/27.17 ), 'tc_Message_Omsg' ) ] )
% 26.73/27.17 , clause( 20002, [ 'c_in'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'(
% 26.73/27.17 'v_G' ) ), 'tc_Message_Omsg' ) ] )
% 26.73/27.17 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 1, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'c_Message_Oanalz'( 'c_union'( 'v_G',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'tc_Message_Omsg' ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 20003, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X'
% 26.73/27.17 , 'v_H', 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'c_Message_Oanalz'( 'c_union'( 'v_G',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'tc_Message_Omsg' ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 2, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Oanalz'( X ), Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 20004, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Oanalz'( X
% 26.73/27.17 ), Y, 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 26.73/27.17 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 3, [ ~( 'c_lessequals'( X, Y, 'tc_set'( 'tc_Message_Omsg' ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_Message_Oanalz'( X ), 'c_Message_Oanalz'( Y ),
% 26.73/27.17 'tc_set'( 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , clause( 20005, [ ~( 'c_lessequals'( X, Y, 'tc_set'( 'tc_Message_Omsg' ) )
% 26.73/27.17 ), 'c_lessequals'( 'c_Message_Oanalz'( X ), 'c_Message_Oanalz'( Y ),
% 26.73/27.17 'tc_set'( 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 26.73/27.17 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20022, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' ),
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'( X ), Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 20006, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'( X
% 26.73/27.17 ), Y, 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Oanalz'( 'c_union'( X
% 26.73/27.17 , Y, 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' )
% 26.73/27.17 ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 4, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' ),
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'( X ), Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 20022, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' ),
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'( X ), Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 26.73/27.17 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 5, [ ~( 'class_Orderings_Oorder'( X ) ), 'c_lessequals'( Y, Y, X )
% 26.73/27.17 ] )
% 26.73/27.17 , clause( 20007, [ ~( 'class_Orderings_Oorder'( X ) ), 'c_lessequals'( Y, Y
% 26.73/27.17 , X ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 26.73/27.17 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 6, [ =( 'c_union'( 'c_minus'( X, Y, 'tc_set'( Z ) ), Y, Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , clause( 20008, [ =( 'c_union'( 'c_minus'( X, Y, 'tc_set'( Z ) ), Y, Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 7, [ =( 'c_union'( X, 'c_minus'( Y, X, 'tc_set'( Z ) ), Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , clause( 20009, [ =( 'c_union'( X, 'c_minus'( Y, X, 'tc_set'( Z ) ), Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 8, [ =( 'c_union'( 'c_insert'( X, Y, Z ), T, Z ), 'c_insert'( X,
% 26.73/27.17 'c_union'( Y, T, Z ), Z ) ) ] )
% 26.73/27.17 , clause( 20010, [ =( 'c_union'( 'c_insert'( X, Y, Z ), T, Z ), 'c_insert'(
% 26.73/27.17 X, 'c_union'( Y, T, Z ), Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 9, [ =( 'c_union'( X, 'c_insert'( Y, Z, T ), T ), 'c_insert'( Y,
% 26.73/27.17 'c_union'( X, Z, T ), T ) ) ] )
% 26.73/27.17 , clause( 20011, [ =( 'c_union'( X, 'c_insert'( Y, Z, T ), T ), 'c_insert'(
% 26.73/27.17 Y, 'c_union'( X, Z, T ), T ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 10, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ) )
% 26.73/27.17 , 'c_lessequals'( X, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20012, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z
% 26.73/27.17 ) ) ), 'c_lessequals'( X, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 11, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ) )
% 26.73/27.17 , 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20013, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z
% 26.73/27.17 ) ) ), 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 12, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~( 'c_lessequals'(
% 26.73/27.17 T, Y, 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_union'( T, X, Z ), Y,
% 26.73/27.17 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20014, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( T, Y, 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_union'( T, X
% 26.73/27.17 , Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 13, [ ~( 'c_lessequals'( 'c_insert'( X, Y, Z ), T, 'tc_set'( Z ) )
% 26.73/27.17 ), 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20015, [ ~( 'c_lessequals'( 'c_insert'( X, Y, Z ), T, 'tc_set'( Z
% 26.73/27.17 ) ) ), 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 14, [ ~( 'c_in'( X, Y, Z ) ), ~( 'c_lessequals'( T, Y, 'tc_set'( Z
% 26.73/27.17 ) ) ), 'c_lessequals'( 'c_insert'( X, T, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20016, [ ~( 'c_in'( X, Y, Z ) ), ~( 'c_lessequals'( T, Y,
% 26.73/27.17 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_insert'( X, T, Z ), Y, 'tc_set'( Z
% 26.73/27.17 ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 15, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~( 'c_lessequals'(
% 26.73/27.17 Y, X, 'tc_set'( Z ) ) ), =( Y, X ) ] )
% 26.73/27.17 , clause( 20017, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( Y, X, 'tc_set'( Z ) ) ), =( Y, X ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 16, [ 'class_Orderings_Oorder'( 'tc_set'( X ) ) ] )
% 26.73/27.17 , clause( 20018, [ 'class_Orderings_Oorder'( 'tc_set'( X ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20092, [ 'c_lessequals'( Y, Y, 'tc_set'( X ) ) ] )
% 26.73/27.17 , clause( 5, [ ~( 'class_Orderings_Oorder'( X ) ), 'c_lessequals'( Y, Y, X
% 26.73/27.17 ) ] )
% 26.73/27.17 , 0, clause( 16, [ 'class_Orderings_Oorder'( 'tc_set'( X ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, 'tc_set'( X ) ), :=( Y, Y )] ),
% 26.73/27.17 substitution( 1, [ :=( X, X )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 18, [ 'c_lessequals'( X, X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 , clause( 20092, [ 'c_lessequals'( Y, Y, 'tc_set'( X ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 26.73/27.17 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20093, [ 'c_lessequals'( Y, 'c_insert'( X, Y, Z ), 'tc_set'( Z ) )
% 26.73/27.17 ] )
% 26.73/27.17 , clause( 13, [ ~( 'c_lessequals'( 'c_insert'( X, Y, Z ), T, 'tc_set'( Z )
% 26.73/27.17 ) ), 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 0, clause( 18, [ 'c_lessequals'( X, X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T,
% 26.73/27.17 'c_insert'( X, Y, Z ) )] ), substitution( 1, [ :=( X, 'c_insert'( X, Y, Z
% 26.73/27.17 ) ), :=( Y, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 26, [ 'c_lessequals'( X, 'c_insert'( Y, X, Z ), 'tc_set'( Z ) ) ]
% 26.73/27.17 )
% 26.73/27.17 , clause( 20093, [ 'c_lessequals'( Y, 'c_insert'( X, Y, Z ), 'tc_set'( Z )
% 26.73/27.17 ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20095, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'( X )
% 26.73/27.17 , Y, 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Oanalz'( 'c_union'( X,
% 26.73/27.17 Y, 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' ) )
% 26.73/27.17 ] )
% 26.73/27.17 , clause( 4, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' ),
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'( X ), Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20100, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( X ) ), Y, 'tc_Message_Omsg' ) ), 'c_union'(
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( X, Y, 'tc_Message_Omsg' ) ),
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( X ) ), 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , clause( 2, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Oanalz'( X ), Y
% 26.73/27.17 , 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , 0, clause( 20095, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 X ), Y, 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Oanalz'( 'c_union'(
% 26.73/27.17 X, Y, 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( X ), 'tc_Message_Omsg' )
% 26.73/27.17 ) ] )
% 26.73/27.17 , 0, 9, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 26.73/27.17 :=( X, 'c_Message_Oanalz'( X ) ), :=( Y, Y )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20101, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( 'c_Message_Oanalz'( X ) ),
% 26.73/27.17 'tc_Message_Omsg' ), 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( X ) ), Y, 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 20100, [ =( 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( X ) ), Y, 'tc_Message_Omsg' ) ), 'c_union'(
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( X, Y, 'tc_Message_Omsg' ) ),
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( X ) ), 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 32, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( 'c_Message_Oanalz'( X ) ),
% 26.73/27.17 'tc_Message_Omsg' ), 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( X ) ), Y, 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 20101, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( 'c_Message_Oanalz'( X ) ),
% 26.73/27.17 'tc_Message_Omsg' ), 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( X ) ), Y, 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 26.73/27.17 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20102, [ 'c_lessequals'( Y, 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ]
% 26.73/27.17 )
% 26.73/27.17 , clause( 11, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) )
% 26.73/27.17 ), 'c_lessequals'( Y, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 0, clause( 18, [ 'c_lessequals'( X, X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T,
% 26.73/27.17 'c_union'( X, Y, Z ) )] ), substitution( 1, [ :=( X, 'c_union'( X, Y, Z )
% 26.73/27.17 ), :=( Y, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 42, [ 'c_lessequals'( X, 'c_union'( Y, X, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20102, [ 'c_lessequals'( Y, 'c_union'( X, Y, Z ), 'tc_set'( Z ) )
% 26.73/27.17 ] )
% 26.73/27.17 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20103, [ 'c_lessequals'( 'c_Message_Oanalz'( X ),
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( Y, X, 'tc_Message_Omsg' ) ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , clause( 3, [ ~( 'c_lessequals'( X, Y, 'tc_set'( 'tc_Message_Omsg' ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_Message_Oanalz'( X ), 'c_Message_Oanalz'( Y ),
% 26.73/27.17 'tc_set'( 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , 0, clause( 42, [ 'c_lessequals'( X, 'c_union'( Y, X, Z ), 'tc_set'( Z ) )
% 26.73/27.17 ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, 'c_union'( Y, X,
% 26.73/27.17 'tc_Message_Omsg' ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=(
% 26.73/27.17 Z, 'tc_Message_Omsg' )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 45, [ 'c_lessequals'( 'c_Message_Oanalz'( X ), 'c_Message_Oanalz'(
% 26.73/27.17 'c_union'( Y, X, 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg' ) ) ]
% 26.73/27.17 )
% 26.73/27.17 , clause( 20103, [ 'c_lessequals'( 'c_Message_Oanalz'( X ),
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( Y, X, 'tc_Message_Omsg' ) ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 26.73/27.17 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20104, [ 'c_lessequals'( X, 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ]
% 26.73/27.17 )
% 26.73/27.17 , clause( 10, [ ~( 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) )
% 26.73/27.17 ), 'c_lessequals'( X, T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 0, clause( 18, [ 'c_lessequals'( X, X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T,
% 26.73/27.17 'c_union'( X, Y, Z ) )] ), substitution( 1, [ :=( X, 'c_union'( X, Y, Z )
% 26.73/27.17 ), :=( Y, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 79, [ 'c_lessequals'( X, 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20104, [ 'c_lessequals'( X, 'c_union'( X, Y, Z ), 'tc_set'( Z ) )
% 26.73/27.17 ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20106, [ 'c_lessequals'( 'c_minus'( X, Y, 'tc_set'( Z ) ),
% 26.73/27.17 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 6, [ =( 'c_union'( 'c_minus'( X, Y, 'tc_set'( Z ) ), Y, Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , 0, clause( 79, [ 'c_lessequals'( X, 'c_union'( X, Y, Z ), 'tc_set'( Z ) )
% 26.73/27.17 ] )
% 26.73/27.17 , 0, 6, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, 'c_minus'( X, Y, 'tc_set'( Z ) ) ), :=( Y, Y )
% 26.73/27.17 , :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 85, [ 'c_lessequals'( 'c_minus'( X, Y, 'tc_set'( Z ) ), 'c_union'(
% 26.73/27.17 X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20106, [ 'c_lessequals'( 'c_minus'( X, Y, 'tc_set'( Z ) ),
% 26.73/27.17 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20108, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_insert'( X, 'c_union'( Z, Y
% 26.73/27.17 , 'tc_Message_Omsg' ), 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg'
% 26.73/27.17 ) ) ] )
% 26.73/27.17 , clause( 9, [ =( 'c_union'( X, 'c_insert'( Y, Z, T ), T ), 'c_insert'( Y,
% 26.73/27.17 'c_union'( X, Z, T ), T ) ) ] )
% 26.73/27.17 , 0, clause( 45, [ 'c_lessequals'( 'c_Message_Oanalz'( X ),
% 26.73/27.17 'c_Message_Oanalz'( 'c_union'( Y, X, 'tc_Message_Omsg' ) ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , 0, 7, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y ), :=( T,
% 26.73/27.17 'tc_Message_Omsg' )] ), substitution( 1, [ :=( X, 'c_insert'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), :=( Y, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 115, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( Y, Z,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_insert'( Y, 'c_union'( X, Z
% 26.73/27.17 , 'tc_Message_Omsg' ), 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg'
% 26.73/27.17 ) ) ] )
% 26.73/27.17 , clause( 20108, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_insert'( X, 'c_union'( Z, Y
% 26.73/27.17 , 'tc_Message_Omsg' ), 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg'
% 26.73/27.17 ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20110, [ 'c_lessequals'( 'c_minus'( 'c_minus'( X, Y, 'tc_set'( Z )
% 26.73/27.17 ), Y, 'tc_set'( Z ) ), 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 6, [ =( 'c_union'( 'c_minus'( X, Y, 'tc_set'( Z ) ), Y, Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , 0, clause( 85, [ 'c_lessequals'( 'c_minus'( X, Y, 'tc_set'( Z ) ),
% 26.73/27.17 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 0, 10, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, 'c_minus'( X, Y, 'tc_set'( Z ) ) ), :=( Y, Y )
% 26.73/27.17 , :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 127, [ 'c_lessequals'( 'c_minus'( 'c_minus'( X, Y, 'tc_set'( Z ) )
% 26.73/27.17 , Y, 'tc_set'( Z ) ), 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20110, [ 'c_lessequals'( 'c_minus'( 'c_minus'( X, Y, 'tc_set'( Z
% 26.73/27.17 ) ), Y, 'tc_set'( Z ) ), 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20111, [ ~( 'c_lessequals'( Z, X, 'tc_set'( Y ) ) ), 'c_lessequals'(
% 26.73/27.17 'c_union'( Z, X, Y ), X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 , clause( 12, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( T, Y, 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_union'( T, X
% 26.73/27.17 , Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 0, clause( 18, [ 'c_lessequals'( X, X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, X ), :=( Z, Y ), :=( T, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 143, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), 'c_lessequals'(
% 26.73/27.17 'c_union'( X, Y, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20111, [ ~( 'c_lessequals'( Z, X, 'tc_set'( Y ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_union'( Z, X, Y ), X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20114, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), 'c_lessequals'(
% 26.73/27.17 'c_union'( Y, X, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 12, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( T, Y, 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_union'( T, X
% 26.73/27.17 , Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 1, clause( 18, [ 'c_lessequals'( X, X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, Y )] ),
% 26.73/27.17 substitution( 1, [ :=( X, Y ), :=( Y, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 144, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), 'c_lessequals'(
% 26.73/27.17 'c_union'( Y, X, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20114, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_union'( Y, X, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20116, [ 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ),
% 26.73/27.17 ~( 'c_lessequals'( 'c_minus'( Y, X, 'tc_set'( Z ) ), T, 'tc_set'( Z ) ) )
% 26.73/27.17 , ~( 'c_lessequals'( X, T, 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , clause( 7, [ =( 'c_union'( X, 'c_minus'( Y, X, 'tc_set'( Z ) ), Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , 0, clause( 12, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( T, Y, 'tc_set'( Z ) ) ), 'c_lessequals'( 'c_union'( T, X
% 26.73/27.17 , Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 2, 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, 'c_minus'( Y, X, 'tc_set'( Z ) ) ), :=( Y, T )
% 26.73/27.17 , :=( Z, Z ), :=( T, X )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 147, [ ~( 'c_lessequals'( 'c_minus'( Y, X, 'tc_set'( Z ) ), T,
% 26.73/27.17 'tc_set'( Z ) ) ), ~( 'c_lessequals'( X, T, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20116, [ 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) )
% 26.73/27.17 , ~( 'c_lessequals'( 'c_minus'( Y, X, 'tc_set'( Z ) ), T, 'tc_set'( Z ) )
% 26.73/27.17 ), ~( 'c_lessequals'( X, T, 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20117, [ ~( 'c_in'( X, Y, Z ) ), 'c_lessequals'( 'c_insert'( X, Y,
% 26.73/27.17 Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 14, [ ~( 'c_in'( X, Y, Z ) ), ~( 'c_lessequals'( T, Y, 'tc_set'(
% 26.73/27.17 Z ) ) ), 'c_lessequals'( 'c_insert'( X, T, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 1, clause( 18, [ 'c_lessequals'( X, X, 'tc_set'( Y ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, Y )] ),
% 26.73/27.17 substitution( 1, [ :=( X, Y ), :=( Y, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 180, [ ~( 'c_in'( X, Y, Z ) ), 'c_lessequals'( 'c_insert'( X, Y, Z
% 26.73/27.17 ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20117, [ ~( 'c_in'( X, Y, Z ) ), 'c_lessequals'( 'c_insert'( X, Y
% 26.73/27.17 , Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20118, [ ~( 'c_lessequals'( Y, 'c_insert'( X, Y, Z ), 'tc_set'( Z )
% 26.73/27.17 ) ), =( Y, 'c_insert'( X, Y, Z ) ), ~( 'c_in'( X, Y, Z ) ) ] )
% 26.73/27.17 , clause( 15, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( Y, X, 'tc_set'( Z ) ) ), =( Y, X ) ] )
% 26.73/27.17 , 0, clause( 180, [ ~( 'c_in'( X, Y, Z ) ), 'c_lessequals'( 'c_insert'( X,
% 26.73/27.17 Y, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 1, substitution( 0, [ :=( X, 'c_insert'( X, Y, Z ) ), :=( Y, Y ), :=( Z,
% 26.73/27.17 Z )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20120, [ =( X, 'c_insert'( Y, X, Z ) ), ~( 'c_in'( Y, X, Z ) ) ] )
% 26.73/27.17 , clause( 20118, [ ~( 'c_lessequals'( Y, 'c_insert'( X, Y, Z ), 'tc_set'( Z
% 26.73/27.17 ) ) ), =( Y, 'c_insert'( X, Y, Z ) ), ~( 'c_in'( X, Y, Z ) ) ] )
% 26.73/27.17 , 0, clause( 26, [ 'c_lessequals'( X, 'c_insert'( Y, X, Z ), 'tc_set'( Z )
% 26.73/27.17 ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20121, [ =( 'c_insert'( Y, X, Z ), X ), ~( 'c_in'( Y, X, Z ) ) ] )
% 26.73/27.17 , clause( 20120, [ =( X, 'c_insert'( Y, X, Z ) ), ~( 'c_in'( Y, X, Z ) ) ]
% 26.73/27.17 )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 190, [ =( 'c_insert'( Y, X, Z ), X ), ~( 'c_in'( Y, X, Z ) ) ] )
% 26.73/27.17 , clause( 20121, [ =( 'c_insert'( Y, X, Z ), X ), ~( 'c_in'( Y, X, Z ) ) ]
% 26.73/27.17 )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20122, [ ~( 'c_lessequals'( Y, 'c_union'( X, Y, Z ), 'tc_set'( Z )
% 26.73/27.17 ) ), =( Y, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( X, Y, 'tc_set'( Z
% 26.73/27.17 ) ) ) ] )
% 26.73/27.17 , clause( 15, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( Y, X, 'tc_set'( Z ) ) ), =( Y, X ) ] )
% 26.73/27.17 , 0, clause( 143, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_union'( X, Y, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 1, substitution( 0, [ :=( X, 'c_union'( X, Y, Z ) ), :=( Y, Y ), :=( Z, Z
% 26.73/27.17 )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20124, [ =( X, 'c_union'( Y, X, Z ) ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , clause( 20122, [ ~( 'c_lessequals'( Y, 'c_union'( X, Y, Z ), 'tc_set'( Z
% 26.73/27.17 ) ) ), =( Y, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( X, Y, 'tc_set'(
% 26.73/27.17 Z ) ) ) ] )
% 26.73/27.17 , 0, clause( 42, [ 'c_lessequals'( X, 'c_union'( Y, X, Z ), 'tc_set'( Z ) )
% 26.73/27.17 ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20125, [ =( 'c_union'( Y, X, Z ), X ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , clause( 20124, [ =( X, 'c_union'( Y, X, Z ) ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 195, [ =( 'c_union'( Y, X, Z ), X ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , clause( 20125, [ =( 'c_union'( Y, X, Z ), X ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20126, [ =( Y, 'c_insert'( X, Y, Z ) ), ~( 'c_in'( X, Y, Z ) ) ] )
% 26.73/27.17 , clause( 190, [ =( 'c_insert'( Y, X, Z ), X ), ~( 'c_in'( Y, X, Z ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20127, [ =( 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ),
% 26.73/27.17 'c_insert'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ),
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , clause( 20126, [ =( Y, 'c_insert'( X, Y, Z ) ), ~( 'c_in'( X, Y, Z ) ) ]
% 26.73/27.17 )
% 26.73/27.17 , 1, clause( 0, [ 'c_in'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'(
% 26.73/27.17 'v_G' ) ), 'tc_Message_Omsg' ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, 'v_X' ), :=( Y, 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ) ), :=( Z, 'tc_Message_Omsg' )] ),
% 26.73/27.17 substitution( 1, [] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20128, [ =( 'c_insert'( 'v_X', 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'tc_Message_Omsg' ), 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ) ) ] )
% 26.73/27.17 , clause( 20127, [ =( 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ),
% 26.73/27.17 'c_insert'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ),
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 269, [ =( 'c_insert'( 'v_X', 'c_Message_Osynth'( 'c_Message_Oanalz'(
% 26.73/27.17 'v_G' ) ), 'tc_Message_Omsg' ), 'c_Message_Osynth'( 'c_Message_Oanalz'(
% 26.73/27.17 'v_G' ) ) ) ] )
% 26.73/27.17 , clause( 20128, [ =( 'c_insert'( 'v_X', 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'tc_Message_Omsg' ), 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ) ) ] )
% 26.73/27.17 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20130, [ =( 'c_insert'( X, 'c_union'( Y, T, Z ), Z ), 'c_union'(
% 26.73/27.17 'c_insert'( X, Y, Z ), T, Z ) ) ] )
% 26.73/27.17 , clause( 8, [ =( 'c_union'( 'c_insert'( X, Y, Z ), T, Z ), 'c_insert'( X,
% 26.73/27.17 'c_union'( Y, T, Z ), Z ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] )
% 26.73/27.17 ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20131, [ =( 'c_insert'( 'v_X', 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' ), 'tc_Message_Omsg'
% 26.73/27.17 ), 'c_union'( 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), X,
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , clause( 269, [ =( 'c_insert'( 'v_X', 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'tc_Message_Omsg' ), 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ) ) ] )
% 26.73/27.17 , 0, clause( 20130, [ =( 'c_insert'( X, 'c_union'( Y, T, Z ), Z ),
% 26.73/27.17 'c_union'( 'c_insert'( X, Y, Z ), T, Z ) ) ] )
% 26.73/27.17 , 0, 11, substitution( 0, [] ), substitution( 1, [ :=( X, 'v_X' ), :=( Y,
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ) ), :=( Z,
% 26.73/27.17 'tc_Message_Omsg' ), :=( T, X )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 313, [ =( 'c_insert'( 'v_X', 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' ), 'tc_Message_Omsg'
% 26.73/27.17 ), 'c_union'( 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), X,
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , clause( 20131, [ =( 'c_insert'( 'v_X', 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' ), 'tc_Message_Omsg'
% 26.73/27.17 ), 'c_union'( 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), X,
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20133, [ ~( 'c_lessequals'( X, 'c_union'( X, Y, Z ), 'tc_set'( Z )
% 26.73/27.17 ) ), =( X, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( Y, X, 'tc_set'( Z
% 26.73/27.17 ) ) ) ] )
% 26.73/27.17 , clause( 15, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), ~(
% 26.73/27.17 'c_lessequals'( Y, X, 'tc_set'( Z ) ) ), =( Y, X ) ] )
% 26.73/27.17 , 0, clause( 144, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_union'( Y, X, Z ), Y, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 1, substitution( 0, [ :=( X, 'c_union'( X, Y, Z ) ), :=( Y, X ), :=( Z, Z
% 26.73/27.17 )] ), substitution( 1, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20135, [ =( X, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , clause( 20133, [ ~( 'c_lessequals'( X, 'c_union'( X, Y, Z ), 'tc_set'( Z
% 26.73/27.17 ) ) ), =( X, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( Y, X, 'tc_set'(
% 26.73/27.17 Z ) ) ) ] )
% 26.73/27.17 , 0, clause( 79, [ 'c_lessequals'( X, 'c_union'( X, Y, Z ), 'tc_set'( Z ) )
% 26.73/27.17 ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20136, [ =( 'c_union'( X, Y, Z ), X ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , clause( 20135, [ =( X, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 458, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), =( 'c_union'( Y
% 26.73/27.17 , X, Z ), Y ) ] )
% 26.73/27.17 , clause( 20136, [ =( 'c_union'( X, Y, Z ), X ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20138, [ ~( 'c_lessequals'( Y, 'c_union'( X, Y, Z ), 'tc_set'( Z )
% 26.73/27.17 ) ), 'c_lessequals'( 'c_union'( Y, 'c_minus'( X, Y, 'tc_set'( Z ) ), Z )
% 26.73/27.17 , 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 147, [ ~( 'c_lessequals'( 'c_minus'( Y, X, 'tc_set'( Z ) ), T,
% 26.73/27.17 'tc_set'( Z ) ) ), ~( 'c_lessequals'( X, T, 'tc_set'( Z ) ) ),
% 26.73/27.17 'c_lessequals'( 'c_union'( X, Y, Z ), T, 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 0, clause( 127, [ 'c_lessequals'( 'c_minus'( 'c_minus'( X, Y, 'tc_set'( Z
% 26.73/27.17 ) ), Y, 'tc_set'( Z ) ), 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, Y ), :=( Y, 'c_minus'( X, Y, 'tc_set'( Z ) )
% 26.73/27.17 ), :=( Z, Z ), :=( T, 'c_union'( X, Y, Z ) )] ), substitution( 1, [ :=(
% 26.73/27.17 X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20140, [ 'c_lessequals'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z )
% 26.73/27.17 , 'tc_set'( Z ) ), ~( 'c_lessequals'( X, 'c_union'( Y, X, Z ), 'tc_set'(
% 26.73/27.17 Z ) ) ) ] )
% 26.73/27.17 , clause( 7, [ =( 'c_union'( X, 'c_minus'( Y, X, 'tc_set'( Z ) ), Z ),
% 26.73/27.17 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , 0, clause( 20138, [ ~( 'c_lessequals'( Y, 'c_union'( X, Y, Z ), 'tc_set'(
% 26.73/27.17 Z ) ) ), 'c_lessequals'( 'c_union'( Y, 'c_minus'( X, Y, 'tc_set'( Z ) ),
% 26.73/27.17 Z ), 'c_union'( X, Y, Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 1, 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20141, [ 'c_lessequals'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z )
% 26.73/27.17 , 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20140, [ 'c_lessequals'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z
% 26.73/27.17 ), 'tc_set'( Z ) ), ~( 'c_lessequals'( X, 'c_union'( Y, X, Z ), 'tc_set'(
% 26.73/27.17 Z ) ) ) ] )
% 26.73/27.17 , 1, clause( 42, [ 'c_lessequals'( X, 'c_union'( Y, X, Z ), 'tc_set'( Z ) )
% 26.73/27.17 ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 2457, [ 'c_lessequals'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z )
% 26.73/27.17 , 'tc_set'( Z ) ) ] )
% 26.73/27.17 , clause( 20141, [ 'c_lessequals'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z
% 26.73/27.17 ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20142, [ =( X, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , clause( 458, [ ~( 'c_lessequals'( X, Y, 'tc_set'( Z ) ) ), =( 'c_union'(
% 26.73/27.17 Y, X, Z ), Y ) ] )
% 26.73/27.17 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20143, [ =( 'c_union'( X, Y, Z ), 'c_union'( 'c_union'( X, Y, Z ),
% 26.73/27.17 'c_union'( Y, X, Z ), Z ) ) ] )
% 26.73/27.17 , clause( 20142, [ =( X, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , 1, clause( 2457, [ 'c_lessequals'( 'c_union'( X, Y, Z ), 'c_union'( Y, X
% 26.73/27.17 , Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, 'c_union'( X, Y, Z ) ), :=( Y, 'c_union'( Y
% 26.73/27.17 , X, Z ) ), :=( Z, Z )] ), substitution( 1, [ :=( X, Y ), :=( Y, X ),
% 26.73/27.17 :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20144, [ =( 'c_union'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z ),
% 26.73/27.17 Z ), 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , clause( 20143, [ =( 'c_union'( X, Y, Z ), 'c_union'( 'c_union'( X, Y, Z )
% 26.73/27.17 , 'c_union'( Y, X, Z ), Z ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 2475, [ =( 'c_union'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z ), Z
% 26.73/27.17 ), 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , clause( 20144, [ =( 'c_union'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z )
% 26.73/27.17 , Z ), 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 eqswap(
% 26.73/27.17 clause( 20145, [ =( Y, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( X, Y,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , clause( 195, [ =( 'c_union'( Y, X, Z ), X ), ~( 'c_lessequals'( Y, X,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20147, [ =( 'c_union'( X, Y, Z ), 'c_union'( 'c_union'( Y, X, Z ),
% 26.73/27.17 'c_union'( X, Y, Z ), Z ) ) ] )
% 26.73/27.17 , clause( 20145, [ =( Y, 'c_union'( X, Y, Z ) ), ~( 'c_lessequals'( X, Y,
% 26.73/27.17 'tc_set'( Z ) ) ) ] )
% 26.73/27.17 , 1, clause( 2457, [ 'c_lessequals'( 'c_union'( X, Y, Z ), 'c_union'( Y, X
% 26.73/27.17 , Z ), 'tc_set'( Z ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [ :=( X, 'c_union'( Y, X, Z ) ), :=( Y, 'c_union'( X
% 26.73/27.17 , Y, Z ) ), :=( Z, Z )] ), substitution( 1, [ :=( X, Y ), :=( Y, X ),
% 26.73/27.17 :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20148, [ =( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z ) ) ] )
% 26.73/27.17 , clause( 2475, [ =( 'c_union'( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z )
% 26.73/27.17 , Z ), 'c_union'( X, Y, Z ) ) ] )
% 26.73/27.17 , 0, clause( 20147, [ =( 'c_union'( X, Y, Z ), 'c_union'( 'c_union'( Y, X,
% 26.73/27.17 Z ), 'c_union'( X, Y, Z ), Z ) ) ] )
% 26.73/27.17 , 0, 5, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 26.73/27.17 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 2477, [ =( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z ) ) ] )
% 26.73/27.17 , clause( 20148, [ =( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 26.73/27.17 permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20150, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Oanalz'( 'c_union'(
% 26.73/27.17 'v_G', 'v_H', 'tc_Message_Omsg' ) ), 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'tc_Message_Omsg' ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 2477, [ =( 'c_union'( X, Y, Z ), 'c_union'( Y, X, Z ) ) ] )
% 26.73/27.17 , 0, clause( 1, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X'
% 26.73/27.17 , 'v_H', 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'c_Message_Oanalz'( 'c_union'( 'v_G',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'tc_Message_Omsg' ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , 0, 7, substitution( 0, [ :=( X, 'c_Message_Osynth'( 'c_Message_Oanalz'(
% 26.73/27.17 'v_G' ) ) ), :=( Y, 'c_Message_Oanalz'( 'c_union'( 'v_G', 'v_H',
% 26.73/27.17 'tc_Message_Omsg' ) ) ), :=( Z, 'tc_Message_Omsg' )] ), substitution( 1
% 26.73/27.17 , [] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20154, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'(
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), 'v_H',
% 26.73/27.17 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 32, [ =( 'c_union'( 'c_Message_Oanalz'( 'c_union'( X, Y,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Osynth'( 'c_Message_Oanalz'( X ) ),
% 26.73/27.17 'tc_Message_Omsg' ), 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( X ) ), Y, 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , 0, clause( 20150, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'(
% 26.73/27.17 'v_X', 'v_H', 'tc_Message_Omsg' ) ), 'c_union'( 'c_Message_Oanalz'(
% 26.73/27.17 'c_union'( 'v_G', 'v_H', 'tc_Message_Omsg' ) ), 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), 'tc_Message_Omsg' ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , 0, 7, substitution( 0, [ :=( X, 'v_G' ), :=( Y, 'v_H' )] ),
% 26.73/27.17 substitution( 1, [] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 2500, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X',
% 26.73/27.17 'v_H', 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'(
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), 'v_H',
% 26.73/27.17 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , clause( 20154, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X'
% 26.73/27.17 , 'v_H', 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'(
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), 'v_H',
% 26.73/27.17 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 paramod(
% 26.73/27.17 clause( 20157, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X', X,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' ) ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , clause( 313, [ =( 'c_insert'( 'v_X', 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' ), 'tc_Message_Omsg'
% 26.73/27.17 ), 'c_union'( 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), X,
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , 0, clause( 115, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( Y, Z,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_insert'( Y, 'c_union'( X, Z
% 26.73/27.17 , 'tc_Message_Omsg' ), 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg'
% 26.73/27.17 ) ) ] )
% 26.73/27.17 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X,
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ) ), :=( Y, 'v_X' ), :=(
% 26.73/27.17 Z, X )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 4758, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X', X,
% 26.73/27.17 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'( 'c_Message_Osynth'(
% 26.73/27.17 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' ) ), 'tc_set'(
% 26.73/27.17 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , clause( 20157, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X', X
% 26.73/27.17 , 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'(
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' )
% 26.73/27.17 ), 'tc_set'( 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 resolution(
% 26.73/27.17 clause( 20158, [] )
% 26.73/27.17 , clause( 2500, [ ~( 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X'
% 26.73/27.17 , 'v_H', 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'(
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), 'v_H',
% 26.73/27.17 'tc_Message_Omsg' ) ), 'tc_set'( 'tc_Message_Omsg' ) ) ) ] )
% 26.73/27.17 , 0, clause( 4758, [ 'c_lessequals'( 'c_Message_Oanalz'( 'c_insert'( 'v_X'
% 26.73/27.17 , X, 'tc_Message_Omsg' ) ), 'c_Message_Oanalz'( 'c_union'(
% 26.73/27.17 'c_Message_Osynth'( 'c_Message_Oanalz'( 'v_G' ) ), X, 'tc_Message_Omsg' )
% 26.73/27.17 ), 'tc_set'( 'tc_Message_Omsg' ) ) ] )
% 26.73/27.17 , 0, substitution( 0, [] ), substitution( 1, [ :=( X, 'v_H' )] )).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 subsumption(
% 26.73/27.17 clause( 20000, [] )
% 26.73/27.17 , clause( 20158, [] )
% 26.73/27.17 , substitution( 0, [] ), permutation( 0, [] ) ).
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 end.
% 26.73/27.17
% 26.73/27.17 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 26.73/27.17
% 26.73/27.17 Memory use:
% 26.73/27.17
% 26.73/27.17 space for terms: 323428
% 26.73/27.17 space for clauses: 1548451
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 clauses generated: 1511137
% 26.73/27.17 clauses kept: 20001
% 26.73/27.17 clauses selected: 5095
% 26.73/27.17 clauses deleted: 1197
% 26.73/27.17 clauses inuse deleted: 213
% 26.73/27.17
% 26.73/27.17 subsentry: 312685
% 26.73/27.17 literals s-matched: 217979
% 26.73/27.17 literals matched: 214986
% 26.73/27.17 full subsumption: 5924
% 26.73/27.17
% 26.73/27.17 checksum: 906395717
% 26.73/27.17
% 26.73/27.17
% 26.73/27.17 Bliksem ended
%------------------------------------------------------------------------------