Anne is rough. Charlie is quiet. Dave is quiet. Fiona is rough. If something is furry then it is rough. If Dave is quiet then Dave is not cold.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If Dave is quiet then Dave is not cold.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "cold" "-"))
Fiona is rough.
True
1
proof
[(triple4)]
("Fiona" "is" "rough" "+")
triple4
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Dave is not cold.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "cold" "-")
((triple3) -> (rule2 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is cold.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is rough.[(triple1)] Charlie is quiet.[(triple2)] Dave is quiet.[(triple3)] Fiona is rough.[(triple4)] @1: Dave is not cold.[(((triple3) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Dave is not cold.
("Dave" "is" "cold" "-")
((triple3) -> (rule2 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1