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