Dave is furry. Dave is kind. Dave is rough. Dave is round. Gary is big. Gary is furry. Gary is red. If someone is rough and not furry then they are kind. If someone is rough and red then they are kind. If someone is round and not rough then they are big. If someone is quiet then they are not big. All rough, kind people are round. If someone is rough then they are quiet.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
If someone is rough and not furry then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "kind" "+"))
If someone is rough and red then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is round and not rough then they are big.
((("someone" "is" "round" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "big" "+"))
If someone is quiet then they are not big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "-"))
All rough, kind people are round.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Gary is furry.
True
1
proof
[(triple6)]
("Gary" "is" "furry" "+")
triple6
Gary is not furry.
False
1
inv-proof
[(triple6)]
("Gary" "is" "furry" "-")
triple6
Dave is quiet.
True
2
proof
[(((triple3) -> rule6))]
("Dave" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple3) -> rule6))]
("Dave" "is" "quiet" "-")
((triple3) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not big.
True
3
proof
[(((((triple3) -> rule6)) -> rule4))]
("Dave" "is" "big" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule4))]
("Dave" "is" "big" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is quiet.
Unknown
rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Dave is furry.[(triple1)] Dave is kind.[(triple2)] Dave is rough.[(triple3)] Dave is round.[(triple4 OR ((triple3 triple2) -> rule5))] Gary is big.[(triple5)] Gary is furry.[(triple6)] Gary is red.[(triple7)] @1: Dave is quiet.[(((triple3) -> rule6))] @2: Dave is not big.[(((((triple3) -> rule6)) -> rule4))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple3 triple2) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2