Bob is furry. Dave is green. Erin is rough. Gary is cold. If someone is kind and cold then they are green. If Gary is quiet then Gary is green. Furry people are rough.
Bob is furry.
("Bob" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If someone is kind and cold then they are green.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If Gary is quiet then Gary is green.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "green" "+"))
Furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Erin is rough.
True
1
proof
[(triple3)]
("Erin" "is" "rough" "+")
triple3
Erin is not rough.
False
1
inv-proof
[(triple3)]
("Erin" "is" "rough" "-")
triple3
Bob is rough.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is furry.[(triple1)] Dave is green.[(triple2)] Erin is rough.[(triple3)] Gary is cold.[(triple4)] @1: Bob is rough.[(((triple1) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1