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