Bob is blue. Bob is cold. Bob is furry. Bob is green. Bob is quiet. Bob is round. Bob is smart. Dave is cold. Dave is furry. Dave is green. Dave is quiet. Harry is round. All blue, green people are furry. All quiet people are smart. If Harry is quiet then Harry is smart. If someone is smart and furry then they are cold. Cold people are furry. All quiet people are cold. Smart people are furry. All cold people are furry.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
All blue, green people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If Harry is quiet then Harry is smart.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "smart" "+"))
If someone is smart and furry then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
All quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Harry is round.
True
1
proof
[(triple12)]
("Harry" "is" "round" "+")
triple12
Bob is not quiet.
False
1
inv-proof
[(triple5)]
("Bob" "is" "quiet" "-")
triple5
Harry is not furry.
Unknown
inv-rconc
[@3: Harry is furry.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule2 <- FAIL)]]
("Harry" "is" "furry" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple5) -> rule6) OR ((triple7 triple3) -> rule4) OR ((triple7 ((triple7) -> rule7)) -> rule4) OR ((triple7 ((triple1 triple4) -> rule1)) -> rule4) OR ((((triple5) -> rule2) triple3) -> rule4) OR ((((triple5) -> rule2) ((triple7) -> rule7)) -> rule4) OR ((((triple5) -> rule2) ((triple1 triple4) -> rule1)) -> rule4) OR ((triple7 ((((triple5) -> rule2)) -> rule7)) -> rule4) OR ((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule7)) -> rule4))] Bob is furry.[(triple3 OR ((triple2) -> rule5) OR ((triple2) -> rule8) OR ((triple7) -> rule7) OR ((triple1 triple4) -> rule1) OR ((((triple5) -> rule2)) -> rule7) OR ((((triple5) -> rule6)) -> rule5) OR ((((triple5) -> rule6)) -> rule8))] Bob is green.[(triple4)] Bob is quiet.[(triple5)] Bob is round.[(triple6)] Bob is smart.[(triple7 OR ((triple5) -> rule2))] Dave is cold.[(triple8 OR ((triple11) -> rule6) OR ((((triple11) -> rule2) triple9) -> rule4) OR ((((triple11) -> rule2) ((((triple11) -> rule2)) -> rule7)) -> rule4))] Dave is furry.[(triple9 OR ((triple8) -> rule5) OR ((triple8) -> rule8) OR ((((triple11) -> rule2)) -> rule7) OR ((((triple11) -> rule6)) -> rule5) OR ((((triple11) -> rule6)) -> rule8))] Dave is green.[(triple10)] Dave is quiet.[(triple11)] Harry is round.[(triple12)] @1: Dave is smart.[(((triple11) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple5) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple7 triple3) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple7 ((triple7) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((triple7 ((triple1 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple5) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5) -> (rule2 % int3)) ((triple7) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((triple5) -> (rule2 % int3)) ((triple1 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((triple7 ((((triple5) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((triple5) -> (rule2 % int3)) ((((triple5) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple2) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple2) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple7) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple1 triple4) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
((triple5) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple8
((triple11) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple11) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple11) -> (rule2 % int3)) ((((triple11) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
triple9
((triple8) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple8) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple11) -> (rule6 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple11) -> (rule6 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Dave is smart.
("Dave" "is" "smart" "+")
((triple11) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1