Anne is quiet. Anne is red. Anne is white. Bob is not green. Bob is nice. Harry is furry. Harry is green. Harry is nice. Harry is quiet. Harry is not red. Harry is smart. Harry is white. Green people are white. All quiet people are nice. If Harry is smart then Harry is quiet. If someone is red then they are smart. Red, green people are not furry. If someone is furry then they are quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If Harry is smart then Harry is quiet.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "quiet" "+"))
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Red, green people are not furry.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "-"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Bob is nice.
True
1
proof
[(triple5)]
("Bob" "is" "nice" "+")
triple5
Harry is not smart.
False
1
inv-proof
[(triple11)]
("Harry" "is" "smart" "-")
triple11
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Anne is quiet.[(triple1)] Anne is red.[(triple2)] Anne is white.[(triple3)] Bob is nice.[(triple5)] Bob is not green.[(triple4)] Harry is furry.[(triple6)] Harry is green.[(triple7)] Harry is nice.[(triple8 OR ((triple9) -> rule2) OR ((((triple11) -> rule3)) -> rule2) OR ((((triple6) -> rule6)) -> rule2))] Harry is not red.[(triple10)] Harry is quiet.[(triple9 OR ((triple11) -> rule3) OR ((triple6) -> rule6))] Harry is smart.[(triple11)] Harry is white.[(triple12 OR ((triple7) -> rule1))] @1: Anne is nice.[(((triple1) -> rule2))] Anne is smart.[(((triple2) -> rule4))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is not green.
("Bob" "is" "green" "-")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple9) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not red.
("Harry" "is" "red" "-")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
((triple11) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple6) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple7) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1