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