Bob is big. Bob is cold. Bob is furry. Bob is green. Charlie is big. Charlie is green. Charlie is smart. If Bob is furry then Bob is green. Green, kind people are smart. If someone is big and furry then they are smart. If someone is furry and big then they are smart. All nice, green people are kind. Green, furry people are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If Bob is furry then Bob is green.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "green" "+"))
Green, kind people are smart.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and furry then they are smart.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is furry and big then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All nice, green people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Green, furry people are kind.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Bob is green.
True
1
proof
[(triple4 OR ((triple3) -> rule1))]
("Bob" "is" "green" "+")
triple4
((triple3) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is not green.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "green" "-")
triple6
Bob is kind.
True
3
proof
[(((triple4 triple3) -> rule6) OR ((((triple3) -> rule1) triple3) -> rule6))]
("Bob" "is" "kind" "+")
((triple4 triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((triple1 triple3) -> rule3) OR ((triple3 triple1) -> rule4) OR ((triple4 ((triple4 triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule1) ((triple4 triple3) -> rule6)) -> rule2) OR ((triple4 ((((triple3) -> rule1) triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule1) ((((triple3) -> rule1) triple3) -> rule6)) -> rule2))]
("Bob" "is" "smart" "-")
((triple1 triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3 triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple4 ((triple4 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple4 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((triple4 ((((triple3) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is green.[(triple4 OR ((triple3) -> rule1))] Charlie is big.[(triple5)] Charlie is green.[(triple6)] Charlie is smart.[(triple7)] @1: Bob is kind.[(((triple4 triple3) -> rule6) OR ((((triple3) -> rule1) triple3) -> rule6))] Bob is smart.[(((triple1 triple3) -> rule3) OR ((triple3 triple1) -> rule4) OR ((triple4 ((triple4 triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule1) ((triple4 triple3) -> rule6)) -> rule2) OR ((triple4 ((((triple3) -> rule1) triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule1) ((((triple3) -> rule1) triple3) -> rule6)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
((triple3) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple4 triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple1 triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3 triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple4 ((triple4 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple4 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((triple4 ((((triple3) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3