Bob is blue. Bob is cold. Bob is furry. Bob is quiet. Bob is round. Bob is smart. Bob is young. Dave is blue. Dave is round. Dave is smart. All round things are blue. Quiet, young things are smart. All blue things are round. Young things are quiet. Round, young things are blue. All cold, smart things are furry.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
All round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Quiet, young things are smart.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Round, young things are blue.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All cold, smart things are furry.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Bob is quiet.
True
1
proof
[(triple4 OR ((triple7) -> rule4))]
("Bob" "is" "quiet" "+")
triple4
((triple7) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not blue.
False
1
inv-proof
[(triple1 OR ((triple5) -> rule1) OR ((triple5 triple7) -> rule5))]
("Bob" "is" "blue" "-")
triple1
((triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple5 triple7) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Bob is blue.[(triple1 OR ((triple5) -> rule1) OR ((triple5 triple7) -> rule5))] Bob is cold.[(triple2)] Bob is furry.[(triple3 OR ((triple2 triple6) -> rule6) OR ((triple2 ((triple4 triple7) -> rule2)) -> rule6) OR ((triple2 ((((triple7) -> rule4) triple7) -> rule2)) -> rule6))] Bob is quiet.[(triple4 OR ((triple7) -> rule4))] Bob is round.[(triple5 OR ((triple1) -> rule3))] Bob is smart.[(triple6 OR ((triple4 triple7) -> rule2) OR ((((triple7) -> rule4) triple7) -> rule2))] Bob is young.[(triple7)] Dave is blue.[(triple8 OR ((triple9) -> rule1))] Dave is round.[(triple9 OR ((triple8) -> rule3))] Dave is smart.[(triple10)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple5 triple7) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple2 triple6) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple2 ((triple4 triple7) -> (rule2 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((triple2 ((((triple7) -> (rule4 % int3)) triple7) -> (rule2 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple7) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple4 triple7) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple7) -> (rule4 % int2)) triple7) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
((triple9) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple9
((triple8) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple10