Anne is quiet. Anne is red. Charlie is quiet. Charlie is rough. Dave is nice. Dave is rough. Dave is white. Gary is quiet. Gary is red. Gary is rough. Nice, rough people are blue. If someone is quiet and rough then they are blue. If Gary is furry then Gary is white. If someone is rough and white then they are furry. Furry people are quiet. If Gary is blue and Gary is quiet then Gary is white.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Nice, rough people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and rough then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If Gary is furry then Gary is white.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "white" "+"))
If someone is rough and white then they are furry.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is blue and Gary is quiet then Gary is white.
((("Gary" "is" "blue" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "white" "+"))
Gary is rough.
True
1
proof
[(triple10)]
("Gary" "is" "rough" "+")
triple10
Gary is not red.
False
1
inv-proof
[(triple9)]
("Gary" "is" "red" "-")
triple9
Charlie is blue.
True
3
proof
[(((triple3 triple4) -> rule2))]
("Charlie" "is" "blue" "+")
((triple3 triple4) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Dave is not furry.
False
3
inv-proof
[(((triple6 triple7) -> rule4))]
("Dave" "is" "furry" "-")
((triple6 triple7) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
True
4
proof
[(((((triple6 triple7) -> rule4)) -> rule5))]
("Dave" "is" "quiet" "+")
((((triple6 triple7) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is not white.
False
5
inv-proof
[(((((triple8 triple10) -> rule2) triple8) -> rule6))]
("Gary" "is" "white" "-")
((((triple8 triple10) -> (rule2 % int2)) triple8) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
True
7
proof
[(((triple10 ((((triple8 triple10) -> rule2) triple8) -> rule6)) -> rule4))]
("Gary" "is" "furry" "+")
((triple10 ((((triple8 triple10) -> (rule2 % int3)) triple8) -> (rule6 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not furry.
False
7
inv-proof
[(((triple10 ((((triple8 triple10) -> rule2) triple8) -> rule6)) -> rule4))]
("Gary" "is" "furry" "-")
((triple10 ((((triple8 triple10) -> (rule2 % int3)) triple8) -> (rule6 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "furry" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "furry" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is quiet.[(triple1)] Anne is red.[(triple2)] Charlie is quiet.[(triple3)] Charlie is rough.[(triple4)] Dave is nice.[(triple5)] Dave is rough.[(triple6)] Dave is white.[(triple7)] Gary is quiet.[(triple8)] Gary is red.[(triple9)] Gary is rough.[(triple10)] @1: Charlie is blue.[(((triple3 triple4) -> rule2))] Dave is blue.[(((triple5 triple6) -> rule1) OR ((((((triple6 triple7) -> rule4)) -> rule5) triple6) -> rule2))] Dave is furry.[(((triple6 triple7) -> rule4))] Gary is blue.[(((triple8 triple10) -> rule2))] @2: Dave is quiet.[(((((triple6 triple7) -> rule4)) -> rule5))] Gary is white.[(((((triple8 triple10) -> rule2) triple8) -> rule6))] @3: Gary is furry.[(((triple10 ((((triple8 triple10) -> rule2) triple8) -> rule6)) -> rule4))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3 triple4) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple5 triple6) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((((triple6 triple7) -> (rule4 % int3))) -> (rule5 % int2)) triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple6 triple7) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple8 triple10) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple6 triple7) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple8 triple10) -> (rule2 % int2)) triple8) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple10 ((((triple8 triple10) -> (rule2 % int3)) triple8) -> (rule6 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3