%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SEU373+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n019.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 : Tue Jul 19 07:12:53 EDT 2022
% Result : Theorem 0.83s 1.33s
% Output : Refutation 0.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.14/0.14 % Problem : SEU373+1 : TPTP v8.1.0. Released v3.3.0.
% 0.14/0.15 % Command : bliksem %s
% 0.15/0.36 % Computer : n019.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % DateTime : Mon Jun 20 02:04:39 EDT 2022
% 0.15/0.36 % CPUTime :
% 0.83/1.19 *** allocated 10000 integers for termspace/termends
% 0.83/1.19 *** allocated 10000 integers for clauses
% 0.83/1.19 *** allocated 10000 integers for justifications
% 0.83/1.19 Bliksem 1.12
% 0.83/1.19
% 0.83/1.19
% 0.83/1.19 Automatic Strategy Selection
% 0.83/1.19
% 0.83/1.19
% 0.83/1.19 Clauses:
% 0.83/1.19
% 0.83/1.19 { ! in( X, Y ), ! in( Y, X ) }.
% 0.83/1.19 { ! empty( X ), function( X ) }.
% 0.83/1.19 { ! empty( X ), relation( X ) }.
% 0.83/1.19 { ! element( X, powerset( cartesian_product2( Y, Z ) ) ), relation( X ) }.
% 0.83/1.19 { ! relation( X ), ! empty( X ), ! function( X ), relation( X ) }.
% 0.83/1.19 { ! relation( X ), ! empty( X ), ! function( X ), function( X ) }.
% 0.83/1.19 { ! relation( X ), ! empty( X ), ! function( X ), one_to_one( X ) }.
% 0.83/1.19 { ! rel_str( X ), ! rel_str( Y ), ! subrelstr( Y, X ), subset( the_carrier
% 0.83/1.19 ( Y ), the_carrier( X ) ) }.
% 0.83/1.19 { ! rel_str( X ), ! rel_str( Y ), ! subrelstr( Y, X ), subset(
% 0.83/1.19 the_InternalRel( Y ), the_InternalRel( X ) ) }.
% 0.83/1.19 { ! rel_str( X ), ! rel_str( Y ), ! subset( the_carrier( Y ), the_carrier(
% 0.83/1.19 X ) ), ! subset( the_InternalRel( Y ), the_InternalRel( X ) ), subrelstr
% 0.83/1.19 ( Y, X ) }.
% 0.83/1.19 { ! one_sorted_str( X ), ! net_str( Y, X ), ! net_str( Z, X ), ! subnetstr
% 0.83/1.19 ( Z, X, Y ), subrelstr( Z, Y ) }.
% 0.83/1.19 { ! one_sorted_str( X ), ! net_str( Y, X ), ! net_str( Z, X ), ! subnetstr
% 0.83/1.19 ( Z, X, Y ), the_mapping( X, Z ) = relation_dom_restr_as_relation_of(
% 0.83/1.19 the_carrier( Y ), the_carrier( X ), the_mapping( X, Y ), the_carrier( Z )
% 0.83/1.19 ) }.
% 0.83/1.19 { ! one_sorted_str( X ), ! net_str( Y, X ), ! net_str( Z, X ), ! subrelstr
% 0.83/1.19 ( Z, Y ), ! the_mapping( X, Z ) = relation_dom_restr_as_relation_of(
% 0.83/1.19 the_carrier( Y ), the_carrier( X ), the_mapping( X, Y ), the_carrier( Z )
% 0.83/1.19 ), subnetstr( Z, X, Y ) }.
% 0.83/1.19 { && }.
% 0.83/1.19 { && }.
% 0.83/1.19 { && }.
% 0.83/1.19 { ! relation( X ), relation( relation_dom_restriction( X, Y ) ) }.
% 0.83/1.19 { ! relation_of2( Z, X, Y ), relation_of2_as_subset(
% 0.83/1.19 relation_dom_restr_as_relation_of( X, Y, Z, T ), X, Y ) }.
% 0.83/1.19 { ! rel_str( X ), one_sorted_str( X ) }.
% 0.83/1.19 { && }.
% 0.83/1.19 { ! one_sorted_str( X ), ! net_str( Y, X ), rel_str( Y ) }.
% 0.83/1.19 { && }.
% 0.83/1.19 { && }.
% 0.83/1.19 { ! rel_str( X ), ! subrelstr( Y, X ), rel_str( Y ) }.
% 0.83/1.19 { ! one_sorted_str( X ), ! net_str( Y, X ), ! subnetstr( Z, X, Y ), net_str
% 0.83/1.19 ( Z, X ) }.
% 0.83/1.19 { ! relation_of2_as_subset( Z, X, Y ), element( Z, powerset(
% 0.83/1.19 cartesian_product2( X, Y ) ) ) }.
% 0.83/1.19 { ! rel_str( X ), relation_of2_as_subset( the_InternalRel( X ), the_carrier
% 0.83/1.19 ( X ), the_carrier( X ) ) }.
% 0.83/1.19 { && }.
% 0.83/1.19 { ! one_sorted_str( X ), ! net_str( Y, X ), function( the_mapping( X, Y ) )
% 0.83/1.19 }.
% 0.83/1.19 { ! one_sorted_str( X ), ! net_str( Y, X ), quasi_total( the_mapping( X, Y
% 0.83/1.19 ), the_carrier( Y ), the_carrier( X ) ) }.
% 0.83/1.19 { ! one_sorted_str( X ), ! net_str( Y, X ), relation_of2_as_subset(
% 0.83/1.19 the_mapping( X, Y ), the_carrier( Y ), the_carrier( X ) ) }.
% 0.83/1.19 { rel_str( skol1 ) }.
% 0.83/1.19 { one_sorted_str( skol2 ) }.
% 0.83/1.19 { ! one_sorted_str( X ), net_str( skol3( X ), X ) }.
% 0.83/1.19 { relation_of2( skol4( X, Y ), X, Y ) }.
% 0.83/1.19 { element( skol5( X ), X ) }.
% 0.83/1.19 { ! rel_str( X ), subrelstr( skol6( X ), X ) }.
% 0.83/1.19 { ! one_sorted_str( X ), ! net_str( Y, X ), subnetstr( skol7( X, Y ), X, Y
% 0.83/1.19 ) }.
% 0.83/1.19 { relation_of2_as_subset( skol8( X, Y ), X, Y ) }.
% 0.83/1.19 { empty( empty_set ) }.
% 0.83/1.19 { relation( empty_set ) }.
% 0.83/1.19 { relation_empty_yielding( empty_set ) }.
% 0.83/1.19 { ! relation( X ), ! relation_empty_yielding( X ), relation(
% 0.83/1.19 relation_dom_restriction( X, Y ) ) }.
% 0.83/1.19 { ! relation( X ), ! relation_empty_yielding( X ), relation_empty_yielding
% 0.83/1.19 ( relation_dom_restriction( X, Y ) ) }.
% 0.83/1.19 { ! empty( powerset( X ) ) }.
% 0.83/1.19 { ! relation( X ), ! function( X ), relation( relation_dom_restriction( X,
% 0.83/1.19 Y ) ) }.
% 0.83/1.19 { ! relation( X ), ! function( X ), function( relation_dom_restriction( X,
% 0.83/1.19 Y ) ) }.
% 0.83/1.19 { empty( empty_set ) }.
% 0.83/1.19 { relation( empty_set ) }.
% 0.83/1.19 { empty( X ), empty( Y ), ! empty( cartesian_product2( X, Y ) ) }.
% 0.83/1.19 { relation( skol9 ) }.
% 0.83/1.19 { function( skol9 ) }.
% 0.83/1.19 { relation( skol10 ) }.
% 0.83/1.19 { relation_empty_yielding( skol10 ) }.
% 0.83/1.19 { function( skol10 ) }.
% 0.83/1.19 { empty( skol11 ) }.
% 0.83/1.19 { relation( skol11 ) }.
% 0.83/1.19 { empty( X ), ! empty( skol12( Y ) ) }.
% 0.83/1.19 { empty( X ), element( skol12( X ), powerset( X ) ) }.
% 0.83/1.19 { relation( skol13 ) }.
% 0.83/1.19 { empty( skol13 ) }.
% 0.83/1.19 { function( skol13 ) }.
% 0.83/1.19 { ! empty( skol14 ) }.
% 0.83/1.19 { relation( skol14 ) }.
% 0.83/1.19 { empty( skol15( Y ) ) }.
% 0.83/1.19 { element( skol15( X ), powerset( X ) ) }.
% 0.83/1.19 { relation( skol16 ) }.
% 0.83/1.19 { function( skol16 ) }.
% 0.83/1.19 { one_to_one( skol16 ) }.
% 0.83/1.33 { relation( skol17 ) }.
% 0.83/1.33 { relation_empty_yielding( skol17 ) }.
% 0.83/1.33 { relation( skol18 ) }.
% 0.83/1.33 { relation_empty_yielding( skol18 ) }.
% 0.83/1.33 { function( skol18 ) }.
% 0.83/1.33 { ! relation_of2( Z, X, Y ), relation_dom_restr_as_relation_of( X, Y, Z, T
% 0.83/1.33 ) = relation_dom_restriction( Z, T ) }.
% 0.83/1.33 { ! relation_of2_as_subset( Z, X, Y ), relation_of2( Z, X, Y ) }.
% 0.83/1.33 { ! relation_of2( Z, X, Y ), relation_of2_as_subset( Z, X, Y ) }.
% 0.83/1.33 { subset( X, X ) }.
% 0.83/1.33 { one_sorted_str( skol19 ) }.
% 0.83/1.33 { net_str( skol20, skol19 ) }.
% 0.83/1.33 { subnetstr( skol21, skol19, skol20 ) }.
% 0.83/1.33 { ! subset( the_carrier( skol21 ), the_carrier( skol20 ) ) }.
% 0.83/1.33 { ! in( X, Y ), element( X, Y ) }.
% 0.83/1.33 { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 0.83/1.33 { ! element( X, powerset( Y ) ), subset( X, Y ) }.
% 0.83/1.33 { ! subset( X, Y ), element( X, powerset( Y ) ) }.
% 0.83/1.33 { ! in( X, Z ), ! element( Z, powerset( Y ) ), element( X, Y ) }.
% 0.83/1.33 { ! in( X, Y ), ! element( Y, powerset( Z ) ), ! empty( Z ) }.
% 0.83/1.33 { ! empty( X ), X = empty_set }.
% 0.83/1.33 { ! in( X, Y ), ! empty( Y ) }.
% 0.83/1.33 { ! empty( X ), X = Y, ! empty( Y ) }.
% 0.83/1.33
% 0.83/1.33 percentage equality = 0.032258, percentage horn = 0.962025
% 0.83/1.33 This is a problem with some equality
% 0.83/1.33
% 0.83/1.33
% 0.83/1.33
% 0.83/1.33 Options Used:
% 0.83/1.33
% 0.83/1.33 useres = 1
% 0.83/1.33 useparamod = 1
% 0.83/1.33 useeqrefl = 1
% 0.83/1.33 useeqfact = 1
% 0.83/1.33 usefactor = 1
% 0.83/1.33 usesimpsplitting = 0
% 0.83/1.33 usesimpdemod = 5
% 0.83/1.33 usesimpres = 3
% 0.83/1.33
% 0.83/1.33 resimpinuse = 1000
% 0.83/1.33 resimpclauses = 20000
% 0.83/1.33 substype = eqrewr
% 0.83/1.33 backwardsubs = 1
% 0.83/1.33 selectoldest = 5
% 0.83/1.33
% 0.83/1.33 litorderings [0] = split
% 0.83/1.33 litorderings [1] = extend the termordering, first sorting on arguments
% 0.83/1.33
% 0.83/1.33 termordering = kbo
% 0.83/1.33
% 0.83/1.33 litapriori = 0
% 0.83/1.33 termapriori = 1
% 0.83/1.33 litaposteriori = 0
% 0.83/1.33 termaposteriori = 0
% 0.83/1.33 demodaposteriori = 0
% 0.83/1.33 ordereqreflfact = 0
% 0.83/1.33
% 0.83/1.33 litselect = negord
% 0.83/1.33
% 0.83/1.33 maxweight = 15
% 0.83/1.33 maxdepth = 30000
% 0.83/1.33 maxlength = 115
% 0.83/1.33 maxnrvars = 195
% 0.83/1.33 excuselevel = 1
% 0.83/1.33 increasemaxweight = 1
% 0.83/1.33
% 0.83/1.33 maxselected = 10000000
% 0.83/1.33 maxnrclauses = 10000000
% 0.83/1.33
% 0.83/1.33 showgenerated = 0
% 0.83/1.33 showkept = 0
% 0.83/1.33 showselected = 0
% 0.83/1.33 showdeleted = 0
% 0.83/1.33 showresimp = 1
% 0.83/1.33 showstatus = 2000
% 0.83/1.33
% 0.83/1.33 prologoutput = 0
% 0.83/1.33 nrgoals = 5000000
% 0.83/1.33 totalproof = 1
% 0.83/1.33
% 0.83/1.33 Symbols occurring in the translation:
% 0.83/1.33
% 0.83/1.33 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.83/1.33 . [1, 2] (w:1, o:44, a:1, s:1, b:0),
% 0.83/1.33 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 0.83/1.33 ! [4, 1] (w:0, o:24, a:1, s:1, b:0),
% 0.83/1.33 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.83/1.33 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.83/1.33 in [37, 2] (w:1, o:68, a:1, s:1, b:0),
% 0.83/1.33 empty [38, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.83/1.33 function [39, 1] (w:1, o:30, a:1, s:1, b:0),
% 0.83/1.33 relation [40, 1] (w:1, o:31, a:1, s:1, b:0),
% 0.83/1.33 cartesian_product2 [42, 2] (w:1, o:69, a:1, s:1, b:0),
% 0.83/1.33 powerset [43, 1] (w:1, o:34, a:1, s:1, b:0),
% 0.83/1.33 element [44, 2] (w:1, o:70, a:1, s:1, b:0),
% 0.83/1.33 one_to_one [45, 1] (w:1, o:33, a:1, s:1, b:0),
% 0.83/1.33 rel_str [46, 1] (w:1, o:35, a:1, s:1, b:0),
% 0.83/1.33 subrelstr [47, 2] (w:1, o:72, a:1, s:1, b:0),
% 0.83/1.33 the_carrier [48, 1] (w:1, o:41, a:1, s:1, b:0),
% 0.83/1.33 subset [49, 2] (w:1, o:73, a:1, s:1, b:0),
% 0.83/1.33 the_InternalRel [50, 1] (w:1, o:42, a:1, s:1, b:0),
% 0.83/1.33 one_sorted_str [51, 1] (w:1, o:32, a:1, s:1, b:0),
% 0.83/1.33 net_str [52, 2] (w:1, o:74, a:1, s:1, b:0),
% 0.83/1.33 subnetstr [53, 3] (w:1, o:82, a:1, s:1, b:0),
% 0.83/1.33 the_mapping [54, 2] (w:1, o:78, a:1, s:1, b:0),
% 0.83/1.33 relation_dom_restr_as_relation_of [55, 4] (w:1, o:83, a:1, s:1, b:0)
% 0.83/1.33 ,
% 0.83/1.33 relation_dom_restriction [56, 2] (w:1, o:71, a:1, s:1, b:0),
% 0.83/1.33 relation_of2 [58, 3] (w:1, o:80, a:1, s:1, b:0),
% 0.83/1.33 relation_of2_as_subset [59, 3] (w:1, o:81, a:1, s:1, b:0),
% 0.83/1.33 quasi_total [60, 3] (w:1, o:79, a:1, s:1, b:0),
% 0.83/1.33 empty_set [61, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.83/1.33 relation_empty_yielding [62, 1] (w:1, o:43, a:1, s:1, b:0),
% 0.83/1.33 skol1 [63, 0] (w:1, o:11, a:1, s:1, b:1),
% 0.83/1.33 skol2 [64, 0] (w:1, o:20, a:1, s:1, b:1),
% 0.83/1.33 skol3 [65, 1] (w:1, o:36, a:1, s:1, b:1),
% 0.83/1.33 skol4 [66, 2] (w:1, o:75, a:1, s:1, b:1),
% 0.83/1.33 skol5 [67, 1] (w:1, o:37, a:1, s:1, b:1),
% 0.83/1.33 skol6 [68, 1] (w:1, o:38, a:1, s:1, b:1),
% 0.83/1.33 skol7 [69, 2] (w:1, o:76, a:1, s:1, b:1),
% 0.83/1.33 skol8 [70, 2] (w:1, o:77, a:1, s:1, b:1),
% 0.83/1.33 skol9 [71, 0] (w:1, o:21, a:1, s:1, b:1),
% 0.83/1.33 skol10 [72, 0] (w:1, o:12, a:1, s:1, b:1),
% 0.83/1.33 skol11 [73, 0] (w:1, o:13, a:1, s:1, b:1),
% 0.83/1.33 skol12 [74, 1] (w:1, o:39, a:1, s:1, b:1),
% 0.83/1.33 skol13 [75, 0] (w:1, o:14, a:1, s:1, b:1),
% 0.83/1.33 skol14 [76, 0] (w:1, o:15, a:1, s:1, b:1),
% 0.83/1.33 skol15 [77, 1] (w:1, o:40, a:1, s:1, b:1),
% 0.83/1.33 skol16 [78, 0] (w:1, o:16, a:1, s:1, b:1),
% 0.83/1.33 skol17 [79, 0] (w:1, o:17, a:1, s:1, b:1),
% 0.83/1.33 skol18 [80, 0] (w:1, o:18, a:1, s:1, b:1),
% 0.83/1.33 skol19 [81, 0] (w:1, o:19, a:1, s:1, b:1),
% 0.83/1.33 skol20 [82, 0] (w:1, o:22, a:1, s:1, b:1),
% 0.83/1.33 skol21 [83, 0] (w:1, o:23, a:1, s:1, b:1).
% 0.83/1.33
% 0.83/1.33
% 0.83/1.33 Starting Search:
% 0.83/1.33
% 0.83/1.33 *** allocated 15000 integers for clauses
% 0.83/1.33 *** allocated 22500 integers for clauses
% 0.83/1.33 *** allocated 33750 integers for clauses
% 0.83/1.33 *** allocated 50625 integers for clauses
% 0.83/1.33 *** allocated 15000 integers for termspace/termends
% 0.83/1.33 *** allocated 75937 integers for clauses
% 0.83/1.33 Resimplifying inuse:
% 0.83/1.33 Done
% 0.83/1.33
% 0.83/1.33 *** allocated 22500 integers for termspace/termends
% 0.83/1.33 *** allocated 113905 integers for clauses
% 0.83/1.33
% 0.83/1.33 Intermediate Status:
% 0.83/1.33 Generated: 5006
% 0.83/1.33 Kept: 2005
% 0.83/1.33 Inuse: 297
% 0.83/1.33 Deleted: 42
% 0.83/1.33 Deletedinuse: 21
% 0.83/1.33
% 0.83/1.33 Resimplifying inuse:
% 0.83/1.33 Done
% 0.83/1.33
% 0.83/1.33 *** allocated 33750 integers for termspace/termends
% 0.83/1.33 *** allocated 170857 integers for clauses
% 0.83/1.33
% 0.83/1.33 Bliksems!, er is een bewijs:
% 0.83/1.33 % SZS status Theorem
% 0.83/1.33 % SZS output start Refutation
% 0.83/1.33
% 0.83/1.33 (5) {G0,W12,D3,L4,V2,M4} I { ! rel_str( X ), ! rel_str( Y ), ! subrelstr( Y
% 0.83/1.33 , X ), subset( the_carrier( Y ), the_carrier( X ) ) }.
% 0.83/1.33 (8) {G0,W15,D2,L5,V3,M5} I { ! one_sorted_str( X ), ! net_str( Y, X ), !
% 0.83/1.33 net_str( Z, X ), ! subnetstr( Z, X, Y ), subrelstr( Z, Y ) }.
% 0.83/1.33 (15) {G0,W7,D2,L3,V2,M3} I { ! one_sorted_str( X ), ! net_str( Y, X ),
% 0.83/1.33 rel_str( Y ) }.
% 0.83/1.33 (16) {G0,W7,D2,L3,V2,M3} I { ! rel_str( X ), ! subrelstr( Y, X ), rel_str(
% 0.83/1.33 Y ) }.
% 0.83/1.33 (17) {G0,W12,D2,L4,V3,M4} I { ! one_sorted_str( X ), ! net_str( Y, X ), !
% 0.83/1.33 subnetstr( Z, X, Y ), net_str( Z, X ) }.
% 0.83/1.33 (66) {G0,W2,D2,L1,V0,M1} I { one_sorted_str( skol19 ) }.
% 0.83/1.33 (67) {G0,W3,D2,L1,V0,M1} I { net_str( skol20, skol19 ) }.
% 0.83/1.33 (68) {G0,W4,D2,L1,V0,M1} I { subnetstr( skol21, skol19, skol20 ) }.
% 0.83/1.33 (69) {G0,W5,D3,L1,V0,M1} I { ! subset( the_carrier( skol21 ), the_carrier(
% 0.83/1.33 skol20 ) ) }.
% 0.83/1.33 (97) {G1,W9,D2,L3,V0,M3} R(8,68);r(66) { ! net_str( skol20, skol19 ), !
% 0.83/1.33 net_str( skol21, skol19 ), subrelstr( skol21, skol20 ) }.
% 0.83/1.33 (159) {G1,W2,D2,L1,V0,M1} R(15,67);r(66) { rel_str( skol20 ) }.
% 0.83/1.33 (179) {G2,W5,D2,L2,V1,M2} R(16,159) { ! subrelstr( X, skol20 ), rel_str( X
% 0.83/1.33 ) }.
% 0.83/1.33 (216) {G1,W6,D2,L2,V0,M2} R(17,68);r(66) { ! net_str( skol20, skol19 ),
% 0.83/1.33 net_str( skol21, skol19 ) }.
% 0.83/1.33 (777) {G2,W5,D2,L2,V0,M2} R(69,5);r(159) { ! rel_str( skol21 ), ! subrelstr
% 0.83/1.33 ( skol21, skol20 ) }.
% 0.83/1.33 (782) {G3,W3,D2,L1,V0,M1} S(777);r(179) { ! subrelstr( skol21, skol20 ) }.
% 0.83/1.33 (1645) {G4,W3,D2,L1,V0,M1} S(97);r(67);r(782) { ! net_str( skol21, skol19 )
% 0.83/1.33 }.
% 0.83/1.33 (2843) {G5,W0,D0,L0,V0,M0} S(216);r(67);r(1645) { }.
% 0.83/1.33
% 0.83/1.33
% 0.83/1.33 % SZS output end Refutation
% 0.83/1.33 found a proof!
% 0.83/1.33
% 0.83/1.33
% 0.83/1.33 Unprocessed initial clauses:
% 0.83/1.33
% 0.83/1.33 (2845) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 0.83/1.33 (2846) {G0,W4,D2,L2,V1,M2} { ! empty( X ), function( X ) }.
% 0.83/1.33 (2847) {G0,W4,D2,L2,V1,M2} { ! empty( X ), relation( X ) }.
% 0.83/1.33 (2848) {G0,W8,D4,L2,V3,M2} { ! element( X, powerset( cartesian_product2( Y
% 0.83/1.33 , Z ) ) ), relation( X ) }.
% 0.83/1.33 (2849) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 0.83/1.33 ), relation( X ) }.
% 0.83/1.33 (2850) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 0.83/1.33 ), function( X ) }.
% 0.83/1.33 (2851) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 0.83/1.33 ), one_to_one( X ) }.
% 0.83/1.33 (2852) {G0,W12,D3,L4,V2,M4} { ! rel_str( X ), ! rel_str( Y ), ! subrelstr
% 0.83/1.33 ( Y, X ), subset( the_carrier( Y ), the_carrier( X ) ) }.
% 0.83/1.33 (2853) {G0,W12,D3,L4,V2,M4} { ! rel_str( X ), ! rel_str( Y ), ! subrelstr
% 0.83/1.33 ( Y, X ), subset( the_InternalRel( Y ), the_InternalRel( X ) ) }.
% 0.83/1.33 (2854) {G0,W17,D3,L5,V2,M5} { ! rel_str( X ), ! rel_str( Y ), ! subset(
% 0.83/1.33 the_carrier( Y ), the_carrier( X ) ), ! subset( the_InternalRel( Y ),
% 0.83/1.33 the_InternalRel( X ) ), subrelstr( Y, X ) }.
% 0.83/1.33 (2855) {G0,W15,D2,L5,V3,M5} { ! one_sorted_str( X ), ! net_str( Y, X ), !
% 0.83/1.33 net_str( Z, X ), ! subnetstr( Z, X, Y ), subrelstr( Z, Y ) }.
% 0.83/1.33 (2856) {G0,W26,D4,L5,V3,M5} { ! one_sorted_str( X ), ! net_str( Y, X ), !
% 0.83/1.33 net_str( Z, X ), ! subnetstr( Z, X, Y ), the_mapping( X, Z ) =
% 0.83/1.33 relation_dom_restr_as_relation_of( the_carrier( Y ), the_carrier( X ),
% 0.83/1.33 the_mapping( X, Y ), the_carrier( Z ) ) }.
% 0.83/1.33 (2857) {G0,W29,D4,L6,V3,M6} { ! one_sorted_str( X ), ! net_str( Y, X ), !
% 0.83/1.33 net_str( Z, X ), ! subrelstr( Z, Y ), ! the_mapping( X, Z ) =
% 0.83/1.33 relation_dom_restr_as_relation_of( the_carrier( Y ), the_carrier( X ),
% 0.83/1.33 the_mapping( X, Y ), the_carrier( Z ) ), subnetstr( Z, X, Y ) }.
% 0.83/1.33 (2858) {G0,W1,D1,L1,V0,M1} { && }.
% 0.83/1.33 (2859) {G0,W1,D1,L1,V0,M1} { && }.
% 0.83/1.33 (2860) {G0,W1,D1,L1,V0,M1} { && }.
% 0.83/1.33 (2861) {G0,W6,D3,L2,V2,M2} { ! relation( X ), relation(
% 0.83/1.33 relation_dom_restriction( X, Y ) ) }.
% 0.83/1.33 (2862) {G0,W12,D3,L2,V4,M2} { ! relation_of2( Z, X, Y ),
% 0.83/1.33 relation_of2_as_subset( relation_dom_restr_as_relation_of( X, Y, Z, T ),
% 0.83/1.33 X, Y ) }.
% 0.83/1.33 (2863) {G0,W4,D2,L2,V1,M2} { ! rel_str( X ), one_sorted_str( X ) }.
% 0.83/1.33 (2864) {G0,W1,D1,L1,V0,M1} { && }.
% 0.83/1.33 (2865) {G0,W7,D2,L3,V2,M3} { ! one_sorted_str( X ), ! net_str( Y, X ),
% 0.83/1.33 rel_str( Y ) }.
% 0.83/1.33 (2866) {G0,W1,D1,L1,V0,M1} { && }.
% 0.83/1.33 (2867) {G0,W1,D1,L1,V0,M1} { && }.
% 0.83/1.33 (2868) {G0,W7,D2,L3,V2,M3} { ! rel_str( X ), ! subrelstr( Y, X ), rel_str
% 0.83/1.33 ( Y ) }.
% 0.83/1.33 (2869) {G0,W12,D2,L4,V3,M4} { ! one_sorted_str( X ), ! net_str( Y, X ), !
% 0.83/1.33 subnetstr( Z, X, Y ), net_str( Z, X ) }.
% 0.83/1.33 (2870) {G0,W10,D4,L2,V3,M2} { ! relation_of2_as_subset( Z, X, Y ), element
% 0.83/1.33 ( Z, powerset( cartesian_product2( X, Y ) ) ) }.
% 0.83/1.33 (2871) {G0,W9,D3,L2,V1,M2} { ! rel_str( X ), relation_of2_as_subset(
% 0.83/1.33 the_InternalRel( X ), the_carrier( X ), the_carrier( X ) ) }.
% 0.83/1.33 (2872) {G0,W1,D1,L1,V0,M1} { && }.
% 0.83/1.33 (2873) {G0,W9,D3,L3,V2,M3} { ! one_sorted_str( X ), ! net_str( Y, X ),
% 0.83/1.33 function( the_mapping( X, Y ) ) }.
% 0.83/1.33 (2874) {G0,W13,D3,L3,V2,M3} { ! one_sorted_str( X ), ! net_str( Y, X ),
% 0.83/1.33 quasi_total( the_mapping( X, Y ), the_carrier( Y ), the_carrier( X ) )
% 0.83/1.33 }.
% 0.83/1.33 (2875) {G0,W13,D3,L3,V2,M3} { ! one_sorted_str( X ), ! net_str( Y, X ),
% 0.83/1.33 relation_of2_as_subset( the_mapping( X, Y ), the_carrier( Y ),
% 0.83/1.33 the_carrier( X ) ) }.
% 0.83/1.33 (2876) {G0,W2,D2,L1,V0,M1} { rel_str( skol1 ) }.
% 0.83/1.33 (2877) {G0,W2,D2,L1,V0,M1} { one_sorted_str( skol2 ) }.
% 0.83/1.33 (2878) {G0,W6,D3,L2,V1,M2} { ! one_sorted_str( X ), net_str( skol3( X ), X
% 0.83/1.33 ) }.
% 0.83/1.33 (2879) {G0,W6,D3,L1,V2,M1} { relation_of2( skol4( X, Y ), X, Y ) }.
% 0.83/1.33 (2880) {G0,W4,D3,L1,V1,M1} { element( skol5( X ), X ) }.
% 0.83/1.33 (2881) {G0,W6,D3,L2,V1,M2} { ! rel_str( X ), subrelstr( skol6( X ), X )
% 0.83/1.33 }.
% 0.83/1.33 (2882) {G0,W11,D3,L3,V2,M3} { ! one_sorted_str( X ), ! net_str( Y, X ),
% 0.83/1.33 subnetstr( skol7( X, Y ), X, Y ) }.
% 0.83/1.33 (2883) {G0,W6,D3,L1,V2,M1} { relation_of2_as_subset( skol8( X, Y ), X, Y )
% 0.83/1.33 }.
% 0.83/1.33 (2884) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 0.83/1.33 (2885) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 0.83/1.33 (2886) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( empty_set ) }.
% 0.83/1.33 (2887) {G0,W8,D3,L3,V2,M3} { ! relation( X ), ! relation_empty_yielding( X
% 0.83/1.33 ), relation( relation_dom_restriction( X, Y ) ) }.
% 0.83/1.33 (2888) {G0,W8,D3,L3,V2,M3} { ! relation( X ), ! relation_empty_yielding( X
% 0.83/1.33 ), relation_empty_yielding( relation_dom_restriction( X, Y ) ) }.
% 0.83/1.33 (2889) {G0,W3,D3,L1,V1,M1} { ! empty( powerset( X ) ) }.
% 0.83/1.33 (2890) {G0,W8,D3,L3,V2,M3} { ! relation( X ), ! function( X ), relation(
% 0.83/1.33 relation_dom_restriction( X, Y ) ) }.
% 0.83/1.33 (2891) {G0,W8,D3,L3,V2,M3} { ! relation( X ), ! function( X ), function(
% 0.83/1.33 relation_dom_restriction( X, Y ) ) }.
% 0.83/1.33 (2892) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 0.83/1.33 (2893) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 0.83/1.33 (2894) {G0,W8,D3,L3,V2,M3} { empty( X ), empty( Y ), ! empty(
% 0.83/1.33 cartesian_product2( X, Y ) ) }.
% 0.83/1.33 (2895) {G0,W2,D2,L1,V0,M1} { relation( skol9 ) }.
% 0.83/1.33 (2896) {G0,W2,D2,L1,V0,M1} { function( skol9 ) }.
% 0.83/1.33 (2897) {G0,W2,D2,L1,V0,M1} { relation( skol10 ) }.
% 0.83/1.33 (2898) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol10 ) }.
% 0.83/1.33 (2899) {G0,W2,D2,L1,V0,M1} { function( skol10 ) }.
% 0.83/1.33 (2900) {G0,W2,D2,L1,V0,M1} { empty( skol11 ) }.
% 0.83/1.33 (2901) {G0,W2,D2,L1,V0,M1} { relation( skol11 ) }.
% 0.83/1.33 (2902) {G0,W5,D3,L2,V2,M2} { empty( X ), ! empty( skol12( Y ) ) }.
% 0.83/1.33 (2903) {G0,W7,D3,L2,V1,M2} { empty( X ), element( skol12( X ), powerset( X
% 0.83/1.33 ) ) }.
% 0.83/1.33 (2904) {G0,W2,D2,L1,V0,M1} { relation( skol13 ) }.
% 0.83/1.33 (2905) {G0,W2,D2,L1,V0,M1} { empty( skol13 ) }.
% 0.83/1.33 (2906) {G0,W2,D2,L1,V0,M1} { function( skol13 ) }.
% 0.83/1.33 (2907) {G0,W2,D2,L1,V0,M1} { ! empty( skol14 ) }.
% 0.83/1.33 (2908) {G0,W2,D2,L1,V0,M1} { relation( skol14 ) }.
% 0.83/1.33 (2909) {G0,W3,D3,L1,V1,M1} { empty( skol15( Y ) ) }.
% 0.83/1.33 (2910) {G0,W5,D3,L1,V1,M1} { element( skol15( X ), powerset( X ) ) }.
% 0.83/1.33 (2911) {G0,W2,D2,L1,V0,M1} { relation( skol16 ) }.
% 0.83/1.33 (2912) {G0,W2,D2,L1,V0,M1} { function( skol16 ) }.
% 0.83/1.33 (2913) {G0,W2,D2,L1,V0,M1} { one_to_one( skol16 ) }.
% 0.83/1.33 (2914) {G0,W2,D2,L1,V0,M1} { relation( skol17 ) }.
% 0.83/1.33 (2915) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol17 ) }.
% 0.83/1.33 (2916) {G0,W2,D2,L1,V0,M1} { relation( skol18 ) }.
% 0.83/1.33 (2917) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol18 ) }.
% 0.83/1.33 (2918) {G0,W2,D2,L1,V0,M1} { function( skol18 ) }.
% 0.83/1.33 (2919) {G0,W13,D3,L2,V4,M2} { ! relation_of2( Z, X, Y ),
% 0.83/1.33 relation_dom_restr_as_relation_of( X, Y, Z, T ) =
% 0.83/1.33 relation_dom_restriction( Z, T ) }.
% 0.83/1.33 (2920) {G0,W8,D2,L2,V3,M2} { ! relation_of2_as_subset( Z, X, Y ),
% 0.83/1.33 relation_of2( Z, X, Y ) }.
% 0.83/1.33 (2921) {G0,W8,D2,L2,V3,M2} { ! relation_of2( Z, X, Y ),
% 0.83/1.33 relation_of2_as_subset( Z, X, Y ) }.
% 0.83/1.33 (2922) {G0,W3,D2,L1,V1,M1} { subset( X, X ) }.
% 0.83/1.33 (2923) {G0,W2,D2,L1,V0,M1} { one_sorted_str( skol19 ) }.
% 0.83/1.33 (2924) {G0,W3,D2,L1,V0,M1} { net_str( skol20, skol19 ) }.
% 0.83/1.33 (2925) {G0,W4,D2,L1,V0,M1} { subnetstr( skol21, skol19, skol20 ) }.
% 0.83/1.33 (2926) {G0,W5,D3,L1,V0,M1} { ! subset( the_carrier( skol21 ), the_carrier
% 0.83/1.33 ( skol20 ) ) }.
% 0.83/1.33 (2927) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), element( X, Y ) }.
% 0.83/1.33 (2928) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 0.83/1.33 (2929) {G0,W7,D3,L2,V2,M2} { ! element( X, powerset( Y ) ), subset( X, Y )
% 0.83/1.33 }.
% 0.83/1.33 (2930) {G0,W7,D3,L2,V2,M2} { ! subset( X, Y ), element( X, powerset( Y ) )
% 0.83/1.33 }.
% 0.83/1.33 (2931) {G0,W10,D3,L3,V3,M3} { ! in( X, Z ), ! element( Z, powerset( Y ) )
% 0.83/1.33 , element( X, Y ) }.
% 0.83/1.33 (2932) {G0,W9,D3,L3,V3,M3} { ! in( X, Y ), ! element( Y, powerset( Z ) ),
% 0.83/1.33 ! empty( Z ) }.
% 0.83/1.33 (2933) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 0.83/1.33 (2934) {G0,W5,D2,L2,V2,M2} { ! in( X, Y ), ! empty( Y ) }.
% 0.83/1.33 (2935) {G0,W7,D2,L3,V2,M3} { ! empty( X ), X = Y, ! empty( Y ) }.
% 0.83/1.33
% 0.83/1.33
% 0.83/1.33 Total Proof:
% 0.83/1.33
% 0.83/1.33 subsumption: (5) {G0,W12,D3,L4,V2,M4} I { ! rel_str( X ), ! rel_str( Y ), !
% 0.83/1.33 subrelstr( Y, X ), subset( the_carrier( Y ), the_carrier( X ) ) }.
% 0.83/1.33 parent0: (2852) {G0,W12,D3,L4,V2,M4} { ! rel_str( X ), ! rel_str( Y ), !
% 0.83/1.33 subrelstr( Y, X ), subset( the_carrier( Y ), the_carrier( X ) ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := X
% 0.83/1.33 Y := Y
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 1 ==> 1
% 0.83/1.33 2 ==> 2
% 0.83/1.33 3 ==> 3
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (8) {G0,W15,D2,L5,V3,M5} I { ! one_sorted_str( X ), ! net_str
% 0.83/1.33 ( Y, X ), ! net_str( Z, X ), ! subnetstr( Z, X, Y ), subrelstr( Z, Y )
% 0.83/1.33 }.
% 0.83/1.33 parent0: (2855) {G0,W15,D2,L5,V3,M5} { ! one_sorted_str( X ), ! net_str( Y
% 0.83/1.33 , X ), ! net_str( Z, X ), ! subnetstr( Z, X, Y ), subrelstr( Z, Y ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := X
% 0.83/1.33 Y := Y
% 0.83/1.33 Z := Z
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 1 ==> 1
% 0.83/1.33 2 ==> 2
% 0.83/1.33 3 ==> 3
% 0.83/1.33 4 ==> 4
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (15) {G0,W7,D2,L3,V2,M3} I { ! one_sorted_str( X ), ! net_str
% 0.83/1.33 ( Y, X ), rel_str( Y ) }.
% 0.83/1.33 parent0: (2865) {G0,W7,D2,L3,V2,M3} { ! one_sorted_str( X ), ! net_str( Y
% 0.83/1.33 , X ), rel_str( Y ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := X
% 0.83/1.33 Y := Y
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 1 ==> 1
% 0.83/1.33 2 ==> 2
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (16) {G0,W7,D2,L3,V2,M3} I { ! rel_str( X ), ! subrelstr( Y, X
% 0.83/1.33 ), rel_str( Y ) }.
% 0.83/1.33 parent0: (2868) {G0,W7,D2,L3,V2,M3} { ! rel_str( X ), ! subrelstr( Y, X )
% 0.83/1.33 , rel_str( Y ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := X
% 0.83/1.33 Y := Y
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 1 ==> 1
% 0.83/1.33 2 ==> 2
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (17) {G0,W12,D2,L4,V3,M4} I { ! one_sorted_str( X ), ! net_str
% 0.83/1.33 ( Y, X ), ! subnetstr( Z, X, Y ), net_str( Z, X ) }.
% 0.83/1.33 parent0: (2869) {G0,W12,D2,L4,V3,M4} { ! one_sorted_str( X ), ! net_str( Y
% 0.83/1.33 , X ), ! subnetstr( Z, X, Y ), net_str( Z, X ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := X
% 0.83/1.33 Y := Y
% 0.83/1.33 Z := Z
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 1 ==> 1
% 0.83/1.33 2 ==> 2
% 0.83/1.33 3 ==> 3
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (66) {G0,W2,D2,L1,V0,M1} I { one_sorted_str( skol19 ) }.
% 0.83/1.33 parent0: (2923) {G0,W2,D2,L1,V0,M1} { one_sorted_str( skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (67) {G0,W3,D2,L1,V0,M1} I { net_str( skol20, skol19 ) }.
% 0.83/1.33 parent0: (2924) {G0,W3,D2,L1,V0,M1} { net_str( skol20, skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (68) {G0,W4,D2,L1,V0,M1} I { subnetstr( skol21, skol19, skol20
% 0.83/1.33 ) }.
% 0.83/1.33 parent0: (2925) {G0,W4,D2,L1,V0,M1} { subnetstr( skol21, skol19, skol20 )
% 0.83/1.33 }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (69) {G0,W5,D3,L1,V0,M1} I { ! subset( the_carrier( skol21 ),
% 0.83/1.33 the_carrier( skol20 ) ) }.
% 0.83/1.33 parent0: (2926) {G0,W5,D3,L1,V0,M1} { ! subset( the_carrier( skol21 ),
% 0.83/1.33 the_carrier( skol20 ) ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3028) {G1,W11,D2,L4,V0,M4} { ! one_sorted_str( skol19 ), !
% 0.83/1.33 net_str( skol20, skol19 ), ! net_str( skol21, skol19 ), subrelstr( skol21
% 0.83/1.33 , skol20 ) }.
% 0.83/1.33 parent0[3]: (8) {G0,W15,D2,L5,V3,M5} I { ! one_sorted_str( X ), ! net_str(
% 0.83/1.33 Y, X ), ! net_str( Z, X ), ! subnetstr( Z, X, Y ), subrelstr( Z, Y ) }.
% 0.83/1.33 parent1[0]: (68) {G0,W4,D2,L1,V0,M1} I { subnetstr( skol21, skol19, skol20
% 0.83/1.33 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := skol19
% 0.83/1.33 Y := skol20
% 0.83/1.33 Z := skol21
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3029) {G1,W9,D2,L3,V0,M3} { ! net_str( skol20, skol19 ), !
% 0.83/1.33 net_str( skol21, skol19 ), subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent0[0]: (3028) {G1,W11,D2,L4,V0,M4} { ! one_sorted_str( skol19 ), !
% 0.83/1.33 net_str( skol20, skol19 ), ! net_str( skol21, skol19 ), subrelstr( skol21
% 0.83/1.33 , skol20 ) }.
% 0.83/1.33 parent1[0]: (66) {G0,W2,D2,L1,V0,M1} I { one_sorted_str( skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (97) {G1,W9,D2,L3,V0,M3} R(8,68);r(66) { ! net_str( skol20,
% 0.83/1.33 skol19 ), ! net_str( skol21, skol19 ), subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent0: (3029) {G1,W9,D2,L3,V0,M3} { ! net_str( skol20, skol19 ), !
% 0.83/1.33 net_str( skol21, skol19 ), subrelstr( skol21, skol20 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 1 ==> 1
% 0.83/1.33 2 ==> 2
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3030) {G1,W4,D2,L2,V0,M2} { ! one_sorted_str( skol19 ),
% 0.83/1.33 rel_str( skol20 ) }.
% 0.83/1.33 parent0[1]: (15) {G0,W7,D2,L3,V2,M3} I { ! one_sorted_str( X ), ! net_str(
% 0.83/1.33 Y, X ), rel_str( Y ) }.
% 0.83/1.33 parent1[0]: (67) {G0,W3,D2,L1,V0,M1} I { net_str( skol20, skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := skol19
% 0.83/1.33 Y := skol20
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3031) {G1,W2,D2,L1,V0,M1} { rel_str( skol20 ) }.
% 0.83/1.33 parent0[0]: (3030) {G1,W4,D2,L2,V0,M2} { ! one_sorted_str( skol19 ),
% 0.83/1.33 rel_str( skol20 ) }.
% 0.83/1.33 parent1[0]: (66) {G0,W2,D2,L1,V0,M1} I { one_sorted_str( skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (159) {G1,W2,D2,L1,V0,M1} R(15,67);r(66) { rel_str( skol20 )
% 0.83/1.33 }.
% 0.83/1.33 parent0: (3031) {G1,W2,D2,L1,V0,M1} { rel_str( skol20 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3032) {G1,W5,D2,L2,V1,M2} { ! subrelstr( X, skol20 ), rel_str
% 0.83/1.33 ( X ) }.
% 0.83/1.33 parent0[0]: (16) {G0,W7,D2,L3,V2,M3} I { ! rel_str( X ), ! subrelstr( Y, X
% 0.83/1.33 ), rel_str( Y ) }.
% 0.83/1.33 parent1[0]: (159) {G1,W2,D2,L1,V0,M1} R(15,67);r(66) { rel_str( skol20 )
% 0.83/1.33 }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := skol20
% 0.83/1.33 Y := X
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (179) {G2,W5,D2,L2,V1,M2} R(16,159) { ! subrelstr( X, skol20 )
% 0.83/1.33 , rel_str( X ) }.
% 0.83/1.33 parent0: (3032) {G1,W5,D2,L2,V1,M2} { ! subrelstr( X, skol20 ), rel_str( X
% 0.83/1.33 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := X
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 1 ==> 1
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3033) {G1,W8,D2,L3,V0,M3} { ! one_sorted_str( skol19 ), !
% 0.83/1.33 net_str( skol20, skol19 ), net_str( skol21, skol19 ) }.
% 0.83/1.33 parent0[2]: (17) {G0,W12,D2,L4,V3,M4} I { ! one_sorted_str( X ), ! net_str
% 0.83/1.33 ( Y, X ), ! subnetstr( Z, X, Y ), net_str( Z, X ) }.
% 0.83/1.33 parent1[0]: (68) {G0,W4,D2,L1,V0,M1} I { subnetstr( skol21, skol19, skol20
% 0.83/1.33 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 X := skol19
% 0.83/1.33 Y := skol20
% 0.83/1.33 Z := skol21
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3034) {G1,W6,D2,L2,V0,M2} { ! net_str( skol20, skol19 ),
% 0.83/1.33 net_str( skol21, skol19 ) }.
% 0.83/1.33 parent0[0]: (3033) {G1,W8,D2,L3,V0,M3} { ! one_sorted_str( skol19 ), !
% 0.83/1.33 net_str( skol20, skol19 ), net_str( skol21, skol19 ) }.
% 0.83/1.33 parent1[0]: (66) {G0,W2,D2,L1,V0,M1} I { one_sorted_str( skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (216) {G1,W6,D2,L2,V0,M2} R(17,68);r(66) { ! net_str( skol20,
% 0.83/1.33 skol19 ), net_str( skol21, skol19 ) }.
% 0.83/1.33 parent0: (3034) {G1,W6,D2,L2,V0,M2} { ! net_str( skol20, skol19 ), net_str
% 0.83/1.33 ( skol21, skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 1 ==> 1
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3035) {G1,W7,D2,L3,V0,M3} { ! rel_str( skol20 ), ! rel_str(
% 0.83/1.33 skol21 ), ! subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent0[0]: (69) {G0,W5,D3,L1,V0,M1} I { ! subset( the_carrier( skol21 ),
% 0.83/1.33 the_carrier( skol20 ) ) }.
% 0.83/1.33 parent1[3]: (5) {G0,W12,D3,L4,V2,M4} I { ! rel_str( X ), ! rel_str( Y ), !
% 0.83/1.33 subrelstr( Y, X ), subset( the_carrier( Y ), the_carrier( X ) ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 X := skol20
% 0.83/1.33 Y := skol21
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3036) {G2,W5,D2,L2,V0,M2} { ! rel_str( skol21 ), ! subrelstr
% 0.83/1.33 ( skol21, skol20 ) }.
% 0.83/1.33 parent0[0]: (3035) {G1,W7,D2,L3,V0,M3} { ! rel_str( skol20 ), ! rel_str(
% 0.83/1.33 skol21 ), ! subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent1[0]: (159) {G1,W2,D2,L1,V0,M1} R(15,67);r(66) { rel_str( skol20 )
% 0.83/1.33 }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (777) {G2,W5,D2,L2,V0,M2} R(69,5);r(159) { ! rel_str( skol21 )
% 0.83/1.33 , ! subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent0: (3036) {G2,W5,D2,L2,V0,M2} { ! rel_str( skol21 ), ! subrelstr(
% 0.83/1.33 skol21, skol20 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 1 ==> 1
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3037) {G3,W6,D2,L2,V0,M2} { ! subrelstr( skol21, skol20 ), !
% 0.83/1.33 subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent0[0]: (777) {G2,W5,D2,L2,V0,M2} R(69,5);r(159) { ! rel_str( skol21 )
% 0.83/1.33 , ! subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent1[1]: (179) {G2,W5,D2,L2,V1,M2} R(16,159) { ! subrelstr( X, skol20 )
% 0.83/1.33 , rel_str( X ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 X := skol21
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 factor: (3038) {G3,W3,D2,L1,V0,M1} { ! subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent0[0, 1]: (3037) {G3,W6,D2,L2,V0,M2} { ! subrelstr( skol21, skol20 )
% 0.83/1.33 , ! subrelstr( skol21, skol20 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (782) {G3,W3,D2,L1,V0,M1} S(777);r(179) { ! subrelstr( skol21
% 0.83/1.33 , skol20 ) }.
% 0.83/1.33 parent0: (3038) {G3,W3,D2,L1,V0,M1} { ! subrelstr( skol21, skol20 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3039) {G1,W6,D2,L2,V0,M2} { ! net_str( skol21, skol19 ),
% 0.83/1.33 subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent0[0]: (97) {G1,W9,D2,L3,V0,M3} R(8,68);r(66) { ! net_str( skol20,
% 0.83/1.33 skol19 ), ! net_str( skol21, skol19 ), subrelstr( skol21, skol20 ) }.
% 0.83/1.33 parent1[0]: (67) {G0,W3,D2,L1,V0,M1} I { net_str( skol20, skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3040) {G2,W3,D2,L1,V0,M1} { ! net_str( skol21, skol19 ) }.
% 0.83/1.33 parent0[0]: (782) {G3,W3,D2,L1,V0,M1} S(777);r(179) { ! subrelstr( skol21,
% 0.83/1.33 skol20 ) }.
% 0.83/1.33 parent1[1]: (3039) {G1,W6,D2,L2,V0,M2} { ! net_str( skol21, skol19 ),
% 0.83/1.33 subrelstr( skol21, skol20 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (1645) {G4,W3,D2,L1,V0,M1} S(97);r(67);r(782) { ! net_str(
% 0.83/1.33 skol21, skol19 ) }.
% 0.83/1.33 parent0: (3040) {G2,W3,D2,L1,V0,M1} { ! net_str( skol21, skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 0 ==> 0
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3041) {G1,W3,D2,L1,V0,M1} { net_str( skol21, skol19 ) }.
% 0.83/1.33 parent0[0]: (216) {G1,W6,D2,L2,V0,M2} R(17,68);r(66) { ! net_str( skol20,
% 0.83/1.33 skol19 ), net_str( skol21, skol19 ) }.
% 0.83/1.33 parent1[0]: (67) {G0,W3,D2,L1,V0,M1} I { net_str( skol20, skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 resolution: (3042) {G2,W0,D0,L0,V0,M0} { }.
% 0.83/1.33 parent0[0]: (1645) {G4,W3,D2,L1,V0,M1} S(97);r(67);r(782) { ! net_str(
% 0.83/1.33 skol21, skol19 ) }.
% 0.83/1.33 parent1[0]: (3041) {G1,W3,D2,L1,V0,M1} { net_str( skol21, skol19 ) }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 substitution1:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 subsumption: (2843) {G5,W0,D0,L0,V0,M0} S(216);r(67);r(1645) { }.
% 0.83/1.33 parent0: (3042) {G2,W0,D0,L0,V0,M0} { }.
% 0.83/1.33 substitution0:
% 0.83/1.33 end
% 0.83/1.33 permutation0:
% 0.83/1.33 end
% 0.83/1.33
% 0.83/1.33 Proof check complete!
% 0.83/1.33
% 0.83/1.33 Memory use:
% 0.83/1.33
% 0.83/1.33 space for terms: 30592
% 0.83/1.33 space for clauses: 141734
% 0.83/1.33
% 0.83/1.33
% 0.83/1.33 clauses generated: 8934
% 0.83/1.33 clauses kept: 2844
% 0.83/1.33 clauses selected: 399
% 0.83/1.33 clauses deleted: 44
% 0.83/1.33 clauses inuse deleted: 21
% 0.83/1.33
% 0.83/1.33 subsentry: 6446
% 0.83/1.33 literals s-matched: 4538
% 0.83/1.33 literals matched: 4309
% 0.83/1.33 full subsumption: 711
% 0.83/1.33
% 0.83/1.33 checksum: 151597766
% 0.83/1.33
% 0.83/1.33
% 0.83/1.33 Bliksem ended
%------------------------------------------------------------------------------