Bob is big. Bob is blue. Harry is big. Harry is blue. Harry is kind. Harry is nice. Harry is quiet. Blue people are nice. All blue, nice people are furry. If someone is big and blue then they are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
All blue, nice people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is big and blue then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Harry is blue.
True
1
proof
[(triple4)]
("Harry" "is" "blue" "+")
triple4
Harry is not nice.
False
1
inv-proof
[(triple6 OR ((triple4) -> rule1))]
("Harry" "is" "nice" "-")
triple6
((triple4) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
True
3
proof
[(((triple4 triple6) -> rule2) OR ((triple4 ((triple4) -> rule1)) -> rule2))]
("Harry" "is" "furry" "+")
((triple4 triple6) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is not nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "nice" "-")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Harry is big.[(triple3)] Harry is blue.[(triple4)] Harry is kind.[(triple5)] Harry is nice.[(triple6 OR ((triple4) -> rule1))] Harry is quiet.[(triple7)] @1: Bob is cold.[(((triple1 triple2) -> rule3))] Bob is nice.[(((triple2) -> rule1))] Harry is cold.[(((triple3 triple4) -> rule3))] Harry is furry.[(((triple4 triple6) -> rule2) OR ((triple4 ((triple4) -> rule1)) -> rule2))] @2: Bob is furry.[(((triple2 ((triple2) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
((triple4) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple1 triple2) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple3 triple4) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple4 triple6) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2