%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : LAT249-1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n018.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:49:34 EDT 2022
% Result : Unsatisfiable 4.12s 4.50s
% Output : Refutation 4.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LAT249-1 : TPTP v8.1.0. Released v3.1.0.
% 0.12/0.13 % Command : bliksem %s
% 0.12/0.34 % Computer : n018.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Wed Jun 29 16:33:45 EDT 2022
% 0.20/0.34 % CPUTime :
% 4.12/4.50 *** allocated 10000 integers for termspace/termends
% 4.12/4.50 *** allocated 10000 integers for clauses
% 4.12/4.50 *** allocated 10000 integers for justifications
% 4.12/4.50 Bliksem 1.12
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 Automatic Strategy Selection
% 4.12/4.50
% 4.12/4.50 Clauses:
% 4.12/4.50 [
% 4.12/4.50 [ =( meet( X, X ), X ) ],
% 4.12/4.50 [ =( join( X, X ), X ) ],
% 4.12/4.50 [ =( meet( X, join( X, Y ) ), X ) ],
% 4.12/4.50 [ =( join( X, meet( X, Y ) ), X ) ],
% 4.12/4.50 [ =( meet( X, Y ), meet( Y, X ) ) ],
% 4.12/4.50 [ =( join( X, Y ), join( Y, X ) ) ],
% 4.12/4.50 [ =( meet( meet( X, Y ), Z ), meet( X, meet( Y, Z ) ) ) ],
% 4.12/4.50 [ =( join( join( X, Y ), Z ), join( X, join( Y, Z ) ) ) ],
% 4.12/4.50 [ =( join( X, complement( X ) ), one ) ],
% 4.12/4.50 [ =( meet( X, complement( X ) ), zero ) ],
% 4.12/4.50 [ ~( =( meet( X, Y ), zero ) ), ~( =( join( X, Y ), one ) ), =(
% 4.12/4.50 complement( X ), Y ) ],
% 4.12/4.50 [ =( meet( X, join( Y, Z ) ), meet( X, join( Y, meet( X, join( Z, meet(
% 4.12/4.50 X, join( Y, meet( X, Z ) ) ) ) ) ) ) ) ],
% 4.12/4.50 [ =( meet( b, a ), a ) ],
% 4.12/4.50 [ ~( =( join( complement( b ), complement( a ) ), complement( a ) ) ) ]
% 4.12/4.50
% 4.12/4.50 ] .
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 percentage equality = 1.000000, percentage horn = 1.000000
% 4.12/4.50 This is a pure equality problem
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 Options Used:
% 4.12/4.50
% 4.12/4.50 useres = 1
% 4.12/4.50 useparamod = 1
% 4.12/4.50 useeqrefl = 1
% 4.12/4.50 useeqfact = 1
% 4.12/4.50 usefactor = 1
% 4.12/4.50 usesimpsplitting = 0
% 4.12/4.50 usesimpdemod = 5
% 4.12/4.50 usesimpres = 3
% 4.12/4.50
% 4.12/4.50 resimpinuse = 1000
% 4.12/4.50 resimpclauses = 20000
% 4.12/4.50 substype = eqrewr
% 4.12/4.50 backwardsubs = 1
% 4.12/4.50 selectoldest = 5
% 4.12/4.50
% 4.12/4.50 litorderings [0] = split
% 4.12/4.50 litorderings [1] = extend the termordering, first sorting on arguments
% 4.12/4.50
% 4.12/4.50 termordering = kbo
% 4.12/4.50
% 4.12/4.50 litapriori = 0
% 4.12/4.50 termapriori = 1
% 4.12/4.50 litaposteriori = 0
% 4.12/4.50 termaposteriori = 0
% 4.12/4.50 demodaposteriori = 0
% 4.12/4.50 ordereqreflfact = 0
% 4.12/4.50
% 4.12/4.50 litselect = negord
% 4.12/4.50
% 4.12/4.50 maxweight = 15
% 4.12/4.50 maxdepth = 30000
% 4.12/4.50 maxlength = 115
% 4.12/4.50 maxnrvars = 195
% 4.12/4.50 excuselevel = 1
% 4.12/4.50 increasemaxweight = 1
% 4.12/4.50
% 4.12/4.50 maxselected = 10000000
% 4.12/4.50 maxnrclauses = 10000000
% 4.12/4.50
% 4.12/4.50 showgenerated = 0
% 4.12/4.50 showkept = 0
% 4.12/4.50 showselected = 0
% 4.12/4.50 showdeleted = 0
% 4.12/4.50 showresimp = 1
% 4.12/4.50 showstatus = 2000
% 4.12/4.50
% 4.12/4.50 prologoutput = 1
% 4.12/4.50 nrgoals = 5000000
% 4.12/4.50 totalproof = 1
% 4.12/4.50
% 4.12/4.50 Symbols occurring in the translation:
% 4.12/4.50
% 4.12/4.50 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 4.12/4.50 . [1, 2] (w:1, o:22, a:1, s:1, b:0),
% 4.12/4.50 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 4.12/4.50 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 4.12/4.50 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 4.12/4.50 meet [40, 2] (w:1, o:47, a:1, s:1, b:0),
% 4.12/4.50 join [41, 2] (w:1, o:48, a:1, s:1, b:0),
% 4.12/4.50 complement [44, 1] (w:1, o:21, a:1, s:1, b:0),
% 4.12/4.50 one [45, 0] (w:1, o:7, a:1, s:1, b:0),
% 4.12/4.50 zero [46, 0] (w:1, o:13, a:1, s:1, b:0),
% 4.12/4.50 b [47, 0] (w:1, o:15, a:1, s:1, b:0),
% 4.12/4.50 a [48, 0] (w:1, o:14, a:1, s:1, b:0).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 Starting Search:
% 4.12/4.50
% 4.12/4.50 Resimplifying inuse:
% 4.12/4.50 Done
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 Intermediate Status:
% 4.12/4.50 Generated: 49803
% 4.12/4.50 Kept: 2001
% 4.12/4.50 Inuse: 263
% 4.12/4.50 Deleted: 23
% 4.12/4.50 Deletedinuse: 4
% 4.12/4.50
% 4.12/4.50 Resimplifying inuse:
% 4.12/4.50 Done
% 4.12/4.50
% 4.12/4.50 Resimplifying inuse:
% 4.12/4.50 Done
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 Intermediate Status:
% 4.12/4.50 Generated: 112357
% 4.12/4.50 Kept: 4008
% 4.12/4.50 Inuse: 391
% 4.12/4.50 Deleted: 38
% 4.12/4.50 Deletedinuse: 4
% 4.12/4.50
% 4.12/4.50 Resimplifying inuse:
% 4.12/4.50 Done
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 Bliksems!, er is een bewijs:
% 4.12/4.50 % SZS status Unsatisfiable
% 4.12/4.50 % SZS output start Refutation
% 4.12/4.50
% 4.12/4.50 clause( 2, [ =( meet( X, join( X, Y ) ), X ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 3, [ =( join( X, meet( X, Y ) ), X ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 4, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 5, [ =( join( X, Y ), join( Y, X ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 6, [ =( meet( X, meet( Y, Z ) ), meet( meet( X, Y ), Z ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 7, [ =( join( X, join( Y, Z ) ), join( join( X, Y ), Z ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 8, [ =( join( X, complement( X ) ), one ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 9, [ =( meet( X, complement( X ) ), zero ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 10, [ ~( =( meet( X, Y ), zero ) ), ~( =( join( X, Y ), one ) ),
% 4.12/4.50 =( complement( X ), Y ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 11, [ =( meet( X, join( Y, meet( X, join( Z, meet( X, join( Y, meet(
% 4.12/4.50 X, Z ) ) ) ) ) ) ), meet( X, join( Y, Z ) ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 12, [ =( meet( b, a ), a ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 13, [ ~( =( join( complement( b ), complement( a ) ), complement( a
% 4.12/4.50 ) ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 14, [ =( meet( X, one ), X ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 16, [ =( join( complement( X ), X ), one ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 17, [ =( meet( one, X ), X ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 19, [ =( meet( complement( X ), X ), zero ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 20, [ =( meet( a, b ), a ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 23, [ =( join( X, zero ), X ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 26, [ =( join( zero, X ), X ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 27, [ =( meet( zero, X ), zero ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 28, [ =( meet( X, zero ), zero ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 33, [ =( meet( meet( Y, X ), complement( X ) ), zero ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 37, [ =( join( one, X ), one ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 39, [ =( join( X, one ), one ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 42, [ =( join( join( Y, complement( X ) ), X ), one ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 55, [ =( complement( X ), zero ), ~( =( X, one ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 57, [ =( complement( complement( X ) ), X ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 110, [ =( meet( X, join( Z, complement( T ) ) ), meet( X, join( Z,
% 4.12/4.50 Y ) ) ), ~( =( join( T, meet( X, join( Y, meet( X, join( Z, meet( X, Y )
% 4.12/4.50 ) ) ) ) ), one ) ), ~( =( meet( meet( T, X ), join( Y, meet( X, join( Z
% 4.12/4.50 , meet( X, Y ) ) ) ) ), zero ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 154, [ ~( =( complement( X ), complement( a ) ) ), ~( =( meet( X,
% 4.12/4.50 join( complement( b ), complement( a ) ) ), zero ) ), ~( =( join( join( X
% 4.12/4.50 , complement( b ) ), complement( a ) ), one ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 406, [ =( meet( a, complement( b ) ), zero ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 538, [ =( join( join( complement( Y ), X ), Y ), one ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 4355, [ ~( =( meet( a, join( complement( b ), complement( a ) ) ),
% 4.12/4.50 zero ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 4366, [ ~( =( X, one ) ) ] )
% 4.12/4.50 .
% 4.12/4.50 clause( 4371, [] )
% 4.12/4.50 .
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 % SZS output end Refutation
% 4.12/4.50 found a proof!
% 4.12/4.50
% 4.12/4.50 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 4.12/4.50
% 4.12/4.50 initialclauses(
% 4.12/4.50 [ clause( 4373, [ =( meet( X, X ), X ) ] )
% 4.12/4.50 , clause( 4374, [ =( join( X, X ), X ) ] )
% 4.12/4.50 , clause( 4375, [ =( meet( X, join( X, Y ) ), X ) ] )
% 4.12/4.50 , clause( 4376, [ =( join( X, meet( X, Y ) ), X ) ] )
% 4.12/4.50 , clause( 4377, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 4.12/4.50 , clause( 4378, [ =( join( X, Y ), join( Y, X ) ) ] )
% 4.12/4.50 , clause( 4379, [ =( meet( meet( X, Y ), Z ), meet( X, meet( Y, Z ) ) ) ]
% 4.12/4.50 )
% 4.12/4.50 , clause( 4380, [ =( join( join( X, Y ), Z ), join( X, join( Y, Z ) ) ) ]
% 4.12/4.50 )
% 4.12/4.50 , clause( 4381, [ =( join( X, complement( X ) ), one ) ] )
% 4.12/4.50 , clause( 4382, [ =( meet( X, complement( X ) ), zero ) ] )
% 4.12/4.50 , clause( 4383, [ ~( =( meet( X, Y ), zero ) ), ~( =( join( X, Y ), one ) )
% 4.12/4.50 , =( complement( X ), Y ) ] )
% 4.12/4.50 , clause( 4384, [ =( meet( X, join( Y, Z ) ), meet( X, join( Y, meet( X,
% 4.12/4.50 join( Z, meet( X, join( Y, meet( X, Z ) ) ) ) ) ) ) ) ] )
% 4.12/4.50 , clause( 4385, [ =( meet( b, a ), a ) ] )
% 4.12/4.50 , clause( 4386, [ ~( =( join( complement( b ), complement( a ) ),
% 4.12/4.50 complement( a ) ) ) ] )
% 4.12/4.50 ] ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 2, [ =( meet( X, join( X, Y ) ), X ) ] )
% 4.12/4.50 , clause( 4375, [ =( meet( X, join( X, Y ) ), X ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 4.12/4.50 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 3, [ =( join( X, meet( X, Y ) ), X ) ] )
% 4.12/4.50 , clause( 4376, [ =( join( X, meet( X, Y ) ), X ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 4.12/4.50 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 4, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 4.12/4.50 , clause( 4377, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 4.12/4.50 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 5, [ =( join( X, Y ), join( Y, X ) ) ] )
% 4.12/4.50 , clause( 4378, [ =( join( X, Y ), join( Y, X ) ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 4.12/4.50 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4406, [ =( meet( X, meet( Y, Z ) ), meet( meet( X, Y ), Z ) ) ] )
% 4.12/4.50 , clause( 4379, [ =( meet( meet( X, Y ), Z ), meet( X, meet( Y, Z ) ) ) ]
% 4.12/4.50 )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 6, [ =( meet( X, meet( Y, Z ) ), meet( meet( X, Y ), Z ) ) ] )
% 4.12/4.50 , clause( 4406, [ =( meet( X, meet( Y, Z ) ), meet( meet( X, Y ), Z ) ) ]
% 4.12/4.50 )
% 4.12/4.50 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 4.12/4.50 permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4412, [ =( join( X, join( Y, Z ) ), join( join( X, Y ), Z ) ) ] )
% 4.12/4.50 , clause( 4380, [ =( join( join( X, Y ), Z ), join( X, join( Y, Z ) ) ) ]
% 4.12/4.50 )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 7, [ =( join( X, join( Y, Z ) ), join( join( X, Y ), Z ) ) ] )
% 4.12/4.50 , clause( 4412, [ =( join( X, join( Y, Z ) ), join( join( X, Y ), Z ) ) ]
% 4.12/4.50 )
% 4.12/4.50 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 4.12/4.50 permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 8, [ =( join( X, complement( X ) ), one ) ] )
% 4.12/4.50 , clause( 4381, [ =( join( X, complement( X ) ), one ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 9, [ =( meet( X, complement( X ) ), zero ) ] )
% 4.12/4.50 , clause( 4382, [ =( meet( X, complement( X ) ), zero ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 10, [ ~( =( meet( X, Y ), zero ) ), ~( =( join( X, Y ), one ) ),
% 4.12/4.50 =( complement( X ), Y ) ] )
% 4.12/4.50 , clause( 4383, [ ~( =( meet( X, Y ), zero ) ), ~( =( join( X, Y ), one ) )
% 4.12/4.50 , =( complement( X ), Y ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 4.12/4.50 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4458, [ =( meet( X, join( Y, meet( X, join( Z, meet( X, join( Y,
% 4.12/4.50 meet( X, Z ) ) ) ) ) ) ), meet( X, join( Y, Z ) ) ) ] )
% 4.12/4.50 , clause( 4384, [ =( meet( X, join( Y, Z ) ), meet( X, join( Y, meet( X,
% 4.12/4.50 join( Z, meet( X, join( Y, meet( X, Z ) ) ) ) ) ) ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 11, [ =( meet( X, join( Y, meet( X, join( Z, meet( X, join( Y, meet(
% 4.12/4.50 X, Z ) ) ) ) ) ) ), meet( X, join( Y, Z ) ) ) ] )
% 4.12/4.50 , clause( 4458, [ =( meet( X, join( Y, meet( X, join( Z, meet( X, join( Y,
% 4.12/4.50 meet( X, Z ) ) ) ) ) ) ), meet( X, join( Y, Z ) ) ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 4.12/4.50 permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 12, [ =( meet( b, a ), a ) ] )
% 4.12/4.50 , clause( 4385, [ =( meet( b, a ), a ) ] )
% 4.12/4.50 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 13, [ ~( =( join( complement( b ), complement( a ) ), complement( a
% 4.12/4.50 ) ) ) ] )
% 4.12/4.50 , clause( 4386, [ ~( =( join( complement( b ), complement( a ) ),
% 4.12/4.50 complement( a ) ) ) ] )
% 4.12/4.50 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4495, [ =( X, meet( X, join( X, Y ) ) ) ] )
% 4.12/4.50 , clause( 2, [ =( meet( X, join( X, Y ) ), X ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4496, [ =( X, meet( X, one ) ) ] )
% 4.12/4.50 , clause( 8, [ =( join( X, complement( X ) ), one ) ] )
% 4.12/4.50 , 0, clause( 4495, [ =( X, meet( X, join( X, Y ) ) ) ] )
% 4.12/4.50 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 4.12/4.50 :=( Y, complement( X ) )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4497, [ =( meet( X, one ), X ) ] )
% 4.12/4.50 , clause( 4496, [ =( X, meet( X, one ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 14, [ =( meet( X, one ), X ) ] )
% 4.12/4.50 , clause( 4497, [ =( meet( X, one ), X ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4498, [ =( one, join( X, complement( X ) ) ) ] )
% 4.12/4.50 , clause( 8, [ =( join( X, complement( X ) ), one ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4499, [ =( one, join( complement( X ), X ) ) ] )
% 4.12/4.50 , clause( 5, [ =( join( X, Y ), join( Y, X ) ) ] )
% 4.12/4.50 , 0, clause( 4498, [ =( one, join( X, complement( X ) ) ) ] )
% 4.12/4.50 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, complement( X ) )] ),
% 4.12/4.50 substitution( 1, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4502, [ =( join( complement( X ), X ), one ) ] )
% 4.12/4.50 , clause( 4499, [ =( one, join( complement( X ), X ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 16, [ =( join( complement( X ), X ), one ) ] )
% 4.12/4.50 , clause( 4502, [ =( join( complement( X ), X ), one ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4503, [ =( X, meet( X, one ) ) ] )
% 4.12/4.50 , clause( 14, [ =( meet( X, one ), X ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4504, [ =( X, meet( one, X ) ) ] )
% 4.12/4.50 , clause( 4, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 4.12/4.50 , 0, clause( 4503, [ =( X, meet( X, one ) ) ] )
% 4.12/4.50 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, one )] ), substitution( 1, [
% 4.12/4.50 :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4507, [ =( meet( one, X ), X ) ] )
% 4.12/4.50 , clause( 4504, [ =( X, meet( one, X ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 17, [ =( meet( one, X ), X ) ] )
% 4.12/4.50 , clause( 4507, [ =( meet( one, X ), X ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4508, [ =( zero, meet( X, complement( X ) ) ) ] )
% 4.12/4.50 , clause( 9, [ =( meet( X, complement( X ) ), zero ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4509, [ =( zero, meet( complement( X ), X ) ) ] )
% 4.12/4.50 , clause( 4, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 4.12/4.50 , 0, clause( 4508, [ =( zero, meet( X, complement( X ) ) ) ] )
% 4.12/4.50 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, complement( X ) )] ),
% 4.12/4.50 substitution( 1, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4512, [ =( meet( complement( X ), X ), zero ) ] )
% 4.12/4.50 , clause( 4509, [ =( zero, meet( complement( X ), X ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 19, [ =( meet( complement( X ), X ), zero ) ] )
% 4.12/4.50 , clause( 4512, [ =( meet( complement( X ), X ), zero ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4513, [ =( a, meet( b, a ) ) ] )
% 4.12/4.50 , clause( 12, [ =( meet( b, a ), a ) ] )
% 4.12/4.50 , 0, substitution( 0, [] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4514, [ =( a, meet( a, b ) ) ] )
% 4.12/4.50 , clause( 4, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 4.12/4.50 , 0, clause( 4513, [ =( a, meet( b, a ) ) ] )
% 4.12/4.50 , 0, 2, substitution( 0, [ :=( X, b ), :=( Y, a )] ), substitution( 1, [] )
% 4.12/4.50 ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4517, [ =( meet( a, b ), a ) ] )
% 4.12/4.50 , clause( 4514, [ =( a, meet( a, b ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 20, [ =( meet( a, b ), a ) ] )
% 4.12/4.50 , clause( 4517, [ =( meet( a, b ), a ) ] )
% 4.12/4.50 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4519, [ =( X, join( X, meet( X, Y ) ) ) ] )
% 4.12/4.50 , clause( 3, [ =( join( X, meet( X, Y ) ), X ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4520, [ =( X, join( X, zero ) ) ] )
% 4.12/4.50 , clause( 9, [ =( meet( X, complement( X ) ), zero ) ] )
% 4.12/4.50 , 0, clause( 4519, [ =( X, join( X, meet( X, Y ) ) ) ] )
% 4.12/4.50 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 4.12/4.50 :=( Y, complement( X ) )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4521, [ =( join( X, zero ), X ) ] )
% 4.12/4.50 , clause( 4520, [ =( X, join( X, zero ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 23, [ =( join( X, zero ), X ) ] )
% 4.12/4.50 , clause( 4521, [ =( join( X, zero ), X ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4522, [ =( X, join( X, zero ) ) ] )
% 4.12/4.50 , clause( 23, [ =( join( X, zero ), X ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4523, [ =( X, join( zero, X ) ) ] )
% 4.12/4.50 , clause( 5, [ =( join( X, Y ), join( Y, X ) ) ] )
% 4.12/4.50 , 0, clause( 4522, [ =( X, join( X, zero ) ) ] )
% 4.12/4.50 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, zero )] ), substitution( 1, [
% 4.12/4.50 :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4526, [ =( join( zero, X ), X ) ] )
% 4.12/4.50 , clause( 4523, [ =( X, join( zero, X ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 26, [ =( join( zero, X ), X ) ] )
% 4.12/4.50 , clause( 4526, [ =( join( zero, X ), X ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4527, [ =( X, join( zero, X ) ) ] )
% 4.12/4.50 , clause( 26, [ =( join( zero, X ), X ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4529, [ =( meet( zero, X ), zero ) ] )
% 4.12/4.50 , clause( 3, [ =( join( X, meet( X, Y ) ), X ) ] )
% 4.12/4.50 , 0, clause( 4527, [ =( X, join( zero, X ) ) ] )
% 4.12/4.50 , 0, 4, substitution( 0, [ :=( X, zero ), :=( Y, X )] ), substitution( 1, [
% 4.12/4.50 :=( X, meet( zero, X ) )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 27, [ =( meet( zero, X ), zero ) ] )
% 4.12/4.50 , clause( 4529, [ =( meet( zero, X ), zero ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4531, [ =( zero, meet( zero, X ) ) ] )
% 4.12/4.50 , clause( 27, [ =( meet( zero, X ), zero ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4532, [ =( zero, meet( X, zero ) ) ] )
% 4.12/4.50 , clause( 4, [ =( meet( X, Y ), meet( Y, X ) ) ] )
% 4.12/4.50 , 0, clause( 4531, [ =( zero, meet( zero, X ) ) ] )
% 4.12/4.50 , 0, 2, substitution( 0, [ :=( X, zero ), :=( Y, X )] ), substitution( 1, [
% 4.12/4.50 :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4535, [ =( meet( X, zero ), zero ) ] )
% 4.12/4.50 , clause( 4532, [ =( zero, meet( X, zero ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 28, [ =( meet( X, zero ), zero ) ] )
% 4.12/4.50 , clause( 4535, [ =( meet( X, zero ), zero ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4537, [ =( meet( meet( X, Y ), Z ), meet( X, meet( Y, Z ) ) ) ] )
% 4.12/4.50 , clause( 6, [ =( meet( X, meet( Y, Z ) ), meet( meet( X, Y ), Z ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4541, [ =( meet( meet( X, Y ), complement( Y ) ), meet( X, zero ) )
% 4.12/4.50 ] )
% 4.12/4.50 , clause( 9, [ =( meet( X, complement( X ) ), zero ) ] )
% 4.12/4.50 , 0, clause( 4537, [ =( meet( meet( X, Y ), Z ), meet( X, meet( Y, Z ) ) )
% 4.12/4.50 ] )
% 4.12/4.50 , 0, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 4.12/4.50 :=( Y, Y ), :=( Z, complement( Y ) )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4542, [ =( meet( meet( X, Y ), complement( Y ) ), zero ) ] )
% 4.12/4.50 , clause( 28, [ =( meet( X, zero ), zero ) ] )
% 4.12/4.50 , 0, clause( 4541, [ =( meet( meet( X, Y ), complement( Y ) ), meet( X,
% 4.12/4.50 zero ) ) ] )
% 4.12/4.50 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 4.12/4.50 :=( Y, Y )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 33, [ =( meet( meet( Y, X ), complement( X ) ), zero ) ] )
% 4.12/4.50 , clause( 4542, [ =( meet( meet( X, Y ), complement( Y ) ), zero ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 4.12/4.50 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4545, [ =( X, join( X, meet( X, Y ) ) ) ] )
% 4.12/4.50 , clause( 3, [ =( join( X, meet( X, Y ) ), X ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4546, [ =( one, join( one, X ) ) ] )
% 4.12/4.50 , clause( 17, [ =( meet( one, X ), X ) ] )
% 4.12/4.50 , 0, clause( 4545, [ =( X, join( X, meet( X, Y ) ) ) ] )
% 4.12/4.50 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, one ),
% 4.12/4.50 :=( Y, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4547, [ =( join( one, X ), one ) ] )
% 4.12/4.50 , clause( 4546, [ =( one, join( one, X ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 37, [ =( join( one, X ), one ) ] )
% 4.12/4.50 , clause( 4547, [ =( join( one, X ), one ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4548, [ =( one, join( one, X ) ) ] )
% 4.12/4.50 , clause( 37, [ =( join( one, X ), one ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4549, [ =( one, join( X, one ) ) ] )
% 4.12/4.50 , clause( 5, [ =( join( X, Y ), join( Y, X ) ) ] )
% 4.12/4.50 , 0, clause( 4548, [ =( one, join( one, X ) ) ] )
% 4.12/4.50 , 0, 2, substitution( 0, [ :=( X, one ), :=( Y, X )] ), substitution( 1, [
% 4.12/4.50 :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4552, [ =( join( X, one ), one ) ] )
% 4.12/4.50 , clause( 4549, [ =( one, join( X, one ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 39, [ =( join( X, one ), one ) ] )
% 4.12/4.50 , clause( 4552, [ =( join( X, one ), one ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4554, [ =( join( join( X, Y ), Z ), join( X, join( Y, Z ) ) ) ] )
% 4.12/4.50 , clause( 7, [ =( join( X, join( Y, Z ) ), join( join( X, Y ), Z ) ) ] )
% 4.12/4.50 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4559, [ =( join( join( X, complement( Y ) ), Y ), join( X, one ) )
% 4.12/4.50 ] )
% 4.12/4.50 , clause( 16, [ =( join( complement( X ), X ), one ) ] )
% 4.12/4.50 , 0, clause( 4554, [ =( join( join( X, Y ), Z ), join( X, join( Y, Z ) ) )
% 4.12/4.50 ] )
% 4.12/4.50 , 0, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 4.12/4.50 :=( Y, complement( Y ) ), :=( Z, Y )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 paramod(
% 4.12/4.50 clause( 4560, [ =( join( join( X, complement( Y ) ), Y ), one ) ] )
% 4.12/4.50 , clause( 39, [ =( join( X, one ), one ) ] )
% 4.12/4.50 , 0, clause( 4559, [ =( join( join( X, complement( Y ) ), Y ), join( X, one
% 4.12/4.50 ) ) ] )
% 4.12/4.50 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 4.12/4.50 :=( Y, Y )] )).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 subsumption(
% 4.12/4.50 clause( 42, [ =( join( join( Y, complement( X ) ), X ), one ) ] )
% 4.12/4.50 , clause( 4560, [ =( join( join( X, complement( Y ) ), Y ), one ) ] )
% 4.12/4.50 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 4.12/4.50 )] ) ).
% 4.12/4.50
% 4.12/4.50
% 4.12/4.50 eqswap(
% 4.12/4.50 clause( 4562, [ ~( =( zero, meet( X, Y ) ) ), ~( =( join( X, Y ), one ) ),
% 4.12/4.50 =( complement( X ), Y ) ] )
% 4.12/4.50 , clause( 10, [ ~Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------