Anne is furry. Anne is green. Anne is smart. Charlie is furry. Charlie is young. Harry is big. Harry is furry. Harry is green. Harry is nice. Harry is round. Harry is smart. Harry is young. If Harry is young and Harry is green then Harry is nice. Furry, green people are big.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is young and Harry is green then Harry is nice.
((("Harry" "is" "young" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "nice" "+"))
Furry, green people are big.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Anne is green.
True
1
proof
[(triple2)]
("Anne" "is" "green" "+")
triple2
Anne is not green.
False
1
inv-proof
[(triple2)]
("Anne" "is" "green" "-")
triple2
Anne is big.
True
3
proof
[(((triple1 triple2) -> rule2))]
("Anne" "is" "big" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
3
inv-proof
[(((triple1 triple2) -> rule2))]
("Anne" "is" "big" "-")
((triple1 triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is smart.[(triple3)] Charlie is furry.[(triple4)] Charlie is young.[(triple5)] Harry is big.[(triple6 OR ((triple7 triple8) -> rule2))] Harry is furry.[(triple7)] Harry is green.[(triple8)] Harry is nice.[(triple9 OR ((triple12 triple8) -> rule1))] Harry is round.[(triple10)] Harry is smart.[(triple11)] Harry is young.[(triple12)] @1: Anne is big.[(((triple1 triple2) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
((triple7 triple8) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
((triple12 triple8) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1