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