Anne is blue. Anne is not quiet. Anne is red. Anne is smart. Anne is young. Charlie is blue. Charlie is furry. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is young. Gary is furry. Gary is nice. Gary is quiet. Gary is smart. If something is blue and red then it is nice. If something is nice and not red then it is furry. All furry, red things are quiet. If Gary is quiet and Gary is nice then Gary is furry. All red, young things are blue. Red, quiet things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is blue and red then it is nice.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not red then it is furry.
((("something" "is" "nice" "+") ("something" "is" "red" "~")) -> ("something" "is" "furry" "+"))
All furry, red things are quiet.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Gary is quiet and Gary is nice then Gary is furry.
((("Gary" "is" "quiet" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "furry" "+"))
All red, young things are blue.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Red, quiet things are blue.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Gary is furry.
True
1
proof
[(triple12 OR ((triple14 triple13) -> rule4))]
("Gary" "is" "furry" "+")
triple12
((triple14 triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not nice.
False
1
inv-proof
[(triple13)]
("Gary" "is" "nice" "-")
triple13
Anne is nice.
True
3
proof
[(((triple1 triple3) -> rule1) OR ((((triple3 triple5) -> rule5) triple3) -> rule1))]
("Anne" "is" "nice" "+")
((triple1 triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3 triple5) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((triple1 triple3) -> rule1) OR ((((triple3 triple5) -> rule5) triple3) -> rule1))]
("Anne" "is" "nice" "-")
((triple1 triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3 triple5) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "blue" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Anne is blue.[(triple1 OR ((triple3 triple5) -> rule5))] Anne is not quiet.[(triple2)] Anne is red.[(triple3)] Anne is smart.[(triple4)] Anne is young.[(triple5)] Charlie is blue.[(triple6 OR ((triple10 triple11) -> rule5) OR ((triple10 triple9) -> rule6) OR ((triple10 ((triple7 triple10) -> rule3)) -> rule6))] Charlie is furry.[(triple7)] Charlie is nice.[(triple8 OR ((triple6 triple10) -> rule1) OR ((((triple10 triple11) -> rule5) triple10) -> rule1) OR ((((triple10 triple9) -> rule6) triple10) -> rule1) OR ((((triple10 ((triple7 triple10) -> rule3)) -> rule6) triple10) -> rule1))] Charlie is quiet.[(triple9 OR ((triple7 triple10) -> rule3))] Charlie is red.[(triple10)] Charlie is young.[(triple11)] Gary is furry.[(triple12 OR ((triple14 triple13) -> rule4))] Gary is nice.[(triple13)] Gary is quiet.[(triple14)] Gary is smart.[(triple15)] @1: Anne is nice.[(((triple1 triple3) -> rule1) OR ((((triple3 triple5) -> rule5) triple3) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple3 triple5) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
((triple10 triple11) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple10 triple9) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple10 ((triple7 triple10) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
((triple6 triple10) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple10 triple11) -> (rule5 % int2)) triple10) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple10 triple9) -> (rule6 % int2)) triple10) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple10 ((triple7 triple10) -> (rule3 % int3))) -> (rule6 % int2)) triple10) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
((triple7 triple10) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is young.
("Charlie" "is" "young" "+")
triple11
Gary is furry.
("Gary" "is" "furry" "+")
triple12
((triple14 triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Anne is nice.
("Anne" "is" "nice" "+")
((triple1 triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3 triple5) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2