Anne is nice. Charlie is big. Charlie is kind. Charlie is red. Charlie is round. Charlie is smart. Dave is big. Dave is quiet. Dave is not red. Dave is round. Dave is smart. Harry is big. Harry is kind. Harry is nice. Harry is quiet. If someone is round then they are kind.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Dave is big.
True
1
proof
[(triple7)]
("Dave" "is" "big" "+")
triple7
Dave is not smart.
False
1
inv-proof
[(triple11)]
("Dave" "is" "smart" "-")
triple11
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Anne is nice.[(triple1)] Charlie is big.[(triple2)] Charlie is kind.[(triple3 OR ((triple5) -> rule1))] Charlie is red.[(triple4)] Charlie is round.[(triple5)] Charlie is smart.[(triple6)] Dave is big.[(triple7)] Dave is not red.[(triple9)] Dave is quiet.[(triple8)] Dave is round.[(triple10)] Dave is smart.[(triple11)] Harry is big.[(triple12)] Harry is kind.[(triple13)] Harry is nice.[(triple14)] Harry is quiet.[(triple15)] @1: Dave is kind.[(((triple10) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple5) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is not red.
("Dave" "is" "red" "-")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Dave is kind.
("Dave" "is" "kind" "+")
((triple10) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1