%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN714-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Thu Jul 21 02:54:08 EDT 2022
% Result : Unsatisfiable 24.23s 24.66s
% Output : Refutation 24.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SYN714-1 : TPTP v8.1.0. Released v2.5.0.
% 0.11/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n017.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.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Mon Jul 11 22:25:19 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.41/1.08 *** allocated 10000 integers for termspace/termends
% 0.41/1.08 *** allocated 10000 integers for clauses
% 0.41/1.08 *** allocated 10000 integers for justifications
% 0.41/1.08 Bliksem 1.12
% 0.41/1.08
% 0.41/1.08
% 0.41/1.08 Automatic Strategy Selection
% 0.41/1.08
% 0.41/1.08 Clauses:
% 0.41/1.08 [
% 0.41/1.08 [ p48( c62 ) ],
% 0.41/1.08 [ p47( c60 ) ],
% 0.41/1.08 [ p10( X, X ) ],
% 0.41/1.08 [ p7( X, X ) ],
% 0.41/1.08 [ p5( X, X ) ],
% 0.41/1.08 [ p42( X, X ) ],
% 0.41/1.08 [ p40( X, X ) ],
% 0.41/1.08 [ p36( X, X ) ],
% 0.41/1.08 [ p33( X, X ) ],
% 0.41/1.08 [ p32( X, X ) ],
% 0.41/1.08 [ p30( X, X ) ],
% 0.41/1.08 [ p3( X, X ) ],
% 0.41/1.08 [ p28( X, X ) ],
% 0.41/1.08 [ p26( X, X ) ],
% 0.41/1.08 [ p24( X, X ) ],
% 0.41/1.08 [ p23( X, X ) ],
% 0.41/1.08 [ p2( X, X ) ],
% 0.41/1.08 [ p19( X, X ) ],
% 0.41/1.08 [ p18( X, X ) ],
% 0.41/1.08 [ p16( X, X ) ],
% 0.41/1.08 [ p15( X, X ) ],
% 0.41/1.08 [ p51( c66, c67 ) ],
% 0.41/1.08 [ p53( c68, f17( c66 ) ) ],
% 0.41/1.08 [ ~( p16( f17( c66 ), c65 ) ) ],
% 0.41/1.08 [ p10( f11( c62 ), f11( c60 ) ) ],
% 0.41/1.08 [ p49( f4( c60 ), f4( c62 ) ) ],
% 0.41/1.08 [ p3( f12( c62 ), f12( c60 ) ) ],
% 0.41/1.08 [ p52( f20( f21( c62, c64 ) ), c66 ) ],
% 0.41/1.08 [ p2( f22( c58, c60, c61 ), c62 ) ],
% 0.41/1.08 [ p47( X ), ~( p47( Y ) ), ~( p2( Y, X ) ) ],
% 0.41/1.08 [ p48( X ), ~( p48( Y ) ), ~( p2( Y, X ) ) ],
% 0.41/1.08 [ p49( f4( c62 ), f13( f14( c63 ), f4( c60 ) ) ) ],
% 0.41/1.08 [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c60 ) ) ],
% 0.41/1.08 [ p40( f41( X ), f41( Y ) ), ~( p15( X, Y ) ) ],
% 0.41/1.08 [ p10( f11( X ), f11( Y ) ), ~( p2( X, Y ) ) ],
% 0.41/1.08 [ p10( f31( X ), f31( Y ) ), ~( p30( X, Y ) ) ],
% 0.41/1.08 [ p15( f38( X ), f38( Y ) ), ~( p15( X, Y ) ) ],
% 0.41/1.08 [ p16( f17( X ), f17( Y ) ), ~( p15( X, Y ) ) ],
% 0.41/1.08 [ p19( f20( X ), f20( Y ) ), ~( p18( X, Y ) ) ],
% 0.41/1.08 [ p24( f39( X ), f39( Y ) ), ~( p15( X, Y ) ) ],
% 0.41/1.08 [ p3( f12( X ), f12( Y ) ), ~( p2( X, Y ) ) ],
% 0.41/1.08 [ p3( f14( X ), f14( Y ) ), ~( p3( X, Y ) ) ],
% 0.41/1.08 [ p3( f37( X ), f37( Y ) ), ~( p36( X, Y ) ) ],
% 0.41/1.08 [ p3( f4( X ), f4( Y ) ), ~( p2( X, Y ) ) ],
% 0.41/1.08 [ p10( X, Y ), ~( p10( Z, X ) ), ~( p10( Z, Y ) ) ],
% 0.41/1.08 [ p7( X, Y ), ~( p7( Z, X ) ), ~( p7( Z, Y ) ) ],
% 0.41/1.08 [ p5( X, Y ), ~( p5( Z, X ) ), ~( p5( Z, Y ) ) ],
% 0.41/1.08 [ p42( X, Y ), ~( p42( Z, X ) ), ~( p42( Z, Y ) ) ],
% 0.41/1.08 [ p40( X, Y ), ~( p40( Z, X ) ), ~( p40( Z, Y ) ) ],
% 0.41/1.08 [ p36( X, Y ), ~( p36( Z, X ) ), ~( p36( Z, Y ) ) ],
% 0.41/1.08 [ p33( X, Y ), ~( p33( Z, X ) ), ~( p33( Z, Y ) ) ],
% 0.41/1.08 [ p32( X, Y ), ~( p32( Z, X ) ), ~( p32( Z, Y ) ) ],
% 0.41/1.08 [ p30( X, Y ), ~( p30( Z, X ) ), ~( p30( Z, Y ) ) ],
% 0.41/1.08 [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ],
% 0.41/1.08 [ p28( X, Y ), ~( p28( Z, X ) ), ~( p28( Z, Y ) ) ],
% 0.41/1.08 [ p26( X, Y ), ~( p26( Z, X ) ), ~( p26( Z, Y ) ) ],
% 0.41/1.08 [ p24( X, Y ), ~( p24( Z, X ) ), ~( p24( Z, Y ) ) ],
% 0.41/1.08 [ p23( X, Y ), ~( p23( Z, X ) ), ~( p23( Z, Y ) ) ],
% 0.41/1.08 [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ],
% 0.41/1.08 [ p19( X, Y ), ~( p19( Z, X ) ), ~( p19( Z, Y ) ) ],
% 0.41/1.08 [ p18( X, Y ), ~( p18( Z, X ) ), ~( p18( Z, Y ) ) ],
% 0.41/1.08 [ p16( X, Y ), ~( p16( Z, X ) ), ~( p16( Z, Y ) ) ],
% 0.41/1.08 [ p15( X, Y ), ~( p15( Z, X ) ), ~( p15( Z, Y ) ) ],
% 0.41/1.08 [ p50( c66, f25( f27( c59, X ), c67 ), c62 ), ~( p53( X, f17( c66 ) ) )
% 0.41/1.08 ],
% 0.41/1.08 [ p57( X, Y ), ~( p5( Z, Y ) ), ~( p57( T, Z ) ), ~( p5( T, X ) ) ],
% 0.41/1.08 [ p45( X, Y ), ~( p5( Z, X ) ), ~( p5( T, Y ) ), ~( p45( Z, T ) ) ],
% 0.41/1.08 [ p46( X, Y ), ~( p46( Z, T ) ), ~( p7( Z, X ) ), ~( p3( T, Y ) ) ],
% 0.41/1.08 [ p49( X, Y ), ~( p3( Z, Y ) ), ~( p49( T, Z ) ), ~( p3( T, X ) ) ],
% 0.41/1.08 [ p51( X, Y ), ~( p24( Z, Y ) ), ~( p51( T, Z ) ), ~( p15( T, X ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p52( X, Y ), ~( p19( Z, X ) ), ~( p52( Z, T ) ), ~( p15( T, Y ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p53( X, Y ), ~( p26( Z, X ) ), ~( p53( Z, T ) ), ~( p16( T, Y ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p54( X, Y ), ~( p30( Z, X ) ), ~( p54( Z, T ) ), ~( p28( T, Y ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p55( X, Y ), ~( p5( Z, X ) ), ~( p55( Z, T ) ), ~( p10( T, Y ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p56( X, Y ), ~( p36( Z, X ) ), ~( p56( Z, T ) ), ~( p33( T, Y ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p45( X, c61 ), ~( p46( f8( f9( c58, X ), Y ), f4( f6( c59, c60 ) ) ) )
% 0.41/1.08 ],
% 0.41/1.08 [ p7( f8( X, Y ), f8( Z, T ) ), ~( p5( X, Z ) ), ~( p5( Y, T ) ) ],
% 0.41/1.08 [ p18( f21( X, Y ), f21( Z, T ) ), ~( p18( Y, T ) ), ~( p2( X, Z ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p2( f6( X, Y ), f6( Z, T ) ), ~( p2( Y, T ) ), ~( p5( X, Z ) ) ],
% 0.41/1.08 [ p23( f27( X, Y ), f27( Z, T ) ), ~( p26( Y, T ) ), ~( p5( X, Z ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p24( f25( X, Y ), f25( Z, T ) ), ~( p23( X, Z ) ), ~( p24( Y, T ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p28( f29( X, Y ), f29( Z, T ) ), ~( p28( Y, T ) ), ~( p7( X, Z ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ p3( f13( X, Y ), f13( Z, T ) ), ~( p3( X, Z ) ), ~( p3( Y, T ) ) ]
% 5.84/6.28 ,
% 5.84/6.28 [ p32( f35( X, Y ), f35( Z, T ) ), ~( p5( X, Z ) ), ~( p7( Y, T ) ) ]
% 5.84/6.28 ,
% 5.84/6.28 [ p33( f34( X, Y ), f34( Z, T ) ), ~( p32( X, Z ) ), ~( p33( Y, T ) ) ]
% 5.84/6.28 ,
% 5.84/6.28 [ p5( f9( X, Y ), f9( Z, T ) ), ~( p5( X, Z ) ), ~( p5( Y, T ) ) ],
% 5.84/6.28 [ p56( X, f34( f35( Y, Z ), T ) ), ~( p56( X, T ) ), ~( p46( Z, f37( X )
% 5.84/6.28 ) ) ],
% 5.84/6.28 [ p51( X, f25( f27( Y, Z ), T ) ), ~( p51( X, T ) ), ~( p53( Z, f17( X )
% 5.84/6.28 ) ) ],
% 5.84/6.28 [ p54( X, f29( f8( Y, Z ), T ) ), ~( p54( X, T ) ), ~( p55( Z, f31( X )
% 5.84/6.28 ) ) ],
% 5.84/6.28 [ p50( X, Y, Z ), ~( p15( T, X ) ), ~( p2( U, Z ) ), ~( p24( W, Y ) ),
% 5.84/6.28 ~( p50( T, W, U ) ) ],
% 5.84/6.28 [ p2( f22( X, Y, Z ), f22( T, U, W ) ), ~( p5( X, T ) ), ~( p5( Z, W ) )
% 5.84/6.28 , ~( p2( Y, U ) ) ],
% 5.84/6.28 [ p5( f43( X, Y, Z ), f43( T, U, W ) ), ~( p42( Z, W ) ), ~( p5( Y, U )
% 5.84/6.28 ), ~( p15( X, T ) ) ],
% 5.84/6.28 [ p26( f44( X, Y, Z ), f44( T, U, W ) ), ~( p42( Z, W ) ), ~( p5( Y, U )
% 5.84/6.28 ), ~( p15( X, T ) ) ],
% 5.84/6.28 [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p16( f17( f38( X ) ), f17( X
% 5.84/6.28 ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ],
% 5.84/6.28 [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p40( f41( f38( X ) ), f41( X
% 5.84/6.28 ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ],
% 5.84/6.28 [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p52( f20( f21( c62, c64 ) )
% 5.84/6.28 , f38( X ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ],
% 5.84/6.28 [ p16( f17( X ), c65 ), p16( f17( f38( X ) ), f17( X ) ), ~( p50( X, f39(
% 5.84/6.28 X ), c60 ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ],
% 5.84/6.28 [ p16( f17( X ), c65 ), p40( f41( f38( X ) ), f41( X ) ), ~( p50( X, f39(
% 5.84/6.28 X ), c60 ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ],
% 5.84/6.28 [ p16( f17( X ), c65 ), p50( X, Y, c60 ), ~( p51( X, Y ) ), ~( p50( X, Y
% 5.84/6.28 , c62 ) ), ~( p52( f20( f21( c62, c64 ) ), X ) ) ],
% 5.84/6.28 [ p16( f17( X ), c65 ), p52( f20( f21( c62, c64 ) ), f38( X ) ), ~( p50(
% 5.84/6.28 X, f39( X ), c60 ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ],
% 5.84/6.28 [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p50( f38( X ), Y, c62 ), ~(
% 5.84/6.28 p51( f38( X ), Y ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ],
% 5.84/6.28 [ p16( f17( X ), c65 ), p50( f38( X ), Y, c62 ), ~( p51( f38( X ), Y ) )
% 5.84/6.28 , ~( p50( X, f39( X ), c60 ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ]
% 5.84/6.28 ,
% 5.84/6.28 [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p57( c61, f43( X, Y, Z ) ),
% 5.84/6.28 p26( f44( f38( X ), Y, Z ), f44( X, Y, Z ) ), ~( p52( f20( f21( c60, c64
% 5.84/6.28 ) ), X ) ) ],
% 5.84/6.28 [ p16( f17( X ), c65 ), p57( c61, f43( X, Y, Z ) ), p26( f44( f38( X ),
% 5.84/6.28 Y, Z ), f44( X, Y, Z ) ), ~( p50( X, f39( X ), c60 ) ), ~( p52( f20( f21(
% 5.84/6.28 c60, c64 ) ), X ) ) ],
% 5.84/6.28 [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p5( Y, f9( c58, f43( X, Y, Z
% 5.84/6.28 ) ) ), p26( f44( f38( X ), Y, Z ), f44( X, Y, Z ) ), ~( p52( f20( f21(
% 5.84/6.28 c60, c64 ) ), X ) ) ],
% 5.84/6.28 [ p16( f17( X ), c65 ), p5( Y, f9( c58, f43( X, Y, Z ) ) ), p26( f44(
% 5.84/6.28 f38( X ), Y, Z ), f44( X, Y, Z ) ), ~( p50( X, f39( X ), c60 ) ), ~( p52(
% 5.84/6.28 f20( f21( c60, c64 ) ), X ) ) ]
% 5.84/6.28 ] .
% 5.84/6.28
% 5.84/6.28
% 5.84/6.28 percentage equality = 0.000000, percentage horn = 0.876190
% 5.84/6.28 This a non-horn, non-equality problem
% 5.84/6.28
% 5.84/6.28
% 5.84/6.28 Options Used:
% 5.84/6.28
% 5.84/6.28 useres = 1
% 5.84/6.28 useparamod = 0
% 5.84/6.28 useeqrefl = 0
% 5.84/6.28 useeqfact = 0
% 5.84/6.28 usefactor = 1
% 5.84/6.28 usesimpsplitting = 0
% 5.84/6.28 usesimpdemod = 0
% 5.84/6.28 usesimpres = 3
% 5.84/6.28
% 5.84/6.28 resimpinuse = 1000
% 5.84/6.28 resimpclauses = 20000
% 5.84/6.28 substype = standard
% 5.84/6.28 backwardsubs = 1
% 5.84/6.28 selectoldest = 5
% 5.84/6.28
% 5.84/6.28 litorderings [0] = split
% 5.84/6.28 litorderings [1] = liftord
% 5.84/6.28
% 5.84/6.28 termordering = none
% 5.84/6.28
% 5.84/6.28 litapriori = 1
% 5.84/6.28 termapriori = 0
% 5.84/6.28 litaposteriori = 0
% 5.84/6.28 termaposteriori = 0
% 5.84/6.28 demodaposteriori = 0
% 5.84/6.28 ordereqreflfact = 0
% 5.84/6.28
% 5.84/6.28 litselect = none
% 5.84/6.28
% 5.84/6.28 maxweight = 15
% 5.84/6.28 maxdepth = 30000
% 5.84/6.28 maxlength = 115
% 5.84/6.28 maxnrvars = 195
% 5.84/6.28 excuselevel = 1
% 5.84/6.28 increasemaxweight = 1
% 5.84/6.28
% 5.84/6.28 maxselected = 10000000
% 5.84/6.28 maxnrclauses = 10000000
% 5.84/6.28
% 5.84/6.28 showgenerated = 0
% 5.84/6.28 showkept = 0
% 5.84/6.28 showselected = 0
% 5.84/6.28 showdeleted = 0
% 5.84/6.28 showresimp = 1
% 5.84/6.28 showstatus = 2000
% 5.84/6.28
% 5.84/6.28 prologoutput = 1
% 5.84/6.28 nrgoals = 5000000
% 5.84/6.28 totalproof = 1
% 5.84/6.28
% 5.84/6.28 Symbols occurring in the translation:
% 5.84/6.28
% 5.84/6.28 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 5.84/6.28 . [1, 2] (w:1, o:246, a:1, s:1, b:0),
% 5.84/6.28 ! [4, 1] (w:0, o:228, a:1, s:1, b:0),
% 24.23/24.66 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 24.23/24.66 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 24.23/24.66 c62 [39, 0] (w:1, o:12, a:1, s:1, b:0),
% 24.23/24.66 p48 [40, 1] (w:1, o:234, a:1, s:1, b:0),
% 24.23/24.66 c60 [41, 0] (w:1, o:13, a:1, s:1, b:0),
% 24.23/24.66 p47 [42, 1] (w:1, o:233, a:1, s:1, b:0),
% 24.23/24.66 p10 [44, 2] (w:1, o:271, a:1, s:1, b:0),
% 24.23/24.66 p7 [46, 2] (w:1, o:272, a:1, s:1, b:0),
% 24.23/24.66 p5 [48, 2] (w:1, o:292, a:1, s:1, b:0),
% 24.23/24.66 p42 [50, 2] (w:1, o:287, a:1, s:1, b:0),
% 24.23/24.66 p40 [52, 2] (w:1, o:288, a:1, s:1, b:0),
% 24.23/24.66 p36 [54, 2] (w:1, o:282, a:1, s:1, b:0),
% 24.23/24.66 p33 [56, 2] (w:1, o:284, a:1, s:1, b:0),
% 24.23/24.66 p32 [58, 2] (w:1, o:283, a:1, s:1, b:0),
% 24.23/24.66 p30 [60, 2] (w:1, o:285, a:1, s:1, b:0),
% 24.23/24.66 p3 [62, 2] (w:1, o:286, a:1, s:1, b:0),
% 24.23/24.66 p28 [64, 2] (w:1, o:277, a:1, s:1, b:0),
% 24.23/24.66 p26 [66, 2] (w:1, o:278, a:1, s:1, b:0),
% 24.23/24.66 p24 [68, 2] (w:1, o:280, a:1, s:1, b:0),
% 24.23/24.66 p23 [70, 2] (w:1, o:279, a:1, s:1, b:0),
% 24.23/24.66 p2 [72, 2] (w:1, o:281, a:1, s:1, b:0),
% 24.23/24.66 p19 [74, 2] (w:1, o:274, a:1, s:1, b:0),
% 24.23/24.66 p18 [76, 2] (w:1, o:273, a:1, s:1, b:0),
% 24.23/24.66 p16 [78, 2] (w:1, o:276, a:1, s:1, b:0),
% 24.23/24.66 p15 [80, 2] (w:1, o:275, a:1, s:1, b:0),
% 24.23/24.66 c66 [81, 0] (w:1, o:218, a:1, s:1, b:0),
% 24.23/24.66 c67 [82, 0] (w:1, o:219, a:1, s:1, b:0),
% 24.23/24.66 p51 [83, 2] (w:1, o:293, a:1, s:1, b:0),
% 24.23/24.66 c68 [84, 0] (w:1, o:220, a:1, s:1, b:0),
% 24.23/24.66 f17 [85, 1] (w:1, o:235, a:1, s:1, b:0),
% 24.23/24.66 p53 [86, 2] (w:1, o:295, a:1, s:1, b:0),
% 24.23/24.66 c65 [87, 0] (w:1, o:217, a:1, s:1, b:0),
% 24.23/24.66 f11 [88, 1] (w:1, o:236, a:1, s:1, b:0),
% 24.23/24.66 f4 [89, 1] (w:1, o:241, a:1, s:1, b:0),
% 24.23/24.66 p49 [90, 2] (w:1, o:289, a:1, s:1, b:0),
% 24.23/24.66 f12 [91, 1] (w:1, o:242, a:1, s:1, b:0),
% 24.23/24.66 c64 [92, 0] (w:1, o:216, a:1, s:1, b:0),
% 24.23/24.66 f21 [93, 2] (w:1, o:297, a:1, s:1, b:0),
% 24.23/24.66 f20 [94, 1] (w:1, o:244, a:1, s:1, b:0),
% 24.23/24.66 p52 [95, 2] (w:1, o:294, a:1, s:1, b:0),
% 24.23/24.66 c58 [96, 0] (w:1, o:9, a:1, s:1, b:0),
% 24.23/24.66 c61 [97, 0] (w:1, o:11, a:1, s:1, b:0),
% 24.23/24.66 f22 [98, 3] (w:1, o:310, a:1, s:1, b:0),
% 24.23/24.66 c63 [103, 0] (w:1, o:215, a:1, s:1, b:0),
% 24.23/24.66 f14 [104, 1] (w:1, o:243, a:1, s:1, b:0),
% 24.23/24.66 f13 [105, 2] (w:1, o:296, a:1, s:1, b:0),
% 24.23/24.66 c59 [106, 0] (w:1, o:10, a:1, s:1, b:0),
% 24.23/24.66 f27 [107, 2] (w:1, o:298, a:1, s:1, b:0),
% 24.23/24.66 f25 [108, 2] (w:1, o:299, a:1, s:1, b:0),
% 24.23/24.66 p50 [109, 3] (w:1, o:311, a:1, s:1, b:0),
% 24.23/24.66 f41 [111, 1] (w:1, o:245, a:1, s:1, b:0),
% 24.23/24.66 f31 [116, 1] (w:1, o:237, a:1, s:1, b:0),
% 24.23/24.66 f38 [119, 1] (w:1, o:239, a:1, s:1, b:0),
% 24.23/24.66 f39 [126, 1] (w:1, o:240, a:1, s:1, b:0),
% 24.23/24.66 f37 [133, 1] (w:1, o:238, a:1, s:1, b:0),
% 24.23/24.66 p57 [178, 2] (w:1, o:301, a:1, s:1, b:0),
% 24.23/24.66 p45 [183, 2] (w:1, o:290, a:1, s:1, b:0),
% 24.23/24.66 p46 [188, 2] (w:1, o:291, a:1, s:1, b:0),
% 24.23/24.66 p54 [209, 2] (w:1, o:302, a:1, s:1, b:0),
% 24.23/24.66 p55 [214, 2] (w:1, o:303, a:1, s:1, b:0),
% 24.23/24.66 p56 [219, 2] (w:1, o:300, a:1, s:1, b:0),
% 24.23/24.66 f9 [223, 2] (w:1, o:305, a:1, s:1, b:0),
% 24.23/24.66 f8 [225, 2] (w:1, o:304, a:1, s:1, b:0),
% 24.23/24.66 f6 [226, 2] (w:1, o:306, a:1, s:1, b:0),
% 24.23/24.66 f29 [249, 2] (w:1, o:307, a:1, s:1, b:0),
% 24.23/24.66 f35 [258, 2] (w:1, o:309, a:1, s:1, b:0),
% 24.23/24.66 f34 [263, 2] (w:1, o:308, a:1, s:1, b:0),
% 24.23/24.66 f43 [297, 3] (w:1, o:312, a:1, s:1, b:0),
% 24.23/24.66 f44 [304, 3] (w:1, o:313, a:1, s:1, b:0).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 Starting Search:
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 Intermediate Status:
% 24.23/24.66 Generated: 7064
% 24.23/24.66 Kept: 2029
% 24.23/24.66 Inuse: 390
% 24.23/24.66 Deleted: 4
% 24.23/24.66 Deletedinuse: 3
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 Intermediate Status:
% 24.23/24.66 Generated: 16829
% 24.23/24.66 Kept: 4051
% 24.23/24.66 Inuse: 537
% 24.23/24.66 Deleted: 5
% 24.23/24.66 Deletedinuse: 3
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 Intermediate Status:
% 24.23/24.66 Generated: 37750
% 24.23/24.66 Kept: 6080
% 24.23/24.66 Inuse: 700
% 24.23/24.66 Deleted: 5
% 24.23/24.66 Deletedinuse: 3
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 Intermediate Status:
% 24.23/24.66 Generated: 88360
% 24.23/24.66 Kept: 8082
% 24.23/24.66 Inuse: 1052
% 24.23/24.66 Deleted: 5
% 24.23/24.66 Deletedinuse: 3
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 Intermediate Status:
% 24.23/24.66 Generated: 162805
% 24.23/24.66 Kept: 10088
% 24.23/24.66 Inuse: 1452
% 24.23/24.66 Deleted: 8
% 24.23/24.66 Deletedinuse: 3
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 Intermediate Status:
% 24.23/24.66 Generated: 339702
% 24.23/24.66 Kept: 12092
% 24.23/24.66 Inuse: 1772
% 24.23/24.66 Deleted: 8
% 24.23/24.66 Deletedinuse: 3
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 Intermediate Status:
% 24.23/24.66 Generated: 466518
% 24.23/24.66 Kept: 14100
% 24.23/24.66 Inuse: 2319
% 24.23/24.66 Deleted: 12
% 24.23/24.66 Deletedinuse: 7
% 24.23/24.66
% 24.23/24.66 Resimplifying inuse:
% 24.23/24.66 Done
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 Bliksems!, er is een bewijs:
% 24.23/24.66 % SZS status Unsatisfiable
% 24.23/24.66 % SZS output start Refutation
% 24.23/24.66
% 24.23/24.66 clause( 14, [ p24( X, X ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 20, [ p15( X, X ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 21, [ p51( c66, c67 ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 22, [ p53( c68, f17( c66 ) ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 23, [ ~( p16( f17( c66 ), c65 ) ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 27, [ p52( f20( f21( c62, c64 ) ), c66 ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 32, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c60 ) ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 56, [ ~( p24( Z, X ) ), ~( p24( Z, Y ) ), p24( X, Y ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 63, [ ~( p53( X, f17( c66 ) ) ), p50( c66, f25( f27( c59, X ), c67
% 24.23/24.66 ), c62 ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T, Z
% 24.23/24.66 ) ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 86, [ p51( X, f25( f27( Y, Z ), T ) ), ~( p51( X, T ) ), ~( p53( Z
% 24.23/24.66 , f17( X ) ) ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 97, [ p16( f17( X ), c65 ), ~( p51( X, Y ) ), ~( p50( X, Y, c62 ) )
% 24.23/24.66 , ~( p52( f20( f21( c62, c64 ) ), X ) ), p50( X, Y, c60 ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 329, [ p24( Y, X ), ~( p24( X, Y ) ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 512, [ ~( p15( c66, Y ) ), ~( p24( c67, X ) ), p51( Y, X ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 772, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( Y, Z ) ), ~(
% 24.23/24.66 p24( c67, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 773, [ ~( p24( X, Y ) ), ~( p24( c67, X ) ), p51( c66, Y ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 775, [ ~( p15( c66, T ) ), ~( p24( c67, X ) ), ~( p24( Y, Z ) ),
% 24.23/24.66 ~( p24( X, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 776, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, Y ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 777, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( Y, Z ) ), ~(
% 24.23/24.66 p24( Y, c67 ) ), p51( T, Z ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 778, [ ~( p24( X, Y ) ), ~( p24( X, c67 ) ), p51( c66, Y ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 788, [ ~( p15( c66, T ) ), ~( p24( X, c67 ) ), ~( p24( Y, Z ) ),
% 24.23/24.66 ~( p24( X, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 789, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, c67 ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 790, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( c67, Z ) ),
% 24.23/24.66 ~( p24( Y, c67 ) ), p51( T, Z ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 791, [ ~( p24( c67, X ) ), ~( p24( Y, c67 ) ), p51( c66, X ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 792, [ ~( p15( c66, T ) ), ~( p24( Y, c67 ) ), ~( p24( X, Z ) ),
% 24.23/24.66 ~( p24( c67, X ) ), p51( T, Z ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 793, [ ~( p15( c66, X ) ), ~( p24( c67, Y ) ), p51( X, c67 ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 794, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( c67, Z ) ),
% 24.23/24.66 ~( p24( c67, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 796, [ ~( p15( c66, X ) ), ~( p15( X, Y ) ), ~( p24( c67, Z ) ),
% 24.23/24.66 p51( Y, Z ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 797, [ ~( p24( c67, X ) ), p51( c66, X ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 805, [ ~( p15( c66, Z ) ), ~( p24( X, Y ) ), ~( p24( c67, X ) ),
% 24.23/24.66 p51( Z, Y ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 806, [ ~( p15( c66, X ) ), p51( X, c67 ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 1014, [ ~( p51( c66, Y ) ), p51( c66, f25( f27( X, c68 ), Y ) ) ]
% 24.23/24.66 )
% 24.23/24.66 .
% 24.23/24.66 clause( 1410, [ ~( p51( c66, f25( f27( c59, c68 ), c67 ) ) ), ~( p52( f20(
% 24.23/24.66 f21( c62, c64 ) ), c66 ) ), ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62
% 24.23/24.66 ) ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 2032, [ p51( c66, f25( f27( X, c68 ), c67 ) ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 14915, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62 ) ) ] )
% 24.23/24.66 .
% 24.23/24.66 clause( 14916, [] )
% 24.23/24.66 .
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 % SZS output end Refutation
% 24.23/24.66 found a proof!
% 24.23/24.66
% 24.23/24.66 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 24.23/24.66
% 24.23/24.66 initialclauses(
% 24.23/24.66 [ clause( 14918, [ p48( c62 ) ] )
% 24.23/24.66 , clause( 14919, [ p47( c60 ) ] )
% 24.23/24.66 , clause( 14920, [ p10( X, X ) ] )
% 24.23/24.66 , clause( 14921, [ p7( X, X ) ] )
% 24.23/24.66 , clause( 14922, [ p5( X, X ) ] )
% 24.23/24.66 , clause( 14923, [ p42( X, X ) ] )
% 24.23/24.66 , clause( 14924, [ p40( X, X ) ] )
% 24.23/24.66 , clause( 14925, [ p36( X, X ) ] )
% 24.23/24.66 , clause( 14926, [ p33( X, X ) ] )
% 24.23/24.66 , clause( 14927, [ p32( X, X ) ] )
% 24.23/24.66 , clause( 14928, [ p30( X, X ) ] )
% 24.23/24.66 , clause( 14929, [ p3( X, X ) ] )
% 24.23/24.66 , clause( 14930, [ p28( X, X ) ] )
% 24.23/24.66 , clause( 14931, [ p26( X, X ) ] )
% 24.23/24.66 , clause( 14932, [ p24( X, X ) ] )
% 24.23/24.66 , clause( 14933, [ p23( X, X ) ] )
% 24.23/24.66 , clause( 14934, [ p2( X, X ) ] )
% 24.23/24.66 , clause( 14935, [ p19( X, X ) ] )
% 24.23/24.66 , clause( 14936, [ p18( X, X ) ] )
% 24.23/24.66 , clause( 14937, [ p16( X, X ) ] )
% 24.23/24.66 , clause( 14938, [ p15( X, X ) ] )
% 24.23/24.66 , clause( 14939, [ p51( c66, c67 ) ] )
% 24.23/24.66 , clause( 14940, [ p53( c68, f17( c66 ) ) ] )
% 24.23/24.66 , clause( 14941, [ ~( p16( f17( c66 ), c65 ) ) ] )
% 24.23/24.66 , clause( 14942, [ p10( f11( c62 ), f11( c60 ) ) ] )
% 24.23/24.66 , clause( 14943, [ p49( f4( c60 ), f4( c62 ) ) ] )
% 24.23/24.66 , clause( 14944, [ p3( f12( c62 ), f12( c60 ) ) ] )
% 24.23/24.66 , clause( 14945, [ p52( f20( f21( c62, c64 ) ), c66 ) ] )
% 24.23/24.66 , clause( 14946, [ p2( f22( c58, c60, c61 ), c62 ) ] )
% 24.23/24.66 , clause( 14947, [ p47( X ), ~( p47( Y ) ), ~( p2( Y, X ) ) ] )
% 24.23/24.66 , clause( 14948, [ p48( X ), ~( p48( Y ) ), ~( p2( Y, X ) ) ] )
% 24.23/24.66 , clause( 14949, [ p49( f4( c62 ), f13( f14( c63 ), f4( c60 ) ) ) ] )
% 24.23/24.66 , clause( 14950, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c60 ) ) ] )
% 24.23/24.66 , clause( 14951, [ p40( f41( X ), f41( Y ) ), ~( p15( X, Y ) ) ] )
% 24.23/24.66 , clause( 14952, [ p10( f11( X ), f11( Y ) ), ~( p2( X, Y ) ) ] )
% 24.23/24.66 , clause( 14953, [ p10( f31( X ), f31( Y ) ), ~( p30( X, Y ) ) ] )
% 24.23/24.66 , clause( 14954, [ p15( f38( X ), f38( Y ) ), ~( p15( X, Y ) ) ] )
% 24.23/24.66 , clause( 14955, [ p16( f17( X ), f17( Y ) ), ~( p15( X, Y ) ) ] )
% 24.23/24.66 , clause( 14956, [ p19( f20( X ), f20( Y ) ), ~( p18( X, Y ) ) ] )
% 24.23/24.66 , clause( 14957, [ p24( f39( X ), f39( Y ) ), ~( p15( X, Y ) ) ] )
% 24.23/24.66 , clause( 14958, [ p3( f12( X ), f12( Y ) ), ~( p2( X, Y ) ) ] )
% 24.23/24.66 , clause( 14959, [ p3( f14( X ), f14( Y ) ), ~( p3( X, Y ) ) ] )
% 24.23/24.66 , clause( 14960, [ p3( f37( X ), f37( Y ) ), ~( p36( X, Y ) ) ] )
% 24.23/24.66 , clause( 14961, [ p3( f4( X ), f4( Y ) ), ~( p2( X, Y ) ) ] )
% 24.23/24.66 , clause( 14962, [ p10( X, Y ), ~( p10( Z, X ) ), ~( p10( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14963, [ p7( X, Y ), ~( p7( Z, X ) ), ~( p7( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14964, [ p5( X, Y ), ~( p5( Z, X ) ), ~( p5( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14965, [ p42( X, Y ), ~( p42( Z, X ) ), ~( p42( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14966, [ p40( X, Y ), ~( p40( Z, X ) ), ~( p40( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14967, [ p36( X, Y ), ~( p36( Z, X ) ), ~( p36( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14968, [ p33( X, Y ), ~( p33( Z, X ) ), ~( p33( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14969, [ p32( X, Y ), ~( p32( Z, X ) ), ~( p32( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14970, [ p30( X, Y ), ~( p30( Z, X ) ), ~( p30( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14971, [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14972, [ p28( X, Y ), ~( p28( Z, X ) ), ~( p28( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14973, [ p26( X, Y ), ~( p26( Z, X ) ), ~( p26( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14974, [ p24( X, Y ), ~( p24( Z, X ) ), ~( p24( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14975, [ p23( X, Y ), ~( p23( Z, X ) ), ~( p23( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14976, [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14977, [ p19( X, Y ), ~( p19( Z, X ) ), ~( p19( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14978, [ p18( X, Y ), ~( p18( Z, X ) ), ~( p18( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14979, [ p16( X, Y ), ~( p16( Z, X ) ), ~( p16( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14980, [ p15( X, Y ), ~( p15( Z, X ) ), ~( p15( Z, Y ) ) ] )
% 24.23/24.66 , clause( 14981, [ p50( c66, f25( f27( c59, X ), c67 ), c62 ), ~( p53( X,
% 24.23/24.66 f17( c66 ) ) ) ] )
% 24.23/24.66 , clause( 14982, [ p57( X, Y ), ~( p5( Z, Y ) ), ~( p57( T, Z ) ), ~( p5( T
% 24.23/24.66 , X ) ) ] )
% 24.23/24.66 , clause( 14983, [ p45( X, Y ), ~( p5( Z, X ) ), ~( p5( T, Y ) ), ~( p45( Z
% 24.23/24.66 , T ) ) ] )
% 24.23/24.66 , clause( 14984, [ p46( X, Y ), ~( p46( Z, T ) ), ~( p7( Z, X ) ), ~( p3( T
% 24.23/24.66 , Y ) ) ] )
% 24.23/24.66 , clause( 14985, [ p49( X, Y ), ~( p3( Z, Y ) ), ~( p49( T, Z ) ), ~( p3( T
% 24.23/24.66 , X ) ) ] )
% 24.23/24.66 , clause( 14986, [ p51( X, Y ), ~( p24( Z, Y ) ), ~( p51( T, Z ) ), ~( p15(
% 24.23/24.66 T, X ) ) ] )
% 24.23/24.66 , clause( 14987, [ p52( X, Y ), ~( p19( Z, X ) ), ~( p52( Z, T ) ), ~( p15(
% 24.23/24.66 T, Y ) ) ] )
% 24.23/24.66 , clause( 14988, [ p53( X, Y ), ~( p26( Z, X ) ), ~( p53( Z, T ) ), ~( p16(
% 24.23/24.66 T, Y ) ) ] )
% 24.23/24.66 , clause( 14989, [ p54( X, Y ), ~( p30( Z, X ) ), ~( p54( Z, T ) ), ~( p28(
% 24.23/24.66 T, Y ) ) ] )
% 24.23/24.66 , clause( 14990, [ p55( X, Y ), ~( p5( Z, X ) ), ~( p55( Z, T ) ), ~( p10(
% 24.23/24.66 T, Y ) ) ] )
% 24.23/24.66 , clause( 14991, [ p56( X, Y ), ~( p36( Z, X ) ), ~( p56( Z, T ) ), ~( p33(
% 24.23/24.66 T, Y ) ) ] )
% 24.23/24.66 , clause( 14992, [ p45( X, c61 ), ~( p46( f8( f9( c58, X ), Y ), f4( f6(
% 24.23/24.66 c59, c60 ) ) ) ) ] )
% 24.23/24.66 , clause( 14993, [ p7( f8( X, Y ), f8( Z, T ) ), ~( p5( X, Z ) ), ~( p5( Y
% 24.23/24.66 , T ) ) ] )
% 24.23/24.66 , clause( 14994, [ p18( f21( X, Y ), f21( Z, T ) ), ~( p18( Y, T ) ), ~( p2(
% 24.23/24.66 X, Z ) ) ] )
% 24.23/24.66 , clause( 14995, [ p2( f6( X, Y ), f6( Z, T ) ), ~( p2( Y, T ) ), ~( p5( X
% 24.23/24.66 , Z ) ) ] )
% 24.23/24.66 , clause( 14996, [ p23( f27( X, Y ), f27( Z, T ) ), ~( p26( Y, T ) ), ~( p5(
% 24.23/24.66 X, Z ) ) ] )
% 24.23/24.66 , clause( 14997, [ p24( f25( X, Y ), f25( Z, T ) ), ~( p23( X, Z ) ), ~(
% 24.23/24.66 p24( Y, T ) ) ] )
% 24.23/24.66 , clause( 14998, [ p28( f29( X, Y ), f29( Z, T ) ), ~( p28( Y, T ) ), ~( p7(
% 24.23/24.66 X, Z ) ) ] )
% 24.23/24.66 , clause( 14999, [ p3( f13( X, Y ), f13( Z, T ) ), ~( p3( X, Z ) ), ~( p3(
% 24.23/24.66 Y, T ) ) ] )
% 24.23/24.66 , clause( 15000, [ p32( f35( X, Y ), f35( Z, T ) ), ~( p5( X, Z ) ), ~( p7(
% 24.23/24.66 Y, T ) ) ] )
% 24.23/24.66 , clause( 15001, [ p33( f34( X, Y ), f34( Z, T ) ), ~( p32( X, Z ) ), ~(
% 24.23/24.66 p33( Y, T ) ) ] )
% 24.23/24.66 , clause( 15002, [ p5( f9( X, Y ), f9( Z, T ) ), ~( p5( X, Z ) ), ~( p5( Y
% 24.23/24.66 , T ) ) ] )
% 24.23/24.66 , clause( 15003, [ p56( X, f34( f35( Y, Z ), T ) ), ~( p56( X, T ) ), ~(
% 24.23/24.66 p46( Z, f37( X ) ) ) ] )
% 24.23/24.66 , clause( 15004, [ p51( X, f25( f27( Y, Z ), T ) ), ~( p51( X, T ) ), ~(
% 24.23/24.66 p53( Z, f17( X ) ) ) ] )
% 24.23/24.66 , clause( 15005, [ p54( X, f29( f8( Y, Z ), T ) ), ~( p54( X, T ) ), ~( p55(
% 24.23/24.66 Z, f31( X ) ) ) ] )
% 24.23/24.66 , clause( 15006, [ p50( X, Y, Z ), ~( p15( T, X ) ), ~( p2( U, Z ) ), ~(
% 24.23/24.66 p24( W, Y ) ), ~( p50( T, W, U ) ) ] )
% 24.23/24.66 , clause( 15007, [ p2( f22( X, Y, Z ), f22( T, U, W ) ), ~( p5( X, T ) ),
% 24.23/24.66 ~( p5( Z, W ) ), ~( p2( Y, U ) ) ] )
% 24.23/24.66 , clause( 15008, [ p5( f43( X, Y, Z ), f43( T, U, W ) ), ~( p42( Z, W ) ),
% 24.23/24.66 ~( p5( Y, U ) ), ~( p15( X, T ) ) ] )
% 24.23/24.66 , clause( 15009, [ p26( f44( X, Y, Z ), f44( T, U, W ) ), ~( p42( Z, W ) )
% 24.23/24.66 , ~( p5( Y, U ) ), ~( p15( X, T ) ) ] )
% 24.23/24.66 , clause( 15010, [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p16( f17( f38(
% 24.23/24.66 X ) ), f17( X ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15011, [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p40( f41( f38(
% 24.23/24.66 X ) ), f41( X ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15012, [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p52( f20( f21(
% 24.23/24.66 c62, c64 ) ), f38( X ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15013, [ p16( f17( X ), c65 ), p16( f17( f38( X ) ), f17( X ) ),
% 24.23/24.66 ~( p50( X, f39( X ), c60 ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15014, [ p16( f17( X ), c65 ), p40( f41( f38( X ) ), f41( X ) ),
% 24.23/24.66 ~( p50( X, f39( X ), c60 ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15015, [ p16( f17( X ), c65 ), p50( X, Y, c60 ), ~( p51( X, Y ) )
% 24.23/24.66 , ~( p50( X, Y, c62 ) ), ~( p52( f20( f21( c62, c64 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15016, [ p16( f17( X ), c65 ), p52( f20( f21( c62, c64 ) ), f38(
% 24.23/24.66 X ) ), ~( p50( X, f39( X ), c60 ) ), ~( p52( f20( f21( c60, c64 ) ), X )
% 24.23/24.66 ) ] )
% 24.23/24.66 , clause( 15017, [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p50( f38( X )
% 24.23/24.66 , Y, c62 ), ~( p51( f38( X ), Y ) ), ~( p52( f20( f21( c60, c64 ) ), X )
% 24.23/24.66 ) ] )
% 24.23/24.66 , clause( 15018, [ p16( f17( X ), c65 ), p50( f38( X ), Y, c62 ), ~( p51(
% 24.23/24.66 f38( X ), Y ) ), ~( p50( X, f39( X ), c60 ) ), ~( p52( f20( f21( c60, c64
% 24.23/24.66 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15019, [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p57( c61, f43(
% 24.23/24.66 X, Y, Z ) ), p26( f44( f38( X ), Y, Z ), f44( X, Y, Z ) ), ~( p52( f20(
% 24.23/24.66 f21( c60, c64 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15020, [ p16( f17( X ), c65 ), p57( c61, f43( X, Y, Z ) ), p26(
% 24.23/24.66 f44( f38( X ), Y, Z ), f44( X, Y, Z ) ), ~( p50( X, f39( X ), c60 ) ),
% 24.23/24.66 ~( p52( f20( f21( c60, c64 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15021, [ p51( X, f39( X ) ), p16( f17( X ), c65 ), p5( Y, f9( c58
% 24.23/24.66 , f43( X, Y, Z ) ) ), p26( f44( f38( X ), Y, Z ), f44( X, Y, Z ) ), ~(
% 24.23/24.66 p52( f20( f21( c60, c64 ) ), X ) ) ] )
% 24.23/24.66 , clause( 15022, [ p16( f17( X ), c65 ), p5( Y, f9( c58, f43( X, Y, Z ) ) )
% 24.23/24.66 , p26( f44( f38( X ), Y, Z ), f44( X, Y, Z ) ), ~( p50( X, f39( X ), c60
% 24.23/24.66 ) ), ~( p52( f20( f21( c60, c64 ) ), X ) ) ] )
% 24.23/24.66 ] ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 14, [ p24( X, X ) ] )
% 24.23/24.66 , clause( 14932, [ p24( X, X ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 20, [ p15( X, X ) ] )
% 24.23/24.66 , clause( 14938, [ p15( X, X ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 21, [ p51( c66, c67 ) ] )
% 24.23/24.66 , clause( 14939, [ p51( c66, c67 ) ] )
% 24.23/24.66 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 22, [ p53( c68, f17( c66 ) ) ] )
% 24.23/24.66 , clause( 14940, [ p53( c68, f17( c66 ) ) ] )
% 24.23/24.66 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 23, [ ~( p16( f17( c66 ), c65 ) ) ] )
% 24.23/24.66 , clause( 14941, [ ~( p16( f17( c66 ), c65 ) ) ] )
% 24.23/24.66 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 27, [ p52( f20( f21( c62, c64 ) ), c66 ) ] )
% 24.23/24.66 , clause( 14945, [ p52( f20( f21( c62, c64 ) ), c66 ) ] )
% 24.23/24.66 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 32, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c60 ) ) ] )
% 24.23/24.66 , clause( 14950, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c60 ) ) ] )
% 24.23/24.66 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 56, [ ~( p24( Z, X ) ), ~( p24( Z, Y ) ), p24( X, Y ) ] )
% 24.23/24.66 , clause( 14974, [ p24( X, Y ), ~( p24( Z, X ) ), ~( p24( Z, Y ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 24.23/24.66 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2, 1 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 63, [ ~( p53( X, f17( c66 ) ) ), p50( c66, f25( f27( c59, X ), c67
% 24.23/24.66 ), c62 ) ] )
% 24.23/24.66 , clause( 14981, [ p50( c66, f25( f27( c59, X ), c67 ), c62 ), ~( p53( X,
% 24.23/24.66 f17( c66 ) ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 24.23/24.66 0 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T, Z
% 24.23/24.66 ) ) ] )
% 24.23/24.66 , clause( 14986, [ p51( X, Y ), ~( p24( Z, Y ) ), ~( p51( T, Z ) ), ~( p15(
% 24.23/24.66 T, X ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 24.23/24.66 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2, 3 ), ==>( 3, 1 )] )
% 24.23/24.66 ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 86, [ p51( X, f25( f27( Y, Z ), T ) ), ~( p51( X, T ) ), ~( p53( Z
% 24.23/24.66 , f17( X ) ) ) ] )
% 24.23/24.66 , clause( 15004, [ p51( X, f25( f27( Y, Z ), T ) ), ~( p51( X, T ) ), ~(
% 24.23/24.66 p53( Z, f17( X ) ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 24.23/24.66 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 97, [ p16( f17( X ), c65 ), ~( p51( X, Y ) ), ~( p50( X, Y, c62 ) )
% 24.23/24.66 , ~( p52( f20( f21( c62, c64 ) ), X ) ), p50( X, Y, c60 ) ] )
% 24.23/24.66 , clause( 15015, [ p16( f17( X ), c65 ), p50( X, Y, c60 ), ~( p51( X, Y ) )
% 24.23/24.66 , ~( p50( X, Y, c62 ) ), ~( p52( f20( f21( c62, c64 ) ), X ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 24.23/24.66 ), ==>( 1, 4 ), ==>( 2, 1 ), ==>( 3, 2 ), ==>( 4, 3 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15129, [ ~( p24( X, Y ) ), p24( Y, X ) ] )
% 24.23/24.66 , clause( 56, [ ~( p24( Z, X ) ), ~( p24( Z, Y ) ), p24( X, Y ) ] )
% 24.23/24.66 , 1, clause( 14, [ p24( X, X ) ] )
% 24.23/24.66 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, X )] ),
% 24.23/24.66 substitution( 1, [ :=( X, X )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 329, [ p24( Y, X ), ~( p24( X, Y ) ) ] )
% 24.23/24.66 , clause( 15129, [ ~( p24( X, Y ) ), p24( Y, X ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 1
% 24.23/24.66 ), ==>( 1, 0 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15130, [ ~( p24( c67, X ) ), ~( p15( c66, Y ) ), p51( Y, X ) ] )
% 24.23/24.66 , clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T
% 24.23/24.66 , Z ) ) ] )
% 24.23/24.66 , 3, clause( 21, [ p51( c66, c67 ) ] )
% 24.23/24.66 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, c67 ), :=( T, c66 )] )
% 24.23/24.66 , substitution( 1, [] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 512, [ ~( p15( c66, Y ) ), ~( p24( c67, X ) ), p51( Y, X ) ] )
% 24.23/24.66 , clause( 15130, [ ~( p24( c67, X ) ), ~( p15( c66, Y ) ), p51( Y, X ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 1
% 24.23/24.66 ), ==>( 1, 0 ), ==>( 2, 2 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15131, [ ~( p24( X, Y ) ), ~( p15( Z, T ) ), p51( T, Y ), ~( p15(
% 24.23/24.66 c66, Z ) ), ~( p24( c67, X ) ) ] )
% 24.23/24.66 , clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T
% 24.23/24.66 , Z ) ) ] )
% 24.23/24.66 , 3, clause( 512, [ ~( p15( c66, Y ) ), ~( p24( c67, X ) ), p51( Y, X ) ]
% 24.23/24.66 )
% 24.23/24.66 , 2, substitution( 0, [ :=( X, T ), :=( Y, Y ), :=( Z, X ), :=( T, Z )] ),
% 24.23/24.66 substitution( 1, [ :=( X, X ), :=( Y, Z )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 772, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( Y, Z ) ), ~(
% 24.23/24.66 p24( c67, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 , clause( 15131, [ ~( p24( X, Y ) ), ~( p15( Z, T ) ), p51( T, Y ), ~( p15(
% 24.23/24.66 c66, Z ) ), ~( p24( c67, X ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X ), :=( T, T )] ),
% 24.23/24.66 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 1 ), ==>( 2, 4 ), ==>( 3, 0 ),
% 24.23/24.66 ==>( 4, 3 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 factor(
% 24.23/24.66 clause( 15135, [ ~( p15( c66, c66 ) ), ~( p24( X, Y ) ), ~( p24( c67, X ) )
% 24.23/24.66 , p51( c66, Y ) ] )
% 24.23/24.66 , clause( 772, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( Y, Z ) ),
% 24.23/24.66 ~( p24( c67, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 , 0, 1, substitution( 0, [ :=( X, c66 ), :=( Y, X ), :=( Z, Y ), :=( T, c66
% 24.23/24.66 )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15138, [ ~( p24( X, Y ) ), ~( p24( c67, X ) ), p51( c66, Y ) ] )
% 24.23/24.66 , clause( 15135, [ ~( p15( c66, c66 ) ), ~( p24( X, Y ) ), ~( p24( c67, X )
% 24.23/24.66 ), p51( c66, Y ) ] )
% 24.23/24.66 , 0, clause( 20, [ p15( X, X ) ] )
% 24.23/24.66 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 24.23/24.66 , c66 )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 773, [ ~( p24( X, Y ) ), ~( p24( c67, X ) ), p51( c66, Y ) ] )
% 24.23/24.66 , clause( 15138, [ ~( p24( X, Y ) ), ~( p24( c67, X ) ), p51( c66, Y ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 24.23/24.66 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15140, [ ~( p24( X, Y ) ), ~( p15( c66, Z ) ), p51( Z, Y ), ~( p24(
% 24.23/24.66 T, X ) ), ~( p24( c67, T ) ) ] )
% 24.23/24.66 , clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T
% 24.23/24.66 , Z ) ) ] )
% 24.23/24.66 , 3, clause( 773, [ ~( p24( X, Y ) ), ~( p24( c67, X ) ), p51( c66, Y ) ]
% 24.23/24.66 )
% 24.23/24.66 , 2, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X ), :=( T, c66 )] )
% 24.23/24.66 , substitution( 1, [ :=( X, T ), :=( Y, X )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 775, [ ~( p15( c66, T ) ), ~( p24( c67, X ) ), ~( p24( Y, Z ) ),
% 24.23/24.66 ~( p24( X, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 , clause( 15140, [ ~( p24( X, Y ) ), ~( p15( c66, Z ) ), p51( Z, Y ), ~(
% 24.23/24.66 p24( T, X ) ), ~( p24( c67, T ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, T ), :=( T, X )] ),
% 24.23/24.66 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2, 4 ), ==>( 3, 3 ),
% 24.23/24.66 ==>( 4, 1 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 factor(
% 24.23/24.66 clause( 15145, [ ~( p15( c66, X ) ), ~( p24( c67, Y ) ), ~( p24( Y, c67 ) )
% 24.23/24.66 , p51( X, Y ) ] )
% 24.23/24.66 , clause( 775, [ ~( p15( c66, T ) ), ~( p24( c67, X ) ), ~( p24( Y, Z ) ),
% 24.23/24.66 ~( p24( X, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 , 1, 2, substitution( 0, [ :=( X, Y ), :=( Y, c67 ), :=( Z, Y ), :=( T, X )] )
% 24.23/24.66 ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15149, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, Y ), ~(
% 24.23/24.66 p24( Y, c67 ) ) ] )
% 24.23/24.66 , clause( 15145, [ ~( p15( c66, X ) ), ~( p24( c67, Y ) ), ~( p24( Y, c67 )
% 24.23/24.66 ), p51( X, Y ) ] )
% 24.23/24.66 , 1, clause( 329, [ p24( Y, X ), ~( p24( X, Y ) ) ] )
% 24.23/24.66 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 24.23/24.66 , Y ), :=( Y, c67 )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 factor(
% 24.23/24.66 clause( 15151, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, Y ) ] )
% 24.23/24.66 , clause( 15149, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, Y ), ~(
% 24.23/24.66 p24( Y, c67 ) ) ] )
% 24.23/24.66 , 1, 3, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 776, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, Y ) ] )
% 24.23/24.66 , clause( 15151, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, Y ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 24.23/24.66 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15153, [ ~( p24( X, Y ) ), ~( p15( Z, T ) ), p51( T, Y ), ~( p15(
% 24.23/24.66 c66, Z ) ), ~( p24( X, c67 ) ) ] )
% 24.23/24.66 , clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T
% 24.23/24.66 , Z ) ) ] )
% 24.23/24.66 , 3, clause( 776, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, Y ) ]
% 24.23/24.66 )
% 24.23/24.66 , 2, substitution( 0, [ :=( X, T ), :=( Y, Y ), :=( Z, X ), :=( T, Z )] ),
% 24.23/24.66 substitution( 1, [ :=( X, Z ), :=( Y, X )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 777, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( Y, Z ) ), ~(
% 24.23/24.66 p24( Y, c67 ) ), p51( T, Z ) ] )
% 24.23/24.66 , clause( 15153, [ ~( p24( X, Y ) ), ~( p15( Z, T ) ), p51( T, Y ), ~( p15(
% 24.23/24.66 c66, Z ) ), ~( p24( X, c67 ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X ), :=( T, T )] ),
% 24.23/24.66 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 1 ), ==>( 2, 4 ), ==>( 3, 0 ),
% 24.23/24.66 ==>( 4, 3 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 factor(
% 24.23/24.66 clause( 15157, [ ~( p15( c66, c66 ) ), ~( p24( X, Y ) ), ~( p24( X, c67 ) )
% 24.23/24.66 , p51( c66, Y ) ] )
% 24.23/24.66 , clause( 777, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( Y, Z ) ),
% 24.23/24.66 ~( p24( Y, c67 ) ), p51( T, Z ) ] )
% 24.23/24.66 , 0, 1, substitution( 0, [ :=( X, c66 ), :=( Y, X ), :=( Z, Y ), :=( T, c66
% 24.23/24.66 )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15160, [ ~( p24( X, Y ) ), ~( p24( X, c67 ) ), p51( c66, Y ) ] )
% 24.23/24.66 , clause( 15157, [ ~( p15( c66, c66 ) ), ~( p24( X, Y ) ), ~( p24( X, c67 )
% 24.23/24.66 ), p51( c66, Y ) ] )
% 24.23/24.66 , 0, clause( 20, [ p15( X, X ) ] )
% 24.23/24.66 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 24.23/24.66 , c66 )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 778, [ ~( p24( X, Y ) ), ~( p24( X, c67 ) ), p51( c66, Y ) ] )
% 24.23/24.66 , clause( 15160, [ ~( p24( X, Y ) ), ~( p24( X, c67 ) ), p51( c66, Y ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 24.23/24.66 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15162, [ ~( p24( X, Y ) ), ~( p15( c66, Z ) ), p51( Z, Y ), ~( p24(
% 24.23/24.66 T, X ) ), ~( p24( T, c67 ) ) ] )
% 24.23/24.66 , clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T
% 24.23/24.66 , Z ) ) ] )
% 24.23/24.66 , 3, clause( 778, [ ~( p24( X, Y ) ), ~( p24( X, c67 ) ), p51( c66, Y ) ]
% 24.23/24.66 )
% 24.23/24.66 , 2, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X ), :=( T, c66 )] )
% 24.23/24.66 , substitution( 1, [ :=( X, T ), :=( Y, X )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 788, [ ~( p15( c66, T ) ), ~( p24( X, c67 ) ), ~( p24( Y, Z ) ),
% 24.23/24.66 ~( p24( X, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 , clause( 15162, [ ~( p24( X, Y ) ), ~( p15( c66, Z ) ), p51( Z, Y ), ~(
% 24.23/24.66 p24( T, X ) ), ~( p24( T, c67 ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, T ), :=( T, X )] ),
% 24.23/24.66 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2, 4 ), ==>( 3, 3 ),
% 24.23/24.66 ==>( 4, 1 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 factor(
% 24.23/24.66 clause( 15167, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), ~( p24( Y, Y ) ),
% 24.23/24.66 p51( X, c67 ) ] )
% 24.23/24.66 , clause( 788, [ ~( p15( c66, T ) ), ~( p24( X, c67 ) ), ~( p24( Y, Z ) ),
% 24.23/24.66 ~( p24( X, Y ) ), p51( T, Z ) ] )
% 24.23/24.66 , 1, 2, substitution( 0, [ :=( X, Y ), :=( Y, Y ), :=( Z, c67 ), :=( T, X )] )
% 24.23/24.66 ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15171, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, c67 ) ] )
% 24.23/24.66 , clause( 15167, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), ~( p24( Y, Y ) )
% 24.23/24.66 , p51( X, c67 ) ] )
% 24.23/24.66 , 2, clause( 14, [ p24( X, X ) ] )
% 24.23/24.66 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 24.23/24.66 , Y )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 789, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, c67 ) ] )
% 24.23/24.66 , clause( 15171, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, c67 ) ]
% 24.23/24.66 )
% 24.23/24.66 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 24.23/24.66 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15172, [ ~( p24( c67, X ) ), ~( p15( Y, Z ) ), p51( Z, X ), ~( p15(
% 24.23/24.66 c66, Y ) ), ~( p24( T, c67 ) ) ] )
% 24.23/24.66 , clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T
% 24.23/24.66 , Z ) ) ] )
% 24.23/24.66 , 3, clause( 789, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), p51( X, c67 ) ]
% 24.23/24.66 )
% 24.23/24.66 , 2, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, c67 ), :=( T, Y )] )
% 24.23/24.66 , substitution( 1, [ :=( X, Y ), :=( Y, T )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 790, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( c67, Z ) ),
% 24.23/24.66 ~( p24( Y, c67 ) ), p51( T, Z ) ] )
% 24.23/24.66 , clause( 15172, [ ~( p24( c67, X ) ), ~( p15( Y, Z ) ), p51( Z, X ), ~(
% 24.23/24.66 p15( c66, Y ) ), ~( p24( T, c67 ) ) ] )
% 24.23/24.66 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, T ), :=( T, Y )] ),
% 24.23/24.66 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 1 ), ==>( 2, 4 ), ==>( 3, 0 ),
% 24.23/24.66 ==>( 4, 3 )] ) ).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 factor(
% 24.23/24.66 clause( 15176, [ ~( p15( c66, c66 ) ), ~( p24( c67, X ) ), ~( p24( Y, c67 )
% 24.23/24.66 ), p51( c66, X ) ] )
% 24.23/24.66 , clause( 790, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( c67, Z ) ),
% 24.23/24.66 ~( p24( Y, c67 ) ), p51( T, Z ) ] )
% 24.23/24.66 , 0, 1, substitution( 0, [ :=( X, c66 ), :=( Y, Y ), :=( Z, X ), :=( T, c66
% 24.23/24.66 )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 resolution(
% 24.23/24.66 clause( 15179, [ ~( p24( c67, X ) ), ~( p24( Y, c67 ) ), p51( c66, X ) ] )
% 24.23/24.66 , clause( 15176, [ ~( p15( c66, c66 ) ), ~( p24( c67, X ) ), ~( p24( Y, c67
% 24.23/24.66 ) ), p51( c66, X ) ] )
% 24.23/24.66 , 0, clause( 20, [ p15( X, X ) ] )
% 24.23/24.66 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 24.23/24.66 , c66 )] )).
% 24.23/24.66
% 24.23/24.66
% 24.23/24.66 subsumption(
% 24.23/24.66 clause( 791, [ ~( p24( c67, X ) ), ~( p24( Y, c67 ) ), p51( c66, X ) ] )
% 24.23/24.66 , clause( 15179, [ ~( p24( c67, X ) ), ~( p24( Y, c67 ) ), p51( c66, X ) ]
% 24.23/24.67 )
% 24.23/24.67 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 24.23/24.67 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15181, [ ~( p24( X, Y ) ), ~( p15( c66, Z ) ), p51( Z, Y ), ~( p24(
% 24.23/24.67 c67, X ) ), ~( p24( T, c67 ) ) ] )
% 24.23/24.67 , clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T
% 24.23/24.67 , Z ) ) ] )
% 24.23/24.67 , 3, clause( 791, [ ~( p24( c67, X ) ), ~( p24( Y, c67 ) ), p51( c66, X ) ]
% 24.23/24.67 )
% 24.23/24.67 , 2, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X ), :=( T, c66 )] )
% 24.23/24.67 , substitution( 1, [ :=( X, X ), :=( Y, T )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 792, [ ~( p15( c66, T ) ), ~( p24( Y, c67 ) ), ~( p24( X, Z ) ),
% 24.23/24.67 ~( p24( c67, X ) ), p51( T, Z ) ] )
% 24.23/24.67 , clause( 15181, [ ~( p24( X, Y ) ), ~( p15( c66, Z ) ), p51( Z, Y ), ~(
% 24.23/24.67 p24( c67, X ) ), ~( p24( T, c67 ) ) ] )
% 24.23/24.67 , substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, T ), :=( T, Y )] ),
% 24.23/24.67 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2, 4 ), ==>( 3, 3 ),
% 24.23/24.67 ==>( 4, 1 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 factor(
% 24.23/24.67 clause( 15186, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), ~( p24( c67, Y ) )
% 24.23/24.67 , p51( X, c67 ) ] )
% 24.23/24.67 , clause( 792, [ ~( p15( c66, T ) ), ~( p24( Y, c67 ) ), ~( p24( X, Z ) ),
% 24.23/24.67 ~( p24( c67, X ) ), p51( T, Z ) ] )
% 24.23/24.67 , 1, 2, substitution( 0, [ :=( X, Y ), :=( Y, Y ), :=( Z, c67 ), :=( T, X )] )
% 24.23/24.67 ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15189, [ ~( p15( c66, X ) ), ~( p24( c67, Y ) ), p51( X, c67 ), ~(
% 24.23/24.67 p24( c67, Y ) ) ] )
% 24.23/24.67 , clause( 15186, [ ~( p15( c66, X ) ), ~( p24( Y, c67 ) ), ~( p24( c67, Y )
% 24.23/24.67 ), p51( X, c67 ) ] )
% 24.23/24.67 , 1, clause( 329, [ p24( Y, X ), ~( p24( X, Y ) ) ] )
% 24.23/24.67 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 24.23/24.67 , c67 ), :=( Y, Y )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 factor(
% 24.23/24.67 clause( 15191, [ ~( p15( c66, X ) ), ~( p24( c67, Y ) ), p51( X, c67 ) ] )
% 24.23/24.67 , clause( 15189, [ ~( p15( c66, X ) ), ~( p24( c67, Y ) ), p51( X, c67 ),
% 24.23/24.67 ~( p24( c67, Y ) ) ] )
% 24.23/24.67 , 1, 3, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 793, [ ~( p15( c66, X ) ), ~( p24( c67, Y ) ), p51( X, c67 ) ] )
% 24.23/24.67 , clause( 15191, [ ~( p15( c66, X ) ), ~( p24( c67, Y ) ), p51( X, c67 ) ]
% 24.23/24.67 )
% 24.23/24.67 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 24.23/24.67 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15193, [ ~( p24( c67, X ) ), ~( p15( Y, Z ) ), p51( Z, X ), ~( p15(
% 24.23/24.67 c66, Y ) ), ~( p24( c67, T ) ) ] )
% 24.23/24.67 , clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T
% 24.23/24.67 , Z ) ) ] )
% 24.23/24.67 , 3, clause( 793, [ ~( p15( c66, X ) ), ~( p24( c67, Y ) ), p51( X, c67 ) ]
% 24.23/24.67 )
% 24.23/24.67 , 2, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, c67 ), :=( T, Y )] )
% 24.23/24.67 , substitution( 1, [ :=( X, Y ), :=( Y, T )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 794, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( c67, Z ) ),
% 24.23/24.67 ~( p24( c67, Y ) ), p51( T, Z ) ] )
% 24.23/24.67 , clause( 15193, [ ~( p24( c67, X ) ), ~( p15( Y, Z ) ), p51( Z, X ), ~(
% 24.23/24.67 p15( c66, Y ) ), ~( p24( c67, T ) ) ] )
% 24.23/24.67 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, T ), :=( T, Z )] ),
% 24.23/24.67 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 1 ), ==>( 2, 4 ), ==>( 3, 0 ),
% 24.23/24.67 ==>( 4, 2 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 factor(
% 24.23/24.67 clause( 15197, [ ~( p15( c66, X ) ), ~( p15( X, Y ) ), ~( p24( c67, Z ) ),
% 24.23/24.67 p51( Y, Z ) ] )
% 24.23/24.67 , clause( 794, [ ~( p15( c66, X ) ), ~( p15( X, T ) ), ~( p24( c67, Z ) ),
% 24.23/24.67 ~( p24( c67, Y ) ), p51( T, Z ) ] )
% 24.23/24.67 , 2, 3, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Z ), :=( T, Y )] )
% 24.23/24.67 ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 796, [ ~( p15( c66, X ) ), ~( p15( X, Y ) ), ~( p24( c67, Z ) ),
% 24.23/24.67 p51( Y, Z ) ] )
% 24.23/24.67 , clause( 15197, [ ~( p15( c66, X ) ), ~( p15( X, Y ) ), ~( p24( c67, Z ) )
% 24.23/24.67 , p51( Y, Z ) ] )
% 24.23/24.67 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 24.23/24.67 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 3 )] )
% 24.23/24.67 ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 factor(
% 24.23/24.67 clause( 15199, [ ~( p15( c66, c66 ) ), ~( p24( c67, X ) ), p51( c66, X ) ]
% 24.23/24.67 )
% 24.23/24.67 , clause( 796, [ ~( p15( c66, X ) ), ~( p15( X, Y ) ), ~( p24( c67, Z ) ),
% 24.23/24.67 p51( Y, Z ) ] )
% 24.23/24.67 , 0, 1, substitution( 0, [ :=( X, c66 ), :=( Y, c66 ), :=( Z, X )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15200, [ ~( p24( c67, X ) ), p51( c66, X ) ] )
% 24.23/24.67 , clause( 15199, [ ~( p15( c66, c66 ) ), ~( p24( c67, X ) ), p51( c66, X )
% 24.23/24.67 ] )
% 24.23/24.67 , 0, clause( 20, [ p15( X, X ) ] )
% 24.23/24.67 , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, c66 )] )
% 24.23/24.67 ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 797, [ ~( p24( c67, X ) ), p51( c66, X ) ] )
% 24.23/24.67 , clause( 15200, [ ~( p24( c67, X ) ), p51( c66, X ) ] )
% 24.23/24.67 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 24.23/24.67 1 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15201, [ ~( p24( X, Y ) ), ~( p15( c66, Z ) ), p51( Z, Y ), ~( p24(
% 24.23/24.67 c67, X ) ) ] )
% 24.23/24.67 , clause( 68, [ ~( p24( Z, Y ) ), ~( p15( T, X ) ), p51( X, Y ), ~( p51( T
% 24.23/24.67 , Z ) ) ] )
% 24.23/24.67 , 3, clause( 797, [ ~( p24( c67, X ) ), p51( c66, X ) ] )
% 24.23/24.67 , 1, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X ), :=( T, c66 )] )
% 24.23/24.67 , substitution( 1, [ :=( X, X )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 805, [ ~( p15( c66, Z ) ), ~( p24( X, Y ) ), ~( p24( c67, X ) ),
% 24.23/24.67 p51( Z, Y ) ] )
% 24.23/24.67 , clause( 15201, [ ~( p24( X, Y ) ), ~( p15( c66, Z ) ), p51( Z, Y ), ~(
% 24.23/24.67 p24( c67, X ) ) ] )
% 24.23/24.67 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 24.23/24.67 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2, 3 ), ==>( 3, 2 )] )
% 24.23/24.67 ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 factor(
% 24.23/24.67 clause( 15203, [ ~( p15( c66, X ) ), ~( p24( c67, c67 ) ), p51( X, c67 ) ]
% 24.23/24.67 )
% 24.23/24.67 , clause( 805, [ ~( p15( c66, Z ) ), ~( p24( X, Y ) ), ~( p24( c67, X ) ),
% 24.23/24.67 p51( Z, Y ) ] )
% 24.23/24.67 , 1, 2, substitution( 0, [ :=( X, c67 ), :=( Y, c67 ), :=( Z, X )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15204, [ ~( p15( c66, X ) ), p51( X, c67 ) ] )
% 24.23/24.67 , clause( 15203, [ ~( p15( c66, X ) ), ~( p24( c67, c67 ) ), p51( X, c67 )
% 24.23/24.67 ] )
% 24.23/24.67 , 1, clause( 14, [ p24( X, X ) ] )
% 24.23/24.67 , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, c67 )] )
% 24.23/24.67 ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 806, [ ~( p15( c66, X ) ), p51( X, c67 ) ] )
% 24.23/24.67 , clause( 15204, [ ~( p15( c66, X ) ), p51( X, c67 ) ] )
% 24.23/24.67 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 24.23/24.67 1 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15205, [ p51( c66, f25( f27( X, c68 ), Y ) ), ~( p51( c66, Y ) ) ]
% 24.23/24.67 )
% 24.23/24.67 , clause( 86, [ p51( X, f25( f27( Y, Z ), T ) ), ~( p51( X, T ) ), ~( p53(
% 24.23/24.67 Z, f17( X ) ) ) ] )
% 24.23/24.67 , 2, clause( 22, [ p53( c68, f17( c66 ) ) ] )
% 24.23/24.67 , 0, substitution( 0, [ :=( X, c66 ), :=( Y, X ), :=( Z, c68 ), :=( T, Y )] )
% 24.23/24.67 , substitution( 1, [] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 1014, [ ~( p51( c66, Y ) ), p51( c66, f25( f27( X, c68 ), Y ) ) ]
% 24.23/24.67 )
% 24.23/24.67 , clause( 15205, [ p51( c66, f25( f27( X, c68 ), Y ) ), ~( p51( c66, Y ) )
% 24.23/24.67 ] )
% 24.23/24.67 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 1
% 24.23/24.67 ), ==>( 1, 0 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15206, [ p16( f17( c66 ), c65 ), ~( p51( c66, f25( f27( c59, c68 )
% 24.23/24.67 , c67 ) ) ), ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62 ) ), ~( p52(
% 24.23/24.67 f20( f21( c62, c64 ) ), c66 ) ) ] )
% 24.23/24.67 , clause( 32, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c60 ) ) ] )
% 24.23/24.67 , 0, clause( 97, [ p16( f17( X ), c65 ), ~( p51( X, Y ) ), ~( p50( X, Y,
% 24.23/24.67 c62 ) ), ~( p52( f20( f21( c62, c64 ) ), X ) ), p50( X, Y, c60 ) ] )
% 24.23/24.67 , 4, substitution( 0, [] ), substitution( 1, [ :=( X, c66 ), :=( Y, f25(
% 24.23/24.67 f27( c59, c68 ), c67 ) )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15207, [ ~( p51( c66, f25( f27( c59, c68 ), c67 ) ) ), ~( p50( c66
% 24.23/24.67 , f25( f27( c59, c68 ), c67 ), c62 ) ), ~( p52( f20( f21( c62, c64 ) ),
% 24.23/24.67 c66 ) ) ] )
% 24.23/24.67 , clause( 23, [ ~( p16( f17( c66 ), c65 ) ) ] )
% 24.23/24.67 , 0, clause( 15206, [ p16( f17( c66 ), c65 ), ~( p51( c66, f25( f27( c59,
% 24.23/24.67 c68 ), c67 ) ) ), ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62 ) ), ~(
% 24.23/24.67 p52( f20( f21( c62, c64 ) ), c66 ) ) ] )
% 24.23/24.67 , 0, substitution( 0, [] ), substitution( 1, [] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 1410, [ ~( p51( c66, f25( f27( c59, c68 ), c67 ) ) ), ~( p52( f20(
% 24.23/24.67 f21( c62, c64 ) ), c66 ) ), ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62
% 24.23/24.67 ) ) ] )
% 24.23/24.67 , clause( 15207, [ ~( p51( c66, f25( f27( c59, c68 ), c67 ) ) ), ~( p50(
% 24.23/24.67 c66, f25( f27( c59, c68 ), c67 ), c62 ) ), ~( p52( f20( f21( c62, c64 ) )
% 24.23/24.67 , c66 ) ) ] )
% 24.23/24.67 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 2 ), ==>( 2
% 24.23/24.67 , 1 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15208, [ p51( c66, f25( f27( X, c68 ), c67 ) ), ~( p15( c66, c66 )
% 24.23/24.67 ) ] )
% 24.23/24.67 , clause( 1014, [ ~( p51( c66, Y ) ), p51( c66, f25( f27( X, c68 ), Y ) ) ]
% 24.23/24.67 )
% 24.23/24.67 , 0, clause( 806, [ ~( p15( c66, X ) ), p51( X, c67 ) ] )
% 24.23/24.67 , 1, substitution( 0, [ :=( X, X ), :=( Y, c67 )] ), substitution( 1, [
% 24.23/24.67 :=( X, c66 )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15209, [ p51( c66, f25( f27( X, c68 ), c67 ) ) ] )
% 24.23/24.67 , clause( 15208, [ p51( c66, f25( f27( X, c68 ), c67 ) ), ~( p15( c66, c66
% 24.23/24.67 ) ) ] )
% 24.23/24.67 , 1, clause( 20, [ p15( X, X ) ] )
% 24.23/24.67 , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, c66 )] )
% 24.23/24.67 ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 2032, [ p51( c66, f25( f27( X, c68 ), c67 ) ) ] )
% 24.23/24.67 , clause( 15209, [ p51( c66, f25( f27( X, c68 ), c67 ) ) ] )
% 24.23/24.67 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15210, [ ~( p52( f20( f21( c62, c64 ) ), c66 ) ), ~( p50( c66, f25(
% 24.23/24.67 f27( c59, c68 ), c67 ), c62 ) ) ] )
% 24.23/24.67 , clause( 1410, [ ~( p51( c66, f25( f27( c59, c68 ), c67 ) ) ), ~( p52( f20(
% 24.23/24.67 f21( c62, c64 ) ), c66 ) ), ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62
% 24.23/24.67 ) ) ] )
% 24.23/24.67 , 0, clause( 2032, [ p51( c66, f25( f27( X, c68 ), c67 ) ) ] )
% 24.23/24.67 , 0, substitution( 0, [] ), substitution( 1, [ :=( X, c59 )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15211, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62 ) ) ] )
% 24.23/24.67 , clause( 15210, [ ~( p52( f20( f21( c62, c64 ) ), c66 ) ), ~( p50( c66,
% 24.23/24.67 f25( f27( c59, c68 ), c67 ), c62 ) ) ] )
% 24.23/24.67 , 0, clause( 27, [ p52( f20( f21( c62, c64 ) ), c66 ) ] )
% 24.23/24.67 , 0, substitution( 0, [] ), substitution( 1, [] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 14915, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62 ) ) ] )
% 24.23/24.67 , clause( 15211, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62 ) ) ] )
% 24.23/24.67 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15212, [ ~( p53( c68, f17( c66 ) ) ) ] )
% 24.23/24.67 , clause( 14915, [ ~( p50( c66, f25( f27( c59, c68 ), c67 ), c62 ) ) ] )
% 24.23/24.67 , 0, clause( 63, [ ~( p53( X, f17( c66 ) ) ), p50( c66, f25( f27( c59, X )
% 24.23/24.67 , c67 ), c62 ) ] )
% 24.23/24.67 , 1, substitution( 0, [] ), substitution( 1, [ :=( X, c68 )] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 resolution(
% 24.23/24.67 clause( 15213, [] )
% 24.23/24.67 , clause( 15212, [ ~( p53( c68, f17( c66 ) ) ) ] )
% 24.23/24.67 , 0, clause( 22, [ p53( c68, f17( c66 ) ) ] )
% 24.23/24.67 , 0, substitution( 0, [] ), substitution( 1, [] )).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 subsumption(
% 24.23/24.67 clause( 14916, [] )
% 24.23/24.67 , clause( 15213, [] )
% 24.23/24.67 , substitution( 0, [] ), permutation( 0, [] ) ).
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 end.
% 24.23/24.67
% 24.23/24.67 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 24.23/24.67
% 24.23/24.67 Memory use:
% 24.23/24.67
% 24.23/24.67 space for terms: 249121
% 24.23/24.67 space for clauses: 603581
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 clauses generated: 595370
% 24.23/24.67 clauses kept: 14917
% 24.23/24.67 clauses selected: 2537
% 24.23/24.67 clauses deleted: 17
% 24.23/24.67 clauses inuse deleted: 7
% 24.23/24.67
% 24.23/24.67 subsentry: 12932108
% 24.23/24.67 literals s-matched: 5363348
% 24.23/24.67 literals matched: 4609147
% 24.23/24.67 full subsumption: 4211321
% 24.23/24.67
% 24.23/24.67 checksum: -1545808237
% 24.23/24.67
% 24.23/24.67
% 24.23/24.67 Bliksem ended
%------------------------------------------------------------------------------