Anne is cold. Anne is furry. Anne is not red. Anne is young. Charlie is not cold. Charlie is furry. Charlie is red. Dave is not big. Dave is blue. Dave is red. Dave is young. Harry is quiet. All cold, blue people are not quiet. Big people are not quiet. If Dave is big and Dave is not cold then Dave is quiet. If someone is furry and not red then they are big. If Charlie is cold and Charlie is blue then Charlie is not big. If someone is red and big then they are furry. If Anne is red and Anne is furry then Anne is blue. Quiet people are not young.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is young.
("Anne" "is" "young" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All cold, blue people are not quiet.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "-"))
Big people are not quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "-"))
If Dave is big and Dave is not cold then Dave is quiet.
((("Dave" "is" "big" "+") ("Dave" "is" "cold" "~")) -> ("Dave" "is" "quiet" "+"))
If someone is furry and not red then they are big.
((("someone" "is" "furry" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "big" "+"))
If Charlie is cold and Charlie is blue then Charlie is not big.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "big" "-"))
If someone is red and big then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If Anne is red and Anne is furry then Anne is blue.
((("Anne" "is" "red" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "blue" "+"))
Quiet people are not young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "-"))
Charlie is not cold.
True
1
proof
[(triple5)]
("Charlie" "is" "cold" "-")
triple5
Charlie is not furry.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "furry" "-")
triple6
Anne is big.
True
3
proof
[(((triple2 triple3) -> rule4))]
("Anne" "is" "big" "+")
((triple2 triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
3
inv-proof
[(((triple2 triple3) -> rule4))]
("Anne" "is" "big" "-")
((triple2 triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not quiet.
True
4
proof
[(((((triple2 triple3) -> rule4)) -> rule2))]
("Anne" "is" "quiet" "-")
((((triple2 triple3) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
False
4
inv-proof
[(((((triple2 triple3) -> rule4)) -> rule2))]
("Anne" "is" "quiet" "+")
((((triple2 triple3) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "big" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "blue" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is not red.[(triple3)] Anne is young.[(triple4)] Charlie is furry.[(triple6)] Charlie is not cold.[(triple5)] Charlie is red.[(triple7)] Dave is blue.[(triple9)] Dave is not big.[(triple8)] Dave is red.[(triple10)] Dave is young.[(triple11)] Harry is quiet.[(triple12)] @1: Anne is big.[(((triple2 triple3) -> rule4))] Harry is not young.[(((triple12) -> rule8))] @2: Anne is not quiet.[(((((triple2 triple3) -> rule4)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is not red.
("Anne" "is" "red" "-")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is not big.
("Dave" "is" "big" "-")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple2 triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
((triple12) -> (rule8 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
((((triple2 triple3) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2