Anne is big. Anne is green. Charlie is green. Charlie is kind. Harry is big. Harry is nice. Harry is red. If something is big and green then it is smart. All smart things are big. If something is nice and furry then it is green. Big things are green. Nice things are kind. If something is furry and red then it is green.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is big and green then it is smart.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
All smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is nice and furry then it is green.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is furry and red then it is green.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Anne is green.
True
1
proof
[(triple2 OR ((triple1) -> rule4))]
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is not kind.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "kind" "-")
triple4
Harry is green.
True
2
proof
[(((triple5) -> rule4))]
("Harry" "is" "green" "+")
((triple5) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Anne is not smart.
False
3
inv-proof
[(((triple1 triple2) -> rule1) OR ((triple1 ((triple1) -> rule4)) -> rule1))]
("Anne" "is" "smart" "-")
((triple1 triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is smart.
Unknown
rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((triple1) -> rule4))] Charlie is green.[(triple3)] Charlie is kind.[(triple4)] Harry is big.[(triple5)] Harry is nice.[(triple6)] Harry is red.[(triple7)] @1: Anne is smart.[(((triple1 triple2) -> rule1) OR ((triple1 ((triple1) -> rule4)) -> rule1))] Harry is green.[(((triple5) -> rule4))] Harry is kind.[(((triple6) -> rule5))] @2: Harry is smart.[(((triple5 ((triple5) -> rule4)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple5) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple6) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2