Bob is furry. Dave is kind. Gary is quiet. Nice things are rough. If Gary is nice and Gary is rough then Gary is kind. Rough things are blue. If Dave is quiet and Dave is big then Dave is rough. If something is kind then it is nice. If Gary is quiet and Gary is rough then Gary is furry.
Bob is furry.
("Bob" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Gary is nice and Gary is rough then Gary is kind.
((("Gary" "is" "nice" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "kind" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If Dave is quiet and Dave is big then Dave is rough.
((("Dave" "is" "quiet" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "rough" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If Gary is quiet and Gary is rough then Gary is furry.
((("Gary" "is" "quiet" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "furry" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Dave is nice.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
True
4
proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
("Dave" "is" "blue" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not blue.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
("Dave" "is" "blue" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Gary" "is" "kind" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not blue.
Unknown
inv-rconc
[@3: Bob is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule5 <- FAIL)]]
("Bob" "is" "blue" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Gary" "is" "nice" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is furry.[(triple1)] Dave is kind.[(triple2)] Gary is quiet.[(triple3)] @1: Dave is nice.[(((triple2) -> rule5))] @2: Dave is rough.[(((((triple2) -> rule5)) -> rule1))] @3: Dave is blue.[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3