Anne is big. Anne is blue. Anne is furry. Anne is rough. Anne is white. Charlie is rough. Harry is big. Harry is cold. Harry is furry. Harry is quiet. If Harry is cold and Harry is blue then Harry is furry. If someone is cold and quiet then they are white. Cold, white people are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is cold and Harry is blue then Harry is furry.
((("Harry" "is" "cold" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "furry" "+"))
If someone is cold and quiet then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Cold, white people are big.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Charlie is rough.
True
1
proof
[(triple6)]
("Charlie" "is" "rough" "+")
triple6
Harry is not cold.
False
1
inv-proof
[(triple8)]
("Harry" "is" "cold" "-")
triple8
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is furry.[(triple3)] Anne is rough.[(triple4)] Anne is white.[(triple5)] Charlie is rough.[(triple6)] Harry is big.[(triple7 OR ((triple8 ((triple8 triple10) -> rule2)) -> rule3))] Harry is cold.[(triple8)] Harry is furry.[(triple9)] Harry is quiet.[(triple10)] @1: Harry is white.[(((triple8 triple10) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple8 ((triple8 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
((triple8 triple10) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1