Anne is big. Anne is blue. Anne is furry. Anne is red. Anne is rough. Anne is round. Anne is white. Dave is blue. Dave is red. Dave is rough. Dave is white. Gary is big. Gary is furry. Gary is red. Gary is rough. Gary is white. If Gary is round and Gary is furry then Gary is blue. If Gary is white then Gary is round. If Dave is big and Dave is red then Dave is round. Furry, blue things are red. Big, red things are white. Blue, round things are rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is round and Gary is furry then Gary is blue.
((("Gary" "is" "round" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "blue" "+"))
If Gary is white then Gary is round.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "round" "+"))
If Dave is big and Dave is red then Dave is round.
((("Dave" "is" "big" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "round" "+"))
Furry, blue things are red.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Big, red things are white.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Blue, round things are rough.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Anne is red.
True
1
proof
[(triple4 OR ((triple3 triple2) -> rule4))]
("Anne" "is" "red" "+")
triple4
((triple3 triple2) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not white.
False
1
inv-proof
[(triple7 OR ((triple1 triple4) -> rule5) OR ((triple1 ((triple3 triple2) -> rule4)) -> rule5))]
("Anne" "is" "white" "-")
triple7
((triple1 triple4) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple1 ((triple3 triple2) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Gary is round.
True
2
proof
[(((triple16) -> rule2) OR ((((triple12 triple14) -> rule5)) -> rule2))]
("Gary" "is" "round" "+")
((triple16) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple12 triple14) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not round.
False
2
inv-proof
[(((triple16) -> rule2) OR ((((triple12 triple14) -> rule5)) -> rule2))]
("Gary" "is" "round" "-")
((triple16) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple12 triple14) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is furry.[(triple3)] Anne is red.[(triple4 OR ((triple3 triple2) -> rule4))] Anne is rough.[(triple5 OR ((triple2 triple6) -> rule6))] Anne is round.[(triple6)] Anne is white.[(triple7 OR ((triple1 triple4) -> rule5) OR ((triple1 ((triple3 triple2) -> rule4)) -> rule5))] Dave is blue.[(triple8)] Dave is red.[(triple9)] Dave is rough.[(triple10)] Dave is white.[(triple11)] Gary is big.[(triple12)] Gary is furry.[(triple13)] Gary is red.[(triple14 OR ((triple13 ((((triple16) -> rule2) triple13) -> rule1)) -> rule4))] Gary is rough.[(triple15 OR ((((((triple16) -> rule2) triple13) -> rule1) ((triple16) -> rule2)) -> rule6) OR ((((((triple16) -> rule2) triple13) -> rule1) ((((triple12 triple14) -> rule5)) -> rule2)) -> rule6) OR ((((((((triple12 triple14) -> rule5)) -> rule2) triple13) -> rule1) ((triple16) -> rule2)) -> rule6) OR ((((((((triple12 triple14) -> rule5)) -> rule2) triple13) -> rule1) ((((triple12 triple14) -> rule5)) -> rule2)) -> rule6))] Gary is white.[(triple16 OR ((triple12 triple14) -> rule5))] @1: Gary is round.[(((triple16) -> rule2) OR ((((triple12 triple14) -> rule5)) -> rule2))] @2: Gary is blue.[(((((triple16) -> rule2) triple13) -> rule1) OR ((((((triple12 triple14) -> rule5)) -> rule2) triple13) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple3 triple2) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple2 triple6) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple1 triple4) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple1 ((triple3 triple2) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is furry.
("Gary" "is" "furry" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
((triple13 ((((triple16) -> (rule2 % int3)) triple13) -> (rule1 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
triple15
((((((triple16) -> (rule2 % int3)) triple13) -> (rule1 % int2)) ((triple16) -> (rule2 % int3))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple16) -> (rule2 % int4)) triple13) -> (rule1 % int3)) ((((triple12 triple14) -> (rule5 % int2))) -> (rule2 % int4))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
((((((((triple12 triple14) -> (rule5 % int4))) -> (rule2 % int3)) triple13) -> (rule1 % int2)) ((triple16) -> (rule2 % int3))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((((((((triple12 triple14) -> (rule5 % int4))) -> (rule2 % int3)) triple13) -> (rule1 % int2)) ((((triple12 triple14) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
triple16
((triple12 triple14) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple16) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple12 triple14) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple16) -> (rule2 % int2)) triple13) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple12 triple14) -> (rule5 % int3))) -> (rule2 % int2)) triple13) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3