Anne is blue. Anne is cold. Anne is quiet. Anne is red. Anne is round. Anne is young. Bob is rough. Dave is blue. Dave is red. Dave is round. Dave is young. Gary is cold. If Gary is round then Gary is rough. If something is round and quiet then it is blue. Cold, quiet things are round. All cold things are young. If something is round then it is young. If something is round then it is young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If Gary is round then Gary is rough.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "rough" "+"))
If something is round and quiet then it is blue.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Cold, quiet things are round.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Dave is blue.
True
1
proof
[(triple8)]
("Dave" "is" "blue" "+")
triple8
Gary is not cold.
False
1
inv-proof
[(triple12)]
("Gary" "is" "cold" "-")
triple12
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is blue.[(triple1 OR ((triple5 triple3) -> rule2) OR ((((triple2 triple3) -> rule3) triple3) -> rule2))] Anne is cold.[(triple2)] Anne is quiet.[(triple3)] Anne is red.[(triple4)] Anne is round.[(triple5 OR ((triple2 triple3) -> rule3))] Anne is young.[(triple6 OR ((triple2) -> rule4) OR ((triple5) -> rule5) OR ((triple5) -> rule6) OR ((((triple2 triple3) -> rule3)) -> rule5) OR ((((triple2 triple3) -> rule3)) -> rule6))] Bob is rough.[(triple7)] Dave is blue.[(triple8)] Dave is red.[(triple9)] Dave is round.[(triple10)] Dave is young.[(triple11 OR ((triple10) -> rule5) OR ((triple10) -> rule6))] Gary is cold.[(triple12)] @1: Gary is young.[(((triple12) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple5 triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple2 triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple2 triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple6
((triple2) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple5) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple5) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple2 triple3) -> (rule3 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
((triple10) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple10) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple12
Gary is young.
("Gary" "is" "young" "+")
((triple12) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1