Anne is furry. Anne is kind. Anne is rough. Anne is not white. Charlie is cold. Charlie is kind. Charlie is rough. Charlie is round. Charlie is white. Dave is not cold. Dave is green. Dave is white. Gary is cold. Gary is kind. Gary is rough. If something is round then it is furry. Rough things are round. If something is furry and not kind then it is rough.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not white.
("Anne" "is" "white" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is furry and not kind then it is rough.
((("something" "is" "furry" "+") ("something" "is" "kind" "~")) -> ("something" "is" "rough" "+"))
Dave is not cold.
True
1
proof
[(triple10)]
("Dave" "is" "cold" "-")
triple10
Anne is white.
False
1
inv-proof
[(triple4)]
("Anne" "is" "white" "+")
triple4
Gary is round.
True
2
proof
[(((triple15) -> rule2))]
("Gary" "is" "round" "+")
((triple15) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not round.
False
2
inv-proof
[(((triple15) -> rule2))]
("Gary" "is" "round" "-")
((triple15) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
True
3
proof
[(((((triple15) -> rule2)) -> rule1))]
("Gary" "is" "furry" "+")
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple15) -> rule2)) -> rule1))]
("Gary" "is" "furry" "-")
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not furry.
Unknown
inv-rconc
[@3: Dave is furry.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is furry.[(triple1 OR ((((triple3) -> rule2)) -> rule1))] Anne is kind.[(triple2)] Anne is not white.[(triple4)] Anne is rough.[(triple3)] Charlie is cold.[(triple5)] Charlie is kind.[(triple6)] Charlie is rough.[(triple7)] Charlie is round.[(triple8 OR ((triple7) -> rule2))] Charlie is white.[(triple9)] Dave is green.[(triple11)] Dave is not cold.[(triple10)] Dave is white.[(triple12)] Gary is cold.[(triple13)] Gary is kind.[(triple14)] Gary is rough.[(triple15)] @1: Anne is round.[(((triple3) -> rule2))] Charlie is furry.[(((triple8) -> rule1) OR ((((triple7) -> rule2)) -> rule1))] Gary is round.[(((triple15) -> rule2))] @2: Gary is furry.[(((((triple15) -> rule2)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not white.
("Anne" "is" "white" "-")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
((triple7) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple11
Dave is not cold.
("Dave" "is" "cold" "-")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple12
Gary is cold.
("Gary" "is" "cold" "+")
triple13
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Anne is round.
("Anne" "is" "round" "+")
((triple3) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple8) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple15) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2