Bob is quiet. Bob is red. Bob is rough. Bob is white. Harry is red. Harry is round. Harry is white. All red, round things are furry. All round things are red. If something is green and round then it is red. Red, rough things are quiet. All red, furry things are round. All green, rough things are white. Furry, white things are quiet. If something is quiet and green then it is rough.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
All red, round things are furry.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is green and round then it is red.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Red, rough things are quiet.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All red, furry things are round.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
All green, rough things are white.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Furry, white things are quiet.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and green then it is rough.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Bob is not white.
False
1
inv-proof
[(triple4)]
("Bob" "is" "white" "-")
triple4
Harry is furry.
True
3
proof
[(((triple5 triple6) -> rule1) OR ((((triple6) -> rule2) triple6) -> rule1))]
("Harry" "is" "furry" "+")
((triple5 triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple6) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((triple5 triple6) -> rule1) OR ((((triple6) -> rule2) triple6) -> rule1))]
("Harry" "is" "furry" "-")
((triple5 triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple6) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
True
5
proof
[(((((triple5 triple6) -> rule1) triple7) -> rule7) OR ((((((triple6) -> rule2) triple6) -> rule1) triple7) -> rule7))]
("Harry" "is" "quiet" "+")
((((triple5 triple6) -> (rule1 % int2)) triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple6) -> (rule2 % int3)) triple6) -> (rule1 % int2)) triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not quiet.
False
5
inv-proof
[(((((triple5 triple6) -> rule1) triple7) -> rule7) OR ((((((triple6) -> rule2) triple6) -> rule1) triple7) -> rule7))]
("Harry" "is" "quiet" "-")
((((triple5 triple6) -> (rule1 % int2)) triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple6) -> (rule2 % int3)) triple6) -> (rule1 % int2)) triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is furry.
Unknown
rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Bob" "is" "furry" "+")
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Bob is quiet.[(triple1 OR ((triple2 triple3) -> rule4))] Bob is red.[(triple2)] Bob is rough.[(triple3)] Bob is white.[(triple4)] Harry is red.[(triple5 OR ((triple6) -> rule2))] Harry is round.[(triple6)] Harry is white.[(triple7)] @1: Harry is furry.[(((triple5 triple6) -> rule1) OR ((((triple6) -> rule2) triple6) -> rule1))] @2: Harry is quiet.[(((((triple5 triple6) -> rule1) triple7) -> rule7) OR ((((((triple6) -> rule2) triple6) -> rule1) triple7) -> rule7))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
((triple2 triple3) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
((triple6) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
((triple5 triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple6) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple5 triple6) -> (rule1 % int2)) triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple6) -> (rule2 % int3)) triple6) -> (rule1 % int2)) triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3