Dave is cold. Dave is furry. Dave is green. If someone is cold and green then they are kind. If Dave is smart and Dave is rough then Dave is green. Rough, quiet people are cold. If Dave is smart and Dave is cold then Dave is rough. If someone is rough and furry then they are cold. If someone is green and furry then they are quiet.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
If someone is cold and green then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Dave is smart and Dave is rough then Dave is green.
((("Dave" "is" "smart" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "green" "+"))
Rough, quiet people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If Dave is smart and Dave is cold then Dave is rough.
((("Dave" "is" "smart" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "rough" "+"))
If someone is rough and furry then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and furry then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Dave is green.
True
1
proof
[(triple3)]
("Dave" "is" "green" "+")
triple3
Dave is not green.
False
1
inv-proof
[(triple3)]
("Dave" "is" "green" "-")
triple3
Dave is kind.
True
3
proof
[(((triple1 triple3) -> rule1))]
("Dave" "is" "kind" "+")
((triple1 triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not quiet.
False
3
inv-proof
[(((triple3 triple2) -> rule6))]
("Dave" "is" "quiet" "-")
((triple3 triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is cold.[(triple1)] Dave is furry.[(triple2)] Dave is green.[(triple3)] @1: Dave is kind.[(((triple1 triple3) -> rule1))] Dave is quiet.[(((triple3 triple2) -> rule6))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple1 triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3 triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1