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