Charlie is red. Dave is furry. Dave is kind. Dave is not nice. Gary is furry. Gary is kind. Gary is rough. If Gary is rough then Gary is furry. All red, rough things are furry. If Gary is green and Gary is kind then Gary is rough. Nice, red things are cold. Red things are nice. All furry, kind things are not nice. If something is red and nice then it is rough. If something is green and nice then it is rough.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Gary is rough then Gary is furry.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "furry" "+"))
All red, rough things are furry.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If Gary is green and Gary is kind then Gary is rough.
((("Gary" "is" "green" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "rough" "+"))
Nice, red things are cold.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
All furry, kind things are not nice.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "-"))
If something is red and nice then it is rough.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is green and nice then it is rough.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Charlie is red.
True
1
proof
[(triple1)]
("Charlie" "is" "red" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple2)]
("Dave" "is" "furry" "-")
triple2
Gary is not nice.
True
3
proof
[(((triple5 triple6) -> rule6) OR ((((triple7) -> rule1) triple6) -> rule6))]
("Gary" "is" "nice" "-")
((triple5 triple6) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
((((triple7) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule7))]
("Charlie" "is" "rough" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule7))]
("Charlie" "is" "rough" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule5)) -> rule7)) -> rule2))]
("Charlie" "is" "furry" "+")
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not furry.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule5)) -> rule7)) -> rule2))]
("Charlie" "is" "furry" "-")
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "+")
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Charlie is red.[(triple1)] Dave is furry.[(triple2)] Dave is kind.[(triple3)] Dave is not nice.[(triple4 OR ((triple2 triple3) -> rule6))] Gary is furry.[(triple5 OR ((triple7) -> rule1))] Gary is kind.[(triple6)] Gary is rough.[(triple7)] @1: Charlie is nice.[(((triple1) -> rule5))] Gary is not nice.[(((triple5 triple6) -> rule6) OR ((((triple7) -> rule1) triple6) -> rule6))] @2: Charlie is cold.[(((((triple1) -> rule5) triple1) -> rule4))] Charlie is rough.[(((triple1 ((triple1) -> rule5)) -> rule7))] @3: Charlie is furry.[(((triple1 ((triple1 ((triple1) -> rule5)) -> rule7)) -> rule2))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not nice.
("Dave" "is" "nice" "-")
triple4
((triple2 triple3) -> (rule6 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple5
((triple7) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((triple5 triple6) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
((((triple7) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3