Dave is furry. Gary is nice. Gary is young. If Dave is furry then Dave is blue. All blue people are round. Blue, round people are red. Red, round people are furry. Young, kind people are nice. If Gary is young then Gary is kind.
Dave is furry.
("Dave" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
If Dave is furry then Dave is blue.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "blue" "+"))
All blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Blue, round people are red.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Red, round people are furry.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Young, kind people are nice.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If Gary is young then Gary is kind.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "kind" "+"))
Dave is furry.
True
1
proof
[(triple1)]
("Dave" "is" "furry" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Gary is kind.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "kind" "-")
((triple3) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Dave is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Dave" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Dave" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is not furry.
Unknown
inv-rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "red" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Dave is furry.[(triple1)] Gary is nice.[(triple2 OR ((triple3 ((triple3) -> rule6)) -> rule5))] Gary is young.[(triple3)] @1: Dave is blue.[(((triple1) -> rule1))] Gary is kind.[(((triple3) -> rule6))] @2: Dave is round.[(((((triple1) -> rule1)) -> rule2))] @3: Dave is red.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
((triple3 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3