Bob is cold. Bob is furry. Bob is red. Bob is round. Dave is kind. Dave is red. Dave is round. Dave is white. Gary is furry. Gary is kind. Gary is round. Harry is blue. Harry is kind. Harry is red. Harry is round. Harry is white. Cold things are round. Red, kind things are white. Cold things are blue. If something is red and round then it is furry. Furry things are kind. If Bob is blue and Bob is red then Bob is kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Red, kind things are white.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is red and round then it is furry.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If Bob is blue and Bob is red then Bob is kind.
((("Bob" "is" "blue" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "kind" "+"))
Dave is round.
True
1
proof
[(triple7)]
("Dave" "is" "round" "+")
triple7
Gary is not furry.
False
1
inv-proof
[(triple9)]
("Gary" "is" "furry" "-")
triple9
Harry is furry.
True
3
proof
[(((triple14 triple15) -> rule4))]
("Harry" "is" "furry" "+")
((triple14 triple15) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple3 triple4) -> rule4)) -> rule5) OR ((((triple1) -> rule3) triple3) -> rule6) OR ((((triple3 ((triple1) -> rule1)) -> rule4)) -> rule5))]
("Bob" "is" "kind" "-")
((triple2) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple1) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple3 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is white.
True
4
proof
[(((triple3 ((triple2) -> rule5)) -> rule2) OR ((triple3 ((((triple3 triple4) -> rule4)) -> rule5)) -> rule2) OR ((triple3 ((((triple1) -> rule3) triple3) -> rule6)) -> rule2) OR ((triple3 ((((triple3 ((triple1) -> rule1)) -> rule4)) -> rule5)) -> rule2))]
("Bob" "is" "white" "+")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple3 ((((triple3 triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple3 ((((triple1) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((triple3 ((((triple3 ((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is not white.
False
4
inv-proof
[(((triple3 ((triple2) -> rule5)) -> rule2) OR ((triple3 ((((triple3 triple4) -> rule4)) -> rule5)) -> rule2) OR ((triple3 ((((triple1) -> rule3) triple3) -> rule6)) -> rule2) OR ((triple3 ((((triple3 ((triple1) -> rule1)) -> rule4)) -> rule5)) -> rule2))]
("Bob" "is" "white" "-")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple3 ((((triple3 triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple3 ((((triple1) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((triple3 ((((triple3 ((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "blue" "+")
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2 OR ((triple3 triple4) -> rule4) OR ((triple3 ((triple1) -> rule1)) -> rule4))] Bob is red.[(triple3)] Bob is round.[(triple4 OR ((triple1) -> rule1))] Dave is kind.[(triple5 OR ((((triple6 triple7) -> rule4)) -> rule5))] Dave is red.[(triple6)] Dave is round.[(triple7)] Dave is white.[(triple8 OR ((triple6 triple5) -> rule2) OR ((triple6 ((((triple6 triple7) -> rule4)) -> rule5)) -> rule2))] Gary is furry.[(triple9)] Gary is kind.[(triple10 OR ((triple9) -> rule5))] Gary is round.[(triple11)] Harry is blue.[(triple12)] Harry is kind.[(triple13 OR ((((triple14 triple15) -> rule4)) -> rule5))] Harry is red.[(triple14)] Harry is round.[(triple15)] Harry is white.[(triple16 OR ((triple14 triple13) -> rule2) OR ((triple14 ((((triple14 triple15) -> rule4)) -> rule5)) -> rule2))] @1: Bob is blue.[(((triple1) -> rule3))] Bob is kind.[(((triple2) -> rule5) OR ((((triple3 triple4) -> rule4)) -> rule5) OR ((((triple1) -> rule3) triple3) -> rule6) OR ((((triple3 ((triple1) -> rule1)) -> rule4)) -> rule5))] Dave is furry.[(((triple6 triple7) -> rule4))] Harry is furry.[(((triple14 triple15) -> rule4))] @2: Bob is white.[(((triple3 ((triple2) -> rule5)) -> rule2) OR ((triple3 ((((triple3 triple4) -> rule4)) -> rule5)) -> rule2) OR ((triple3 ((((triple1) -> rule3) triple3) -> rule6)) -> rule2) OR ((triple3 ((((triple3 ((triple1) -> rule1)) -> rule4)) -> rule5)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple3 triple4) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple3 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple5
((((triple6 triple7) -> (rule4 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
((triple6 triple5) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple6 ((((triple6 triple7) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
((triple9) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
((((triple14 triple15) -> (rule4 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple14 triple13) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple14 ((((triple14 triple15) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple1) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple3 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple6 triple7) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple14 triple15) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple3 ((((triple3 triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple3 ((((triple1) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((triple3 ((((triple3 ((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4