Anne is furry. Charlie is big. Charlie is cold. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is rough. Harry is cold. Harry is furry. Harry is green. Harry is nice. Harry is rough. All green, nice things are quiet. If something is quiet and big then it is furry.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All green, nice things are quiet.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and big then it is furry.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Harry is furry.
True
1
proof
[(triple9)]
("Harry" "is" "furry" "+")
triple9
Charlie is not cold.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "cold" "-")
triple3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is furry.[(triple1)] Charlie is big.[(triple2)] Charlie is cold.[(triple3)] Charlie is green.[(triple4)] Charlie is nice.[(triple5)] Charlie is quiet.[(triple6 OR ((triple4 triple5) -> rule1))] Charlie is rough.[(triple7)] Harry is cold.[(triple8)] Harry is furry.[(triple9)] Harry is green.[(triple10)] Harry is nice.[(triple11)] Harry is rough.[(triple12)] @1: Charlie is furry.[(((triple6 triple2) -> rule2) OR ((((triple4 triple5) -> rule1) triple2) -> rule2))] Harry is quiet.[(((triple10 triple11) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
((triple4 triple5) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple6 triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple4 triple5) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple10 triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1