%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : LAT027-1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.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 : Sun Jul 17 03:48:25 EDT 2022
% Result : Unsatisfiable 1.44s 1.84s
% Output : Refutation 1.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : LAT027-1 : TPTP v8.1.0. Released v2.2.0.
% 0.11/0.13 % Command : bliksem %s
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Wed Jun 29 03:59:46 EDT 2022
% 0.12/0.34 % CPUTime :
% 1.44/1.84 *** allocated 10000 integers for termspace/termends
% 1.44/1.84 *** allocated 10000 integers for clauses
% 1.44/1.84 *** allocated 10000 integers for justifications
% 1.44/1.84 Bliksem 1.12
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 Automatic Strategy Selection
% 1.44/1.84
% 1.44/1.84 Clauses:
% 1.44/1.84 [
% 1.44/1.84 [ =( meet( X, X ), X ) ],
% 1.44/1.84 [ =( join( X, X ), X ) ],
% 1.44/1.84 [ =( meet( X, Y ), meet( Y, X ) ) ],
% 1.44/1.84 [ =( join( X, Y ), join( Y, X ) ) ],
% 1.44/1.84 [ =( meet( meet( join( X, Y ), join( Z, Y ) ), Y ), Y ) ],
% 1.44/1.84 [ =( join( join( meet( X, Y ), meet( Z, Y ) ), Y ), Y ) ],
% 1.44/1.84 [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ],
% 1.44/1.84 [ ~( =( join( join( a, b ), c ), join( a, join( b, c ) ) ) ) ]
% 1.44/1.84 ] .
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 percentage equality = 1.000000, percentage horn = 1.000000
% 1.44/1.84 This is a pure equality problem
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 Options Used:
% 1.44/1.84
% 1.44/1.84 useres = 1
% 1.44/1.84 useparamod = 1
% 1.44/1.84 useeqrefl = 1
% 1.44/1.84 useeqfact = 1
% 1.44/1.84 usefactor = 1
% 1.44/1.84 usesimpsplitting = 0
% 1.44/1.84 usesimpdemod = 5
% 1.44/1.84 usesimpres = 3
% 1.44/1.84
% 1.44/1.84 resimpinuse = 1000
% 1.44/1.84 resimpclauses = 20000
% 1.44/1.84 substype = eqrewr
% 1.44/1.84 backwardsubs = 1
% 1.44/1.84 selectoldest = 5
% 1.44/1.84
% 1.44/1.84 litorderings [0] = split
% 1.44/1.84 litorderings [1] = extend the termordering, first sorting on arguments
% 1.44/1.84
% 1.44/1.84 termordering = kbo
% 1.44/1.84
% 1.44/1.84 litapriori = 0
% 1.44/1.84 termapriori = 1
% 1.44/1.84 litaposteriori = 0
% 1.44/1.84 termaposteriori = 0
% 1.44/1.84 demodaposteriori = 0
% 1.44/1.84 ordereqreflfact = 0
% 1.44/1.84
% 1.44/1.84 litselect = negord
% 1.44/1.84
% 1.44/1.84 maxweight = 15
% 1.44/1.84 maxdepth = 30000
% 1.44/1.84 maxlength = 115
% 1.44/1.84 maxnrvars = 195
% 1.44/1.84 excuselevel = 1
% 1.44/1.84 increasemaxweight = 1
% 1.44/1.84
% 1.44/1.84 maxselected = 10000000
% 1.44/1.84 maxnrclauses = 10000000
% 1.44/1.84
% 1.44/1.84 showgenerated = 0
% 1.44/1.84 showkept = 0
% 1.44/1.84 showselected = 0
% 1.44/1.84 showdeleted = 0
% 1.44/1.84 showresimp = 1
% 1.44/1.84 showstatus = 2000
% 1.44/1.84
% 1.44/1.84 prologoutput = 1
% 1.44/1.84 nrgoals = 5000000
% 1.44/1.84 totalproof = 1
% 1.44/1.84
% 1.44/1.84 Symbols occurring in the translation:
% 1.44/1.84
% 1.44/1.84 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.44/1.84 . [1, 2] (w:1, o:20, a:1, s:1, b:0),
% 1.44/1.84 ! [4, 1] (w:0, o:15, a:1, s:1, b:0),
% 1.44/1.84 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.44/1.84 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.44/1.84 meet [40, 2] (w:1, o:45, a:1, s:1, b:0),
% 1.44/1.84 join [41, 2] (w:1, o:46, a:1, s:1, b:0),
% 1.44/1.84 a [44, 0] (w:1, o:12, a:1, s:1, b:0),
% 1.44/1.84 b [45, 0] (w:1, o:13, a:1, s:1, b:0),
% 1.44/1.84 c [46, 0] (w:1, o:14, a:1, s:1, b:0).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 Starting Search:
% 1.44/1.84
% 1.44/1.84 Resimplifying inuse:
% 1.44/1.84 Done
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 Bliksems!, er is een bewijs:
% 1.44/1.84 % SZS status Unsatisfiable
% 1.44/1.84 % SZS output start Refutation
% 1.44/1.84
% 1.44/1.84 clause( 0, [ =( meet( X, X ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1, [ =( join( X, X ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 2, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 4, [ =( meet( meet( join( X, Y ), join( Z, Y ) ), Y ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 5, [ =( join( join( meet( X, Y ), meet( Z, Y ) ), Y ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 6, [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 7, [ ~( =( join( a, join( b, c ) ), join( join( a, b ), c ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 .
% 1.44/1.84 clause( 9, [ =( meet( Y, join( join( Y, Z ), X ) ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 11, [ =( meet( X, join( X, Y ) ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 12, [ =( meet( X, join( Y, X ) ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 15, [ =( meet( meet( join( Z, Y ), join( Y, X ) ), Y ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 16, [ =( meet( join( X, Y ), Y ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 17, [ =( meet( join( Y, X ), Y ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 18, [ =( join( join( X, meet( Z, join( Y, X ) ) ), join( Y, X ) ),
% 1.44/1.84 join( Y, X ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 21, [ =( join( join( meet( Z, join( X, Y ) ), X ), join( X, Y ) ),
% 1.44/1.84 join( X, Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 30, [ =( join( meet( X, Y ), Y ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 31, [ =( join( X, join( Y, X ) ), join( Y, X ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 34, [ =( meet( Y, meet( X, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 35, [ =( meet( meet( X, Y ), join( Z, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 37, [ =( join( meet( Y, X ), Y ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 38, [ =( join( Y, meet( X, Y ) ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 39, [ =( meet( meet( X, Y ), X ), meet( X, Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 42, [ =( join( X, meet( X, Y ) ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 51, [ ~( =( join( a, join( c, b ) ), join( join( a, b ), c ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 .
% 1.44/1.84 clause( 56, [ =( meet( X, join( join( Y, X ), Z ) ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 60, [ =( meet( meet( X, Y ), join( Y, Z ) ), meet( X, Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 61, [ =( meet( join( join( Y, X ), Z ), X ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 64, [ =( meet( join( X, Z ), meet( Y, X ) ), meet( Y, X ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 71, [ =( join( join( X, Y ), meet( Z, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 80, [ =( join( join( Y, X ), meet( Z, X ) ), join( Y, X ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 82, [ =( join( X, meet( Z, meet( X, Y ) ) ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 100, [ =( join( meet( Y, meet( X, Z ) ), X ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 109, [ =( join( meet( Z, meet( Y, X ) ), X ), X ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 117, [ =( join( meet( meet( X, Y ), Z ), Y ), Y ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 123, [ =( join( meet( X, T ), join( join( Y, X ), Z ) ), join( join(
% 1.44/1.84 Y, X ), Z ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 133, [ =( join( meet( X, T ), join( Y, join( X, Z ) ) ), join( Y,
% 1.44/1.84 join( X, Z ) ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 190, [ =( join( join( Z, X ), join( join( Y, X ), Z ) ), join( join(
% 1.44/1.84 Y, X ), Z ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 194, [ =( join( join( Y, X ), join( X, Y ) ), join( X, Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 243, [ =( meet( meet( Z, join( X, Y ) ), join( Y, X ) ), meet( Z,
% 1.44/1.84 join( X, Y ) ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 249, [ =( meet( join( Z, join( X, Y ) ), join( Y, X ) ), join( X, Y
% 1.44/1.84 ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 255, [ =( meet( join( X, Y ), join( Y, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 257, [ =( join( join( Z, join( Y, X ) ), join( X, Y ) ), join( Z,
% 1.44/1.84 join( Y, X ) ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 261, [ =( join( join( meet( X, Y ), Z ), join( Z, Y ) ), join( Z, Y
% 1.44/1.84 ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 272, [ ~( =( join( join( a, b ), c ), join( join( c, b ), a ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 .
% 1.44/1.84 clause( 273, [ ~( =( join( c, join( a, b ) ), join( join( c, b ), a ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 .
% 1.44/1.84 clause( 275, [ ~( =( join( c, join( b, a ) ), join( join( c, b ), a ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 .
% 1.44/1.84 clause( 976, [ =( join( join( Z, Y ), join( meet( X, Y ), Z ) ), join( Z, Y
% 1.44/1.84 ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 998, [ =( join( join( Z, X ), join( meet( X, Y ), Z ) ), join( Z, X
% 1.44/1.84 ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1003, [ =( join( join( Z, Y ), join( Z, meet( X, Y ) ) ), join( Z,
% 1.44/1.84 Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1026, [ =( join( join( Y, X ), join( meet( Y, Z ), X ) ), join( Y,
% 1.44/1.84 X ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1035, [ =( join( join( join( X, Y ), Z ), join( X, Z ) ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1356, [ =( join( join( X, meet( Z, Y ) ), Y ), join( X, Y ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1370, [ =( join( T, join( Y, Z ) ), join( T, join( Z, Y ) ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1377, [ =( join( join( Z, X ), join( Y, X ) ), join( Z, join( Y, X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1378, [ =( join( join( Z, X ), join( X, Y ) ), join( Z, join( X, Y
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1380, [ =( join( T, join( Z, join( X, Y ) ) ), join( T, join( join(
% 1.44/1.84 Z, Y ), X ) ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1383, [ =( join( X, join( Z, Y ) ), join( join( X, Y ), Z ) ) ] )
% 1.44/1.84 .
% 1.44/1.84 clause( 1413, [] )
% 1.44/1.84 .
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 % SZS output end Refutation
% 1.44/1.84 found a proof!
% 1.44/1.84
% 1.44/1.84 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 1.44/1.84
% 1.44/1.84 initialclauses(
% 1.44/1.84 [ clause( 1415, [ =( meet( X, X ), X ) ] )
% 1.44/1.84 , clause( 1416, [ =( join( X, X ), X ) ] )
% 1.44/1.84 , clause( 1417, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 1.44/1.84 , clause( 1418, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , clause( 1419, [ =( meet( meet( join( X, Y ), join( Z, Y ) ), Y ), Y ) ]
% 1.44/1.84 )
% 1.44/1.84 , clause( 1420, [ =( join( join( meet( X, Y ), meet( Z, Y ) ), Y ), Y ) ]
% 1.44/1.84 )
% 1.44/1.84 , clause( 1421, [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ] )
% 1.44/1.84 , clause( 1422, [ ~( =( join( join( a, b ), c ), join( a, join( b, c ) ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 ] ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 0, [ =( meet( X, X ), X ) ] )
% 1.44/1.84 , clause( 1415, [ =( meet( X, X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 1, [ =( join( X, X ), X ) ] )
% 1.44/1.84 , clause( 1416, [ =( join( X, X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 2, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 1.44/1.84 , clause( 1417, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , clause( 1418, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 4, [ =( meet( meet( join( X, Y ), join( Z, Y ) ), Y ), Y ) ] )
% 1.44/1.84 , clause( 1419, [ =( meet( meet( join( X, Y ), join( Z, Y ) ), Y ), Y ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 5, [ =( join( join( meet( X, Y ), meet( Z, Y ) ), Y ), Y ) ] )
% 1.44/1.84 , clause( 1420, [ =( join( join( meet( X, Y ), meet( Z, Y ) ), Y ), Y ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 6, [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ] )
% 1.44/1.84 , clause( 1421, [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1447, [ ~( =( join( a, join( b, c ) ), join( join( a, b ), c ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 1422, [ ~( =( join( join( a, b ), c ), join( a, join( b, c ) ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 , 0, substitution( 0, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 7, [ ~( =( join( a, join( b, c ) ), join( join( a, b ), c ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , clause( 1447, [ ~( =( join( a, join( b, c ) ), join( join( a, b ), c ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1448, [ =( X, meet( X, join( Y, join( X, Z ) ) ) ) ] )
% 1.44/1.84 , clause( 6, [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1449, [ =( X, meet( X, join( join( X, Z ), Y ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1448, [ =( X, meet( X, join( Y, join( X, Z ) ) ) ) ] )
% 1.44/1.84 , 0, 4, substitution( 0, [ :=( X, Y ), :=( Y, join( X, Z ) )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1453, [ =( meet( X, join( join( X, Y ), Z ) ), X ) ] )
% 1.44/1.84 , clause( 1449, [ =( X, meet( X, join( join( X, Z ), Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 9, [ =( meet( Y, join( join( Y, Z ), X ) ), Y ) ] )
% 1.44/1.84 , clause( 1453, [ =( meet( X, join( join( X, Y ), Z ) ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1458, [ =( X, meet( X, join( Y, join( X, Z ) ) ) ) ] )
% 1.44/1.84 , clause( 6, [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1459, [ =( X, meet( X, join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 1, [ =( join( X, X ), X ) ] )
% 1.44/1.84 , 0, clause( 1458, [ =( X, meet( X, join( Y, join( X, Z ) ) ) ) ] )
% 1.44/1.84 , 0, 4, substitution( 0, [ :=( X, join( X, Y ) )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, join( X, Y ) ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1461, [ =( meet( X, join( X, Y ) ), X ) ] )
% 1.44/1.84 , clause( 1459, [ =( X, meet( X, join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 11, [ =( meet( X, join( X, Y ) ), X ) ] )
% 1.44/1.84 , clause( 1461, [ =( meet( X, join( X, Y ) ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1464, [ =( X, meet( X, join( Y, join( X, Z ) ) ) ) ] )
% 1.44/1.84 , clause( 6, [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1466, [ =( X, meet( X, join( Y, X ) ) ) ] )
% 1.44/1.84 , clause( 1, [ =( join( X, X ), X ) ] )
% 1.44/1.84 , 0, clause( 1464, [ =( X, meet( X, join( Y, join( X, Z ) ) ) ) ] )
% 1.44/1.84 , 0, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.44/1.84 :=( Y, Y ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1468, [ =( meet( X, join( Y, X ) ), X ) ] )
% 1.44/1.84 , clause( 1466, [ =( X, meet( X, join( Y, X ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 12, [ =( meet( X, join( Y, X ) ), X ) ] )
% 1.44/1.84 , clause( 1468, [ =( meet( X, join( Y, X ) ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1469, [ =( Y, meet( meet( join( X, Y ), join( Z, Y ) ), Y ) ) ] )
% 1.44/1.84 , clause( 4, [ =( meet( meet( join( X, Y ), join( Z, Y ) ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1471, [ =( X, meet( meet( join( Y, X ), join( X, Z ) ), X ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1469, [ =( Y, meet( meet( join( X, Y ), join( Z, Y ) ), Y ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 7, substitution( 0, [ :=( X, Z ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1477, [ =( meet( meet( join( Y, X ), join( X, Z ) ), X ), X ) ] )
% 1.44/1.84 , clause( 1471, [ =( X, meet( meet( join( Y, X ), join( X, Z ) ), X ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 15, [ =( meet( meet( join( Z, Y ), join( Y, X ) ), Y ), Y ) ] )
% 1.44/1.84 , clause( 1477, [ =( meet( meet( join( Y, X ), join( X, Z ) ), X ), X ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1479, [ =( Y, meet( meet( join( X, Y ), join( Z, Y ) ), Y ) ) ] )
% 1.44/1.84 , clause( 4, [ =( meet( meet( join( X, Y ), join( Z, Y ) ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1480, [ =( X, meet( join( Y, X ), X ) ) ] )
% 1.44/1.84 , clause( 0, [ =( meet( X, X ), X ) ] )
% 1.44/1.84 , 0, clause( 1479, [ =( Y, meet( meet( join( X, Y ), join( Z, Y ) ), Y ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 3, substitution( 0, [ :=( X, join( Y, X ) )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, X ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1481, [ =( meet( join( Y, X ), X ), X ) ] )
% 1.44/1.84 , clause( 1480, [ =( X, meet( join( Y, X ), X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 16, [ =( meet( join( X, Y ), Y ), Y ) ] )
% 1.44/1.84 , clause( 1481, [ =( meet( join( Y, X ), X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1482, [ =( Y, meet( join( X, Y ), Y ) ) ] )
% 1.44/1.84 , clause( 16, [ =( meet( join( X, Y ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1483, [ =( X, meet( join( X, Y ), X ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1482, [ =( Y, meet( join( X, Y ), Y ) ) ] )
% 1.44/1.84 , 0, 3, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1486, [ =( meet( join( X, Y ), X ), X ) ] )
% 1.44/1.84 , clause( 1483, [ =( X, meet( join( X, Y ), X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 17, [ =( meet( join( Y, X ), Y ), Y ) ] )
% 1.44/1.84 , clause( 1486, [ =( meet( join( X, Y ), X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1488, [ =( Y, join( join( meet( X, Y ), meet( Z, Y ) ), Y ) ) ] )
% 1.44/1.84 , clause( 5, [ =( join( join( meet( X, Y ), meet( Z, Y ) ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1491, [ =( join( X, Y ), join( join( Y, meet( Z, join( X, Y ) ) ),
% 1.44/1.84 join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 12, [ =( meet( X, join( Y, X ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1488, [ =( Y, join( join( meet( X, Y ), meet( Z, Y ) ), Y ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, join( X, Y ) ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1493, [ =( join( join( Y, meet( Z, join( X, Y ) ) ), join( X, Y ) )
% 1.44/1.84 , join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1491, [ =( join( X, Y ), join( join( Y, meet( Z, join( X, Y ) ) )
% 1.44/1.84 , join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 18, [ =( join( join( X, meet( Z, join( Y, X ) ) ), join( Y, X ) ),
% 1.44/1.84 join( Y, X ) ) ] )
% 1.44/1.84 , clause( 1493, [ =( join( join( Y, meet( Z, join( X, Y ) ) ), join( X, Y )
% 1.44/1.84 ), join( X, Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1496, [ =( Y, join( join( meet( X, Y ), meet( Z, Y ) ), Y ) ) ] )
% 1.44/1.84 , clause( 5, [ =( join( join( meet( X, Y ), meet( Z, Y ) ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1500, [ =( join( X, Y ), join( join( meet( Z, join( X, Y ) ), X ),
% 1.44/1.84 join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 11, [ =( meet( X, join( X, Y ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1496, [ =( Y, join( join( meet( X, Y ), meet( Z, Y ) ), Y ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 11, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, Z ), :=( Y, join( X, Y ) ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1502, [ =( join( join( meet( Z, join( X, Y ) ), X ), join( X, Y ) )
% 1.44/1.84 , join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1500, [ =( join( X, Y ), join( join( meet( Z, join( X, Y ) ), X )
% 1.44/1.84 , join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 21, [ =( join( join( meet( Z, join( X, Y ) ), X ), join( X, Y ) ),
% 1.44/1.84 join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1502, [ =( join( join( meet( Z, join( X, Y ) ), X ), join( X, Y )
% 1.44/1.84 ), join( X, Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1504, [ =( Y, join( join( meet( X, Y ), meet( Z, Y ) ), Y ) ) ] )
% 1.44/1.84 , clause( 5, [ =( join( join( meet( X, Y ), meet( Z, Y ) ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1505, [ =( X, join( meet( Y, X ), X ) ) ] )
% 1.44/1.84 , clause( 1, [ =( join( X, X ), X ) ] )
% 1.44/1.84 , 0, clause( 1504, [ =( Y, join( join( meet( X, Y ), meet( Z, Y ) ), Y ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 3, substitution( 0, [ :=( X, meet( Y, X ) )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, X ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1506, [ =( join( meet( Y, X ), X ), X ) ] )
% 1.44/1.84 , clause( 1505, [ =( X, join( meet( Y, X ), X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 30, [ =( join( meet( X, Y ), Y ), Y ) ] )
% 1.44/1.84 , clause( 1506, [ =( join( meet( Y, X ), X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1508, [ =( Y, join( meet( X, Y ), Y ) ) ] )
% 1.44/1.84 , clause( 30, [ =( join( meet( X, Y ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1511, [ =( join( X, Y ), join( Y, join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 12, [ =( meet( X, join( Y, X ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1508, [ =( Y, join( meet( X, Y ), Y ) ) ] )
% 1.44/1.84 , 0, 5, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, join( X, Y ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1512, [ =( join( Y, join( X, Y ) ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1511, [ =( join( X, Y ), join( Y, join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 31, [ =( join( X, join( Y, X ) ), join( Y, X ) ) ] )
% 1.44/1.84 , clause( 1512, [ =( join( Y, join( X, Y ) ), join( X, Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1514, [ =( X, meet( join( X, Y ), X ) ) ] )
% 1.44/1.84 , clause( 17, [ =( meet( join( Y, X ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1517, [ =( meet( X, Y ), meet( Y, meet( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 30, [ =( join( meet( X, Y ), Y ), Y ) ] )
% 1.44/1.84 , 0, clause( 1514, [ =( X, meet( join( X, Y ), X ) ) ] )
% 1.44/1.84 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, meet( X, Y ) ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1518, [ =( meet( Y, meet( X, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , clause( 1517, [ =( meet( X, Y ), meet( Y, meet( X, Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 34, [ =( meet( Y, meet( X, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , clause( 1518, [ =( meet( Y, meet( X, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1520, [ =( X, meet( X, join( Y, join( X, Z ) ) ) ) ] )
% 1.44/1.84 , clause( 6, [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1524, [ =( meet( X, Y ), meet( meet( X, Y ), join( Z, Y ) ) ) ] )
% 1.44/1.84 , clause( 30, [ =( join( meet( X, Y ), Y ), Y ) ] )
% 1.44/1.84 , 0, clause( 1520, [ =( X, meet( X, join( Y, join( X, Z ) ) ) ) ] )
% 1.44/1.84 , 0, 10, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, meet( X, Y ) ), :=( Y, Z ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1526, [ =( meet( meet( X, Y ), join( Z, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , clause( 1524, [ =( meet( X, Y ), meet( meet( X, Y ), join( Z, Y ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 35, [ =( meet( meet( X, Y ), join( Z, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , clause( 1526, [ =( meet( meet( X, Y ), join( Z, Y ) ), meet( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1527, [ =( Y, join( meet( X, Y ), Y ) ) ] )
% 1.44/1.84 , clause( 30, [ =( join( meet( X, Y ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1528, [ =( X, join( meet( X, Y ), X ) ) ] )
% 1.44/1.84 , clause( 2, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1527, [ =( Y, join( meet( X, Y ), Y ) ) ] )
% 1.44/1.84 , 0, 3, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1531, [ =( join( meet( X, Y ), X ), X ) ] )
% 1.44/1.84 , clause( 1528, [ =( X, join( meet( X, Y ), X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 37, [ =( join( meet( Y, X ), Y ), Y ) ] )
% 1.44/1.84 , clause( 1531, [ =( join( meet( X, Y ), X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1532, [ =( Y, join( meet( X, Y ), Y ) ) ] )
% 1.44/1.84 , clause( 30, [ =( join( meet( X, Y ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1533, [ =( X, join( X, meet( Y, X ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1532, [ =( Y, join( meet( X, Y ), Y ) ) ] )
% 1.44/1.84 , 0, 2, substitution( 0, [ :=( X, meet( Y, X ) ), :=( Y, X )] ),
% 1.44/1.84 substitution( 1, [ :=( X, Y ), :=( Y, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1536, [ =( join( X, meet( Y, X ) ), X ) ] )
% 1.44/1.84 , clause( 1533, [ =( X, join( X, meet( Y, X ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 38, [ =( join( Y, meet( X, Y ) ), Y ) ] )
% 1.44/1.84 , clause( 1536, [ =( join( X, meet( Y, X ) ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1538, [ =( X, meet( X, join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 11, [ =( meet( X, join( X, Y ) ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1541, [ =( meet( X, Y ), meet( meet( X, Y ), X ) ) ] )
% 1.44/1.84 , clause( 37, [ =( join( meet( Y, X ), Y ), Y ) ] )
% 1.44/1.84 , 0, clause( 1538, [ =( X, meet( X, join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, 8, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, meet( X, Y ) ), :=( Y, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1542, [ =( meet( meet( X, Y ), X ), meet( X, Y ) ) ] )
% 1.44/1.84 , clause( 1541, [ =( meet( X, Y ), meet( meet( X, Y ), X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 39, [ =( meet( meet( X, Y ), X ), meet( X, Y ) ) ] )
% 1.44/1.84 , clause( 1542, [ =( meet( meet( X, Y ), X ), meet( X, Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1543, [ =( X, join( meet( X, Y ), X ) ) ] )
% 1.44/1.84 , clause( 37, [ =( join( meet( Y, X ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1544, [ =( X, join( X, meet( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1543, [ =( X, join( meet( X, Y ), X ) ) ] )
% 1.44/1.84 , 0, 2, substitution( 0, [ :=( X, meet( X, Y ) ), :=( Y, X )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1547, [ =( join( X, meet( X, Y ) ), X ) ] )
% 1.44/1.84 , clause( 1544, [ =( X, join( X, meet( X, Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 42, [ =( join( X, meet( X, Y ) ), X ) ] )
% 1.44/1.84 , clause( 1547, [ =( join( X, meet( X, Y ) ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1548, [ ~( =( join( join( a, b ), c ), join( a, join( b, c ) ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 7, [ ~( =( join( a, join( b, c ) ), join( join( a, b ), c ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1552, [ ~( =( join( join( a, b ), c ), join( a, join( c, b ) ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1548, [ ~( =( join( join( a, b ), c ), join( a, join( b, c ) )
% 1.44/1.84 ) ) ] )
% 1.44/1.84 , 0, 9, substitution( 0, [ :=( X, b ), :=( Y, c )] ), substitution( 1, [] )
% 1.44/1.84 ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1580, [ ~( =( join( a, join( c, b ) ), join( join( a, b ), c ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 1552, [ ~( =( join( join( a, b ), c ), join( a, join( c, b ) ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 , 0, substitution( 0, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 51, [ ~( =( join( a, join( c, b ) ), join( join( a, b ), c ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , clause( 1580, [ ~( =( join( a, join( c, b ) ), join( join( a, b ), c ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1582, [ =( X, meet( X, join( join( X, Y ), Z ) ) ) ] )
% 1.44/1.84 , clause( 9, [ =( meet( Y, join( join( Y, Z ), X ) ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1584, [ =( X, meet( X, join( join( Y, X ), Z ) ) ) ] )
% 1.44/1.84 , clause( 31, [ =( join( X, join( Y, X ) ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1582, [ =( X, meet( X, join( join( X, Y ), Z ) ) ) ] )
% 1.44/1.84 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, join( Y, X ) ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1586, [ =( meet( X, join( join( Y, X ), Z ) ), X ) ] )
% 1.44/1.84 , clause( 1584, [ =( X, meet( X, join( join( Y, X ), Z ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 56, [ =( meet( X, join( join( Y, X ), Z ) ), X ) ] )
% 1.44/1.84 , clause( 1586, [ =( meet( X, join( join( Y, X ), Z ) ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1588, [ =( X, meet( X, join( join( X, Y ), Z ) ) ) ] )
% 1.44/1.84 , clause( 9, [ =( meet( Y, join( join( Y, Z ), X ) ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1591, [ =( meet( X, Y ), meet( meet( X, Y ), join( Y, Z ) ) ) ] )
% 1.44/1.84 , clause( 30, [ =( join( meet( X, Y ), Y ), Y ) ] )
% 1.44/1.84 , 0, clause( 1588, [ =( X, meet( X, join( join( X, Y ), Z ) ) ) ] )
% 1.44/1.84 , 0, 9, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, meet( X, Y ) ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1592, [ =( meet( meet( X, Y ), join( Y, Z ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , clause( 1591, [ =( meet( X, Y ), meet( meet( X, Y ), join( Y, Z ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 60, [ =( meet( meet( X, Y ), join( Y, Z ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , clause( 1592, [ =( meet( meet( X, Y ), join( Y, Z ) ), meet( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1594, [ =( meet( Y, X ), meet( X, meet( Y, X ) ) ) ] )
% 1.44/1.84 , clause( 34, [ =( meet( Y, meet( X, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1596, [ =( meet( X, join( join( Y, X ), Z ) ), meet( join( join( Y
% 1.44/1.84 , X ), Z ), X ) ) ] )
% 1.44/1.84 , clause( 56, [ =( meet( X, join( join( Y, X ), Z ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1594, [ =( meet( Y, X ), meet( X, meet( Y, X ) ) ) ] )
% 1.44/1.84 , 0, 14, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 substitution( 1, [ :=( X, join( join( Y, X ), Z ) ), :=( Y, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1597, [ =( X, meet( join( join( Y, X ), Z ), X ) ) ] )
% 1.44/1.84 , clause( 56, [ =( meet( X, join( join( Y, X ), Z ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1596, [ =( meet( X, join( join( Y, X ), Z ) ), meet( join(
% 1.44/1.84 join( Y, X ), Z ), X ) ) ] )
% 1.44/1.84 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1599, [ =( meet( join( join( Y, X ), Z ), X ), X ) ] )
% 1.44/1.84 , clause( 1597, [ =( X, meet( join( join( Y, X ), Z ), X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 61, [ =( meet( join( join( Y, X ), Z ), X ), X ) ] )
% 1.44/1.84 , clause( 1599, [ =( meet( join( join( Y, X ), Z ), X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1602, [ =( Y, meet( join( join( X, Y ), Z ), Y ) ) ] )
% 1.44/1.84 , clause( 61, [ =( meet( join( join( Y, X ), Z ), X ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1606, [ =( meet( X, Y ), meet( join( Y, Z ), meet( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 38, [ =( join( Y, meet( X, Y ) ), Y ) ] )
% 1.44/1.84 , 0, clause( 1602, [ =( Y, meet( join( join( X, Y ), Z ), Y ) ) ] )
% 1.44/1.84 , 0, 6, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, meet( X, Y ) ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1608, [ =( meet( join( Y, Z ), meet( X, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , clause( 1606, [ =( meet( X, Y ), meet( join( Y, Z ), meet( X, Y ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 64, [ =( meet( join( X, Z ), meet( Y, X ) ), meet( Y, X ) ) ] )
% 1.44/1.84 , clause( 1608, [ =( meet( join( Y, Z ), meet( X, Y ) ), meet( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1610, [ =( X, join( X, meet( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 42, [ =( join( X, meet( X, Y ) ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1613, [ =( join( X, Y ), join( join( X, Y ), meet( Z, X ) ) ) ] )
% 1.44/1.84 , clause( 64, [ =( meet( join( X, Z ), meet( Y, X ) ), meet( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1610, [ =( X, join( X, meet( X, Y ) ) ) ] )
% 1.44/1.84 , 0, 8, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 1.44/1.84 substitution( 1, [ :=( X, join( X, Y ) ), :=( Y, meet( Z, X ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1614, [ =( join( join( X, Y ), meet( Z, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1613, [ =( join( X, Y ), join( join( X, Y ), meet( Z, X ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 71, [ =( join( join( X, Y ), meet( Z, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1614, [ =( join( join( X, Y ), meet( Z, X ) ), join( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1616, [ =( join( X, Y ), join( join( X, Y ), meet( Z, X ) ) ) ] )
% 1.44/1.84 , clause( 71, [ =( join( join( X, Y ), meet( Z, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1624, [ =( join( X, join( Y, X ) ), join( join( Y, X ), meet( Z, X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 31, [ =( join( X, join( Y, X ) ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1616, [ =( join( X, Y ), join( join( X, Y ), meet( Z, X ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 7, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, join( Y, X ) ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1625, [ =( join( Y, X ), join( join( Y, X ), meet( Z, X ) ) ) ] )
% 1.44/1.84 , clause( 31, [ =( join( X, join( Y, X ) ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1624, [ =( join( X, join( Y, X ) ), join( join( Y, X ), meet(
% 1.44/1.84 Z, X ) ) ) ] )
% 1.44/1.84 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1627, [ =( join( join( X, Y ), meet( Z, Y ) ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1625, [ =( join( Y, X ), join( join( Y, X ), meet( Z, X ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 80, [ =( join( join( Y, X ), meet( Z, X ) ), join( Y, X ) ) ] )
% 1.44/1.84 , clause( 1627, [ =( join( join( X, Y ), meet( Z, Y ) ), join( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1630, [ =( join( X, Y ), join( join( X, Y ), meet( Z, X ) ) ) ] )
% 1.44/1.84 , clause( 71, [ =( join( join( X, Y ), meet( Z, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1632, [ =( join( meet( X, Y ), X ), join( X, meet( Z, meet( X, Y )
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 37, [ =( join( meet( Y, X ), Y ), Y ) ] )
% 1.44/1.84 , 0, clause( 1630, [ =( join( X, Y ), join( join( X, Y ), meet( Z, X ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 7, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, meet( X, Y ) ), :=( Y, X ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1633, [ =( X, join( X, meet( Z, meet( X, Y ) ) ) ) ] )
% 1.44/1.84 , clause( 37, [ =( join( meet( Y, X ), Y ), Y ) ] )
% 1.44/1.84 , 0, clause( 1632, [ =( join( meet( X, Y ), X ), join( X, meet( Z, meet( X
% 1.44/1.84 , Y ) ) ) ) ] )
% 1.44/1.84 , 0, 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1635, [ =( join( X, meet( Y, meet( X, Z ) ) ), X ) ] )
% 1.44/1.84 , clause( 1633, [ =( X, join( X, meet( Z, meet( X, Y ) ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 82, [ =( join( X, meet( Z, meet( X, Y ) ) ), X ) ] )
% 1.44/1.84 , clause( 1635, [ =( join( X, meet( Y, meet( X, Z ) ) ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1638, [ =( join( Y, X ), join( X, join( Y, X ) ) ) ] )
% 1.44/1.84 , clause( 31, [ =( join( X, join( Y, X ) ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1640, [ =( join( X, meet( Y, meet( X, Z ) ) ), join( meet( Y, meet(
% 1.44/1.84 X, Z ) ), X ) ) ] )
% 1.44/1.84 , clause( 82, [ =( join( X, meet( Z, meet( X, Y ) ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1638, [ =( join( Y, X ), join( X, join( Y, X ) ) ) ] )
% 1.44/1.84 , 0, 14, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 1.44/1.84 substitution( 1, [ :=( X, meet( Y, meet( X, Z ) ) ), :=( Y, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1641, [ =( X, join( meet( Y, meet( X, Z ) ), X ) ) ] )
% 1.44/1.84 , clause( 82, [ =( join( X, meet( Z, meet( X, Y ) ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1640, [ =( join( X, meet( Y, meet( X, Z ) ) ), join( meet( Y,
% 1.44/1.84 meet( X, Z ) ), X ) ) ] )
% 1.44/1.84 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1643, [ =( join( meet( Y, meet( X, Z ) ), X ), X ) ] )
% 1.44/1.84 , clause( 1641, [ =( X, join( meet( Y, meet( X, Z ) ), X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 100, [ =( join( meet( Y, meet( X, Z ) ), X ), X ) ] )
% 1.44/1.84 , clause( 1643, [ =( join( meet( Y, meet( X, Z ) ), X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1646, [ =( Y, join( meet( X, meet( Y, Z ) ), Y ) ) ] )
% 1.44/1.84 , clause( 100, [ =( join( meet( Y, meet( X, Z ) ), X ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1648, [ =( X, join( meet( Y, meet( Z, X ) ), X ) ) ] )
% 1.44/1.84 , clause( 34, [ =( meet( Y, meet( X, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , 0, clause( 1646, [ =( Y, join( meet( X, meet( Y, Z ) ), Y ) ) ] )
% 1.44/1.84 , 0, 5, substitution( 0, [ :=( X, Z ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, X ), :=( Z, meet( Z, X ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1650, [ =( join( meet( Y, meet( Z, X ) ), X ), X ) ] )
% 1.44/1.84 , clause( 1648, [ =( X, join( meet( Y, meet( Z, X ) ), X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 109, [ =( join( meet( Z, meet( Y, X ) ), X ), X ) ] )
% 1.44/1.84 , clause( 1650, [ =( join( meet( Y, meet( Z, X ) ), X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1652, [ =( Z, join( meet( X, meet( Y, Z ) ), Z ) ) ] )
% 1.44/1.84 , clause( 109, [ =( join( meet( Z, meet( Y, X ) ), X ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1653, [ =( X, join( meet( meet( Y, X ), Z ), X ) ) ] )
% 1.44/1.84 , clause( 39, [ =( meet( meet( X, Y ), X ), meet( X, Y ) ) ] )
% 1.44/1.84 , 0, clause( 1652, [ =( Z, join( meet( X, meet( Y, Z ) ), Z ) ) ] )
% 1.44/1.84 , 0, 3, substitution( 0, [ :=( X, meet( Y, X ) ), :=( Y, Z )] ),
% 1.44/1.84 substitution( 1, [ :=( X, meet( meet( Y, X ), Z ) ), :=( Y, Y ), :=( Z, X
% 1.44/1.84 )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1655, [ =( join( meet( meet( Y, X ), Z ), X ), X ) ] )
% 1.44/1.84 , clause( 1653, [ =( X, join( meet( meet( Y, X ), Z ), X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 117, [ =( join( meet( meet( X, Y ), Z ), Y ), Y ) ] )
% 1.44/1.84 , clause( 1655, [ =( join( meet( meet( Y, X ), Z ), X ), X ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1658, [ =( Y, join( meet( meet( X, Y ), Z ), Y ) ) ] )
% 1.44/1.84 , clause( 117, [ =( join( meet( meet( X, Y ), Z ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1662, [ =( join( join( X, Y ), Z ), join( meet( Y, T ), join( join(
% 1.44/1.84 X, Y ), Z ) ) ) ] )
% 1.44/1.84 , clause( 56, [ =( meet( X, join( join( Y, X ), Z ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1658, [ =( Y, join( meet( meet( X, Y ), Z ), Y ) ) ] )
% 1.44/1.84 , 0, 8, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 1.44/1.84 substitution( 1, [ :=( X, Y ), :=( Y, join( join( X, Y ), Z ) ), :=( Z, T
% 1.44/1.84 )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1664, [ =( join( meet( Y, T ), join( join( X, Y ), Z ) ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ] )
% 1.44/1.84 , clause( 1662, [ =( join( join( X, Y ), Z ), join( meet( Y, T ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] )
% 1.44/1.84 ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 123, [ =( join( meet( X, T ), join( join( Y, X ), Z ) ), join( join(
% 1.44/1.84 Y, X ), Z ) ) ] )
% 1.44/1.84 , clause( 1664, [ =( join( meet( Y, T ), join( join( X, Y ), Z ) ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z ), :=( T, T )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1666, [ =( Y, join( meet( meet( X, Y ), Z ), Y ) ) ] )
% 1.44/1.84 , clause( 117, [ =( join( meet( meet( X, Y ), Z ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1672, [ =( join( X, join( Y, Z ) ), join( meet( Y, T ), join( X,
% 1.44/1.84 join( Y, Z ) ) ) ) ] )
% 1.44/1.84 , clause( 6, [ =( meet( X, join( Y, join( X, Z ) ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1666, [ =( Y, join( meet( meet( X, Y ), Z ), Y ) ) ] )
% 1.44/1.84 , 0, 8, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 1.44/1.84 substitution( 1, [ :=( X, Y ), :=( Y, join( X, join( Y, Z ) ) ), :=( Z, T
% 1.44/1.84 )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1674, [ =( join( meet( Y, T ), join( X, join( Y, Z ) ) ), join( X,
% 1.44/1.84 join( Y, Z ) ) ) ] )
% 1.44/1.84 , clause( 1672, [ =( join( X, join( Y, Z ) ), join( meet( Y, T ), join( X,
% 1.44/1.84 join( Y, Z ) ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] )
% 1.44/1.84 ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 133, [ =( join( meet( X, T ), join( Y, join( X, Z ) ) ), join( Y,
% 1.44/1.84 join( X, Z ) ) ) ] )
% 1.44/1.84 , clause( 1674, [ =( join( meet( Y, T ), join( X, join( Y, Z ) ) ), join( X
% 1.44/1.84 , join( Y, Z ) ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z ), :=( T, T )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1676, [ =( join( Z, X ), join( join( X, meet( Y, join( Z, X ) ) ),
% 1.44/1.84 join( Z, X ) ) ) ] )
% 1.44/1.84 , clause( 18, [ =( join( join( X, meet( Z, join( Y, X ) ) ), join( Y, X ) )
% 1.44/1.84 , join( Y, X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1681, [ =( join( join( X, Y ), Z ), join( join( Z, Y ), join( join(
% 1.44/1.84 X, Y ), Z ) ) ) ] )
% 1.44/1.84 , clause( 56, [ =( meet( X, join( join( Y, X ), Z ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1676, [ =( join( Z, X ), join( join( X, meet( Y, join( Z, X )
% 1.44/1.84 ) ), join( Z, X ) ) ) ] )
% 1.44/1.84 , 0, 9, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 1.44/1.84 substitution( 1, [ :=( X, Z ), :=( Y, Y ), :=( Z, join( X, Y ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1682, [ =( join( join( Z, Y ), join( join( X, Y ), Z ) ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ] )
% 1.44/1.84 , clause( 1681, [ =( join( join( X, Y ), Z ), join( join( Z, Y ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 190, [ =( join( join( Z, X ), join( join( Y, X ), Z ) ), join( join(
% 1.44/1.84 Y, X ), Z ) ) ] )
% 1.44/1.84 , clause( 1682, [ =( join( join( Z, Y ), join( join( X, Y ), Z ) ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1684, [ =( join( Z, X ), join( join( X, meet( Y, join( Z, X ) ) ),
% 1.44/1.84 join( Z, X ) ) ) ] )
% 1.44/1.84 , clause( 18, [ =( join( join( X, meet( Z, join( Y, X ) ) ), join( Y, X ) )
% 1.44/1.84 , join( Y, X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1687, [ =( join( X, Y ), join( join( Y, X ), join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 11, [ =( meet( X, join( X, Y ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1684, [ =( join( Z, X ), join( join( X, meet( Y, join( Z, X )
% 1.44/1.84 ) ), join( Z, X ) ) ) ] )
% 1.44/1.84 , 0, 7, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, Y ), :=( Y, X ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1688, [ =( join( join( Y, X ), join( X, Y ) ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1687, [ =( join( X, Y ), join( join( Y, X ), join( X, Y ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 194, [ =( join( join( Y, X ), join( X, Y ) ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1688, [ =( join( join( Y, X ), join( X, Y ) ), join( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1690, [ =( meet( X, Y ), meet( meet( X, Y ), join( Y, Z ) ) ) ] )
% 1.44/1.84 , clause( 60, [ =( meet( meet( X, Y ), join( Y, Z ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1691, [ =( meet( X, join( Y, Z ) ), meet( meet( X, join( Y, Z ) ),
% 1.44/1.84 join( Z, Y ) ) ) ] )
% 1.44/1.84 , clause( 194, [ =( join( join( Y, X ), join( X, Y ) ), join( X, Y ) ) ] )
% 1.44/1.84 , 0, clause( 1690, [ =( meet( X, Y ), meet( meet( X, Y ), join( Y, Z ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 12, substitution( 0, [ :=( X, Z ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, join( Y, Z ) ), :=( Z, join( Z, Y ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1692, [ =( meet( meet( X, join( Y, Z ) ), join( Z, Y ) ), meet( X,
% 1.44/1.84 join( Y, Z ) ) ) ] )
% 1.44/1.84 , clause( 1691, [ =( meet( X, join( Y, Z ) ), meet( meet( X, join( Y, Z ) )
% 1.44/1.84 , join( Z, Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 243, [ =( meet( meet( Z, join( X, Y ) ), join( Y, X ) ), meet( Z,
% 1.44/1.84 join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 1692, [ =( meet( meet( X, join( Y, Z ) ), join( Z, Y ) ), meet( X
% 1.44/1.84 , join( Y, Z ) ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1694, [ =( Y, meet( meet( join( X, Y ), join( Y, Z ) ), Y ) ) ] )
% 1.44/1.84 , clause( 15, [ =( meet( meet( join( Z, Y ), join( Y, X ) ), Y ), Y ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1697, [ =( join( X, Y ), meet( meet( join( Z, join( X, Y ) ), join(
% 1.44/1.84 Y, X ) ), join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 194, [ =( join( join( Y, X ), join( X, Y ) ), join( X, Y ) ) ] )
% 1.44/1.84 , 0, clause( 1694, [ =( Y, meet( meet( join( X, Y ), join( Y, Z ) ), Y ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 11, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, Z ), :=( Y, join( X, Y ) ), :=( Z, join( Y, X ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1698, [ =( join( X, Y ), meet( join( Z, join( X, Y ) ), join( Y, X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 243, [ =( meet( meet( Z, join( X, Y ) ), join( Y, X ) ), meet( Z
% 1.44/1.84 , join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, clause( 1697, [ =( join( X, Y ), meet( meet( join( Z, join( X, Y ) ),
% 1.44/1.84 join( Y, X ) ), join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, 4, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, join( Z, join( X
% 1.44/1.84 , Y ) ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )
% 1.44/1.84 ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1699, [ =( meet( join( Z, join( X, Y ) ), join( Y, X ) ), join( X,
% 1.44/1.84 Y ) ) ] )
% 1.44/1.84 , clause( 1698, [ =( join( X, Y ), meet( join( Z, join( X, Y ) ), join( Y,
% 1.44/1.84 X ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 249, [ =( meet( join( Z, join( X, Y ) ), join( Y, X ) ), join( X, Y
% 1.44/1.84 ) ) ] )
% 1.44/1.84 , clause( 1699, [ =( meet( join( Z, join( X, Y ) ), join( Y, X ) ), join( X
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1701, [ =( X, meet( X, join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 11, [ =( meet( X, join( X, Y ) ), X ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1702, [ =( join( X, Y ), meet( join( X, Y ), join( Y, X ) ) ) ] )
% 1.44/1.84 , clause( 194, [ =( join( join( Y, X ), join( X, Y ) ), join( X, Y ) ) ] )
% 1.44/1.84 , 0, clause( 1701, [ =( X, meet( X, join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, 8, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, join( X, Y ) ), :=( Y, join( Y, X ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1703, [ =( meet( join( X, Y ), join( Y, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1702, [ =( join( X, Y ), meet( join( X, Y ), join( Y, X ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 255, [ =( meet( join( X, Y ), join( Y, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1703, [ =( meet( join( X, Y ), join( Y, X ) ), join( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.44/1.84 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1705, [ =( join( X, Y ), join( join( X, Y ), meet( Z, Y ) ) ) ] )
% 1.44/1.84 , clause( 80, [ =( join( join( Y, X ), meet( Z, X ) ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1714, [ =( join( X, join( Y, Z ) ), join( join( X, join( Y, Z ) ),
% 1.44/1.84 join( Z, Y ) ) ) ] )
% 1.44/1.84 , clause( 255, [ =( meet( join( X, Y ), join( Y, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 , 0, clause( 1705, [ =( join( X, Y ), join( join( X, Y ), meet( Z, Y ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 12, substitution( 0, [ :=( X, Z ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, join( Y, Z ) ), :=( Z, join( Z, Y ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1715, [ =( join( join( X, join( Y, Z ) ), join( Z, Y ) ), join( X,
% 1.44/1.84 join( Y, Z ) ) ) ] )
% 1.44/1.84 , clause( 1714, [ =( join( X, join( Y, Z ) ), join( join( X, join( Y, Z ) )
% 1.44/1.84 , join( Z, Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 257, [ =( join( join( Z, join( Y, X ) ), join( X, Y ) ), join( Z,
% 1.44/1.84 join( Y, X ) ) ) ] )
% 1.44/1.84 , clause( 1715, [ =( join( join( X, join( Y, Z ) ), join( Z, Y ) ), join( X
% 1.44/1.84 , join( Y, Z ) ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1717, [ =( join( Y, Z ), join( join( meet( X, join( Y, Z ) ), Y ),
% 1.44/1.84 join( Y, Z ) ) ) ] )
% 1.44/1.84 , clause( 21, [ =( join( join( meet( Z, join( X, Y ) ), X ), join( X, Y ) )
% 1.44/1.84 , join( X, Y ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1720, [ =( join( X, Y ), join( join( meet( Z, Y ), X ), join( X, Y
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 35, [ =( meet( meet( X, Y ), join( Z, Y ) ), meet( X, Y ) ) ] )
% 1.44/1.84 , 0, clause( 1717, [ =( join( Y, Z ), join( join( meet( X, join( Y, Z ) ),
% 1.44/1.84 Y ), join( Y, Z ) ) ) ] )
% 1.44/1.84 , 0, 6, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.44/1.84 substitution( 1, [ :=( X, meet( Z, Y ) ), :=( Y, X ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1721, [ =( join( join( meet( Z, Y ), X ), join( X, Y ) ), join( X,
% 1.44/1.84 Y ) ) ] )
% 1.44/1.84 , clause( 1720, [ =( join( X, Y ), join( join( meet( Z, Y ), X ), join( X,
% 1.44/1.84 Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 261, [ =( join( join( meet( X, Y ), Z ), join( Z, Y ) ), join( Z, Y
% 1.44/1.84 ) ) ] )
% 1.44/1.84 , clause( 1721, [ =( join( join( meet( Z, Y ), X ), join( X, Y ) ), join( X
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1722, [ ~( =( join( join( a, b ), c ), join( a, join( c, b ) ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 51, [ ~( =( join( a, join( c, b ) ), join( join( a, b ), c ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, substitution( 0, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1725, [ ~( =( join( join( a, b ), c ), join( join( c, b ), a ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1722, [ ~( =( join( join( a, b ), c ), join( a, join( c, b ) )
% 1.44/1.84 ) ) ] )
% 1.44/1.84 , 0, 7, substitution( 0, [ :=( X, a ), :=( Y, join( c, b ) )] ),
% 1.44/1.84 substitution( 1, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 272, [ ~( =( join( join( a, b ), c ), join( join( c, b ), a ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , clause( 1725, [ ~( =( join( join( a, b ), c ), join( join( c, b ), a ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1755, [ ~( =( join( join( c, b ), a ), join( join( a, b ), c ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 272, [ ~( =( join( join( a, b ), c ), join( join( c, b ), a ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, substitution( 0, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1758, [ ~( =( join( join( c, b ), a ), join( c, join( a, b ) ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1755, [ ~( =( join( join( c, b ), a ), join( join( a, b ), c )
% 1.44/1.84 ) ) ] )
% 1.44/1.84 , 0, 7, substitution( 0, [ :=( X, join( a, b ) ), :=( Y, c )] ),
% 1.44/1.84 substitution( 1, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1774, [ ~( =( join( c, join( a, b ) ), join( join( c, b ), a ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 1758, [ ~( =( join( join( c, b ), a ), join( c, join( a, b ) ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 , 0, substitution( 0, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 273, [ ~( =( join( c, join( a, b ) ), join( join( c, b ), a ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , clause( 1774, [ ~( =( join( c, join( a, b ) ), join( join( c, b ), a ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1788, [ ~( =( join( join( c, b ), a ), join( c, join( a, b ) ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 273, [ ~( =( join( c, join( a, b ) ), join( join( c, b ), a ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, substitution( 0, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1792, [ ~( =( join( join( c, b ), a ), join( c, join( b, a ) ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1788, [ ~( =( join( join( c, b ), a ), join( c, join( a, b ) )
% 1.44/1.84 ) ) ] )
% 1.44/1.84 , 0, 9, substitution( 0, [ :=( X, a ), :=( Y, b )] ), substitution( 1, [] )
% 1.44/1.84 ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1820, [ ~( =( join( c, join( b, a ) ), join( join( c, b ), a ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , clause( 1792, [ ~( =( join( join( c, b ), a ), join( c, join( b, a ) ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 , 0, substitution( 0, [] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 275, [ ~( =( join( c, join( b, a ) ), join( join( c, b ), a ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , clause( 1820, [ ~( =( join( c, join( b, a ) ), join( join( c, b ), a ) )
% 1.44/1.84 ) ] )
% 1.44/1.84 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1822, [ =( join( X, Y ), meet( join( X, Y ), join( Y, X ) ) ) ] )
% 1.44/1.84 , clause( 255, [ =( meet( join( X, Y ), join( Y, X ) ), join( X, Y ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1827, [ =( join( join( X, Y ), join( meet( Z, Y ), X ) ), meet(
% 1.44/1.84 join( join( X, Y ), join( meet( Z, Y ), X ) ), join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 261, [ =( join( join( meet( X, Y ), Z ), join( Z, Y ) ), join( Z
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , 0, clause( 1822, [ =( join( X, Y ), meet( join( X, Y ), join( Y, X ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 20, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.44/1.84 substitution( 1, [ :=( X, join( X, Y ) ), :=( Y, join( meet( Z, Y ), X )
% 1.44/1.84 )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1829, [ =( join( join( X, Y ), join( meet( Z, Y ), X ) ), join( X,
% 1.44/1.84 Y ) ) ] )
% 1.44/1.84 , clause( 17, [ =( meet( join( Y, X ), Y ), Y ) ] )
% 1.44/1.84 , 0, clause( 1827, [ =( join( join( X, Y ), join( meet( Z, Y ), X ) ), meet(
% 1.44/1.84 join( join( X, Y ), join( meet( Z, Y ), X ) ), join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, 10, substitution( 0, [ :=( X, join( meet( Z, Y ), X ) ), :=( Y, join(
% 1.44/1.84 X, Y ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )
% 1.44/1.84 ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 976, [ =( join( join( Z, Y ), join( meet( X, Y ), Z ) ), join( Z, Y
% 1.44/1.84 ) ) ] )
% 1.44/1.84 , clause( 1829, [ =( join( join( X, Y ), join( meet( Z, Y ), X ) ), join( X
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1832, [ =( join( X, Y ), join( join( X, Y ), join( meet( Z, Y ), X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 976, [ =( join( join( Z, Y ), join( meet( X, Y ), Z ) ), join( Z
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1833, [ =( join( X, Y ), join( join( X, Y ), join( meet( Y, Z ), X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 39, [ =( meet( meet( X, Y ), X ), meet( X, Y ) ) ] )
% 1.44/1.84 , 0, clause( 1832, [ =( join( X, Y ), join( join( X, Y ), join( meet( Z, Y
% 1.44/1.84 ), X ) ) ) ] )
% 1.44/1.84 , 0, 9, substitution( 0, [ :=( X, Y ), :=( Y, Z )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, Y ), :=( Z, meet( Y, Z ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1834, [ =( join( join( X, Y ), join( meet( Y, Z ), X ) ), join( X,
% 1.44/1.84 Y ) ) ] )
% 1.44/1.84 , clause( 1833, [ =( join( X, Y ), join( join( X, Y ), join( meet( Y, Z ),
% 1.44/1.84 X ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 998, [ =( join( join( Z, X ), join( meet( X, Y ), Z ) ), join( Z, X
% 1.44/1.84 ) ) ] )
% 1.44/1.84 , clause( 1834, [ =( join( join( X, Y ), join( meet( Y, Z ), X ) ), join( X
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1835, [ =( join( X, Y ), join( join( X, Y ), join( meet( Z, Y ), X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 976, [ =( join( join( Z, Y ), join( meet( X, Y ), Z ) ), join( Z
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1839, [ =( join( X, Y ), join( join( X, Y ), join( X, meet( Z, Y )
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1835, [ =( join( X, Y ), join( join( X, Y ), join( meet( Z, Y
% 1.44/1.84 ), X ) ) ) ] )
% 1.44/1.84 , 0, 8, substitution( 0, [ :=( X, meet( Z, Y ) ), :=( Y, X )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1867, [ =( join( join( X, Y ), join( X, meet( Z, Y ) ) ), join( X,
% 1.44/1.84 Y ) ) ] )
% 1.44/1.84 , clause( 1839, [ =( join( X, Y ), join( join( X, Y ), join( X, meet( Z, Y
% 1.44/1.84 ) ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 1003, [ =( join( join( Z, Y ), join( Z, meet( X, Y ) ) ), join( Z,
% 1.44/1.84 Y ) ) ] )
% 1.44/1.84 , clause( 1867, [ =( join( join( X, Y ), join( X, meet( Z, Y ) ) ), join( X
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1868, [ =( join( X, Y ), join( join( X, Y ), join( meet( Y, Z ), X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 998, [ =( join( join( Z, X ), join( meet( X, Y ), Z ) ), join( Z
% 1.44/1.84 , X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1872, [ =( join( X, Y ), join( join( X, Y ), join( X, meet( Y, Z )
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1868, [ =( join( X, Y ), join( join( X, Y ), join( meet( Y, Z
% 1.44/1.84 ), X ) ) ) ] )
% 1.44/1.84 , 0, 8, substitution( 0, [ :=( X, meet( Y, Z ) ), :=( Y, X )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1875, [ =( join( X, Y ), join( join( X, meet( Y, Z ) ), join( X, Y
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1872, [ =( join( X, Y ), join( join( X, Y ), join( X, meet( Y
% 1.44/1.84 , Z ) ) ) ) ] )
% 1.44/1.84 , 0, 4, substitution( 0, [ :=( X, join( X, Y ) ), :=( Y, join( X, meet( Y,
% 1.44/1.84 Z ) ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1878, [ =( join( X, Y ), join( join( X, meet( Y, Z ) ), join( Y, X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1875, [ =( join( X, Y ), join( join( X, meet( Y, Z ) ), join(
% 1.44/1.84 X, Y ) ) ) ] )
% 1.44/1.84 , 0, 10, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1880, [ =( join( X, Y ), join( join( meet( Y, Z ), X ), join( Y, X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1878, [ =( join( X, Y ), join( join( X, meet( Y, Z ) ), join(
% 1.44/1.84 Y, X ) ) ) ] )
% 1.44/1.84 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, meet( Y, Z ) )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1881, [ =( join( Y, X ), join( join( meet( Y, Z ), X ), join( Y, X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1880, [ =( join( X, Y ), join( join( meet( Y, Z ), X ), join(
% 1.44/1.84 Y, X ) ) ) ] )
% 1.44/1.84 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1883, [ =( join( X, Y ), join( join( X, Y ), join( meet( X, Z ), Y
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 3, [ =( join( X, Y ), join( Y, X ) ) ] )
% 1.44/1.84 , 0, clause( 1881, [ =( join( Y, X ), join( join( meet( Y, Z ), X ), join(
% 1.44/1.84 Y, X ) ) ) ] )
% 1.44/1.84 , 0, 4, substitution( 0, [ :=( X, join( meet( X, Z ), Y ) ), :=( Y, join( X
% 1.44/1.84 , Y ) )] ), substitution( 1, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1894, [ =( join( join( X, Y ), join( meet( X, Z ), Y ) ), join( X,
% 1.44/1.84 Y ) ) ] )
% 1.44/1.84 , clause( 1883, [ =( join( X, Y ), join( join( X, Y ), join( meet( X, Z ),
% 1.44/1.84 Y ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 1026, [ =( join( join( Y, X ), join( meet( Y, Z ), X ) ), join( Y,
% 1.44/1.84 X ) ) ] )
% 1.44/1.84 , clause( 1894, [ =( join( join( X, Y ), join( meet( X, Z ), Y ) ), join( X
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1902, [ =( join( X, Y ), join( join( X, Y ), join( meet( X, Z ), Y
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 1026, [ =( join( join( Y, X ), join( meet( Y, Z ), X ) ), join( Y
% 1.44/1.84 , X ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1905, [ =( join( join( X, Y ), Z ), join( join( join( X, Y ), Z ),
% 1.44/1.84 join( X, Z ) ) ) ] )
% 1.44/1.84 , clause( 17, [ =( meet( join( Y, X ), Y ), Y ) ] )
% 1.44/1.84 , 0, clause( 1902, [ =( join( X, Y ), join( join( X, Y ), join( meet( X, Z
% 1.44/1.84 ), Y ) ) ) ] )
% 1.44/1.84 , 0, 13, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.44/1.84 :=( X, join( X, Y ) ), :=( Y, Z ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1906, [ =( join( join( join( X, Y ), Z ), join( X, Z ) ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ] )
% 1.44/1.84 , clause( 1905, [ =( join( join( X, Y ), Z ), join( join( join( X, Y ), Z )
% 1.44/1.84 , join( X, Z ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 1035, [ =( join( join( join( X, Y ), Z ), join( X, Z ) ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ] )
% 1.44/1.84 , clause( 1906, [ =( join( join( join( X, Y ), Z ), join( X, Z ) ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1908, [ =( join( join( Z, Y ), X ), join( join( X, Y ), join( join(
% 1.44/1.84 Z, Y ), X ) ) ) ] )
% 1.44/1.84 , clause( 190, [ =( join( join( Z, X ), join( join( Y, X ), Z ) ), join(
% 1.44/1.84 join( Y, X ), Z ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1914, [ =( join( join( X, Y ), join( X, meet( Z, Y ) ) ), join(
% 1.44/1.84 join( join( X, meet( Z, Y ) ), Y ), join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 1003, [ =( join( join( Z, Y ), join( Z, meet( X, Y ) ) ), join( Z
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , 0, clause( 1908, [ =( join( join( Z, Y ), X ), join( join( X, Y ), join(
% 1.44/1.84 join( Z, Y ), X ) ) ) ] )
% 1.44/1.84 , 0, 18, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.44/1.84 substitution( 1, [ :=( X, join( X, meet( Z, Y ) ) ), :=( Y, Y ), :=( Z, X
% 1.44/1.84 )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1919, [ =( join( X, Y ), join( join( join( X, meet( Z, Y ) ), Y ),
% 1.44/1.84 join( X, Y ) ) ) ] )
% 1.44/1.84 , clause( 1003, [ =( join( join( Z, Y ), join( Z, meet( X, Y ) ) ), join( Z
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , 0, clause( 1914, [ =( join( join( X, Y ), join( X, meet( Z, Y ) ) ), join(
% 1.44/1.84 join( join( X, meet( Z, Y ) ), Y ), join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, 1, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1922, [ =( join( X, Y ), join( join( X, meet( Z, Y ) ), Y ) ) ] )
% 1.44/1.84 , clause( 1035, [ =( join( join( join( X, Y ), Z ), join( X, Z ) ), join(
% 1.44/1.84 join( X, Y ), Z ) ) ] )
% 1.44/1.84 , 0, clause( 1919, [ =( join( X, Y ), join( join( join( X, meet( Z, Y ) ),
% 1.44/1.84 Y ), join( X, Y ) ) ) ] )
% 1.44/1.84 , 0, 4, substitution( 0, [ :=( X, X ), :=( Y, meet( Z, Y ) ), :=( Z, Y )] )
% 1.44/1.84 , substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1923, [ =( join( join( X, meet( Z, Y ) ), Y ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1922, [ =( join( X, Y ), join( join( X, meet( Z, Y ) ), Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 1356, [ =( join( join( X, meet( Z, Y ) ), Y ), join( X, Y ) ) ] )
% 1.44/1.84 , clause( 1923, [ =( join( join( X, meet( Z, Y ) ), Y ), join( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1925, [ =( join( X, Z ), join( join( X, meet( Y, Z ) ), Z ) ) ] )
% 1.44/1.84 , clause( 1356, [ =( join( join( X, meet( Z, Y ) ), Y ), join( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1932, [ =( join( X, join( Y, Z ) ), join( join( X, join( Z, Y ) ),
% 1.44/1.84 join( Y, Z ) ) ) ] )
% 1.44/1.84 , clause( 249, [ =( meet( join( Z, join( X, Y ) ), join( Y, X ) ), join( X
% 1.44/1.84 , Y ) ) ] )
% 1.44/1.84 , 0, clause( 1925, [ =( join( X, Z ), join( join( X, meet( Y, Z ) ), Z ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 9, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, T )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, join( T, join( Z, Y ) ) ), :=( Z,
% 1.44/1.84 join( Y, Z ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1933, [ =( join( X, join( Y, Z ) ), join( X, join( Z, Y ) ) ) ] )
% 1.44/1.84 , clause( 257, [ =( join( join( Z, join( Y, X ) ), join( X, Y ) ), join( Z
% 1.44/1.84 , join( Y, X ) ) ) ] )
% 1.44/1.84 , 0, clause( 1932, [ =( join( X, join( Y, Z ) ), join( join( X, join( Z, Y
% 1.44/1.84 ) ), join( Y, Z ) ) ) ] )
% 1.44/1.84 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 1370, [ =( join( T, join( Y, Z ) ), join( T, join( Z, Y ) ) ) ] )
% 1.44/1.84 , clause( 1933, [ =( join( X, join( Y, Z ) ), join( X, join( Z, Y ) ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , substitution( 0, [ :=( X, T ), :=( Y, Y ), :=( Z, Z )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1935, [ =( join( X, Z ), join( join( X, meet( Y, Z ) ), Z ) ) ] )
% 1.44/1.84 , clause( 1356, [ =( join( join( X, meet( Z, Y ) ), Y ), join( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1938, [ =( join( X, join( Y, Z ) ), join( join( X, Z ), join( Y, Z
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 12, [ =( meet( X, join( Y, X ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1935, [ =( join( X, Z ), join( join( X, meet( Y, Z ) ), Z ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 9, substitution( 0, [ :=( X, Z ), :=( Y, Y )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, Z ), :=( Z, join( Y, Z ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1939, [ =( join( join( X, Z ), join( Y, Z ) ), join( X, join( Y, Z
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 1938, [ =( join( X, join( Y, Z ) ), join( join( X, Z ), join( Y,
% 1.44/1.84 Z ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 1377, [ =( join( join( Z, X ), join( Y, X ) ), join( Z, join( Y, X
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 1939, [ =( join( join( X, Z ), join( Y, Z ) ), join( X, join( Y,
% 1.44/1.84 Z ) ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1941, [ =( join( X, Z ), join( join( X, meet( Y, Z ) ), Z ) ) ] )
% 1.44/1.84 , clause( 1356, [ =( join( join( X, meet( Z, Y ) ), Y ), join( X, Y ) ) ]
% 1.44/1.84 )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1944, [ =( join( X, join( Y, Z ) ), join( join( X, Y ), join( Y, Z
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 11, [ =( meet( X, join( X, Y ) ), X ) ] )
% 1.44/1.84 , 0, clause( 1941, [ =( join( X, Z ), join( join( X, meet( Y, Z ) ), Z ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 9, substitution( 0, [ :=( X, Y ), :=( Y, Z )] ), substitution( 1, [
% 1.44/1.84 :=( X, X ), :=( Y, Y ), :=( Z, join( Y, Z ) )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 eqswap(
% 1.44/1.84 clause( 1945, [ =( join( join( X, Y ), join( Y, Z ) ), join( X, join( Y, Z
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 1944, [ =( join( X, join( Y, Z ) ), join( join( X, Y ), join( Y,
% 1.44/1.84 Z ) ) ) ] )
% 1.44/1.84 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 1378, [ =( join( join( Z, X ), join( X, Y ) ), join( Z, join( X, Y
% 1.44/1.84 ) ) ) ] )
% 1.44/1.84 , clause( 1945, [ =( join( join( X, Y ), join( Y, Z ) ), join( X, join( Y,
% 1.44/1.84 Z ) ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1970, [ =( join( X, join( join( join( Y, Z ), T ), join( T, Z ) ) )
% 1.44/1.84 , join( X, join( join( Y, Z ), T ) ) ) ] )
% 1.44/1.84 , clause( 190, [ =( join( join( Z, X ), join( join( Y, X ), Z ) ), join(
% 1.44/1.84 join( Y, X ), Z ) ) ] )
% 1.44/1.84 , 0, clause( 1370, [ =( join( T, join( Y, Z ) ), join( T, join( Z, Y ) ) )
% 1.44/1.84 ] )
% 1.44/1.84 , 0, 14, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, T )] ),
% 1.44/1.84 substitution( 1, [ :=( X, U ), :=( Y, join( join( Y, Z ), T ) ), :=( Z,
% 1.44/1.84 join( T, Z ) ), :=( T, X )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1971, [ =( join( X, join( join( Y, Z ), join( T, Z ) ) ), join( X,
% 1.44/1.84 join( join( Y, Z ), T ) ) ) ] )
% 1.44/1.84 , clause( 1378, [ =( join( join( Z, X ), join( X, Y ) ), join( Z, join( X,
% 1.44/1.84 Y ) ) ) ] )
% 1.44/1.84 , 0, clause( 1970, [ =( join( X, join( join( join( Y, Z ), T ), join( T, Z
% 1.44/1.84 ) ) ), join( X, join( join( Y, Z ), T ) ) ) ] )
% 1.44/1.84 , 0, 3, substitution( 0, [ :=( X, T ), :=( Y, Z ), :=( Z, join( Y, Z ) )] )
% 1.44/1.84 , substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] )
% 1.44/1.84 ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 paramod(
% 1.44/1.84 clause( 1972, [ =( join( X, join( Y, join( T, Z ) ) ), join( X, join( join(
% 1.44/1.84 Y, Z ), T ) ) ) ] )
% 1.44/1.84 , clause( 1377, [ =( join( join( Z, X ), join( Y, X ) ), join( Z, join( Y,
% 1.44/1.84 X ) ) ) ] )
% 1.44/1.84 , 0, clause( 1971, [ =( join( X, join( join( Y, Z ), join( T, Z ) ) ), join(
% 1.44/1.84 X, join( join( Y, Z ), T ) ) ) ] )
% 1.44/1.84 , 0, 3, substitution( 0, [ :=( X, Z ), :=( Y, T ), :=( Z, Y )] ),
% 1.44/1.84 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] )).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 subsumption(
% 1.44/1.84 clause( 1380, [ =( join( T, join( Z, join( X, Y ) ) ), join( T, join( join(
% 1.44/1.84 Z, Y ), X ) ) ) ] )
% 1.44/1.84 , clause( 1972, [ =( join( X, join( Y, join( T, Z ) ) ), join( X, join(
% 1.44/1.84 join( Y, Z ), T ) ) ) ] )
% 1.44/1.84 , substitution( 0, [ :=( X, T ), :=( Y, Z ), :=( Z, Y ), :=( T, X )] ),
% 1.44/1.84 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 ==> clause( 1383, [ =( join( X, join( Z, Y ) ), join( join( X, Y ), Z ) ) ]
% 1.44/1.84 )
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84
% 1.44/1.84 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 1.44/1.84
% 1.44/1.84 Bliksem ended
%------------------------------------------------------------------------------