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