Dave is rough. Erin is green. Fiona is furry. Gary is red. If Gary is quiet and Gary is furry then Gary is rough. Green, rough things are red. Rough things are quiet. Green things are kind. All green things are quiet. If something is red then it is furry.
Dave is rough.
("Dave" "is" "rough" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
If Gary is quiet and Gary is furry then Gary is rough.
((("Gary" "is" "quiet" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "rough" "+"))
Green, rough things are red.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
Rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Erin is green.
True
1
proof
[(triple2)]
("Erin" "is" "green" "+")
triple2
Erin is not green.
False
1
inv-proof
[(triple2)]
("Erin" "is" "green" "-")
triple2
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is rough.[(triple1)] Erin is green.[(triple2)] Fiona is furry.[(triple3)] Gary is red.[(triple4)] @1: Dave is quiet.[(((triple1) -> rule3))] Erin is kind.[(((triple2) -> rule4))] Erin is quiet.[(((triple2) -> rule5))] Gary is furry.[(((triple4) -> rule6))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple4) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1