Charlie is nice. Dave is cold. Dave is kind. Dave is nice. Dave is young. Erin is cold. Erin is kind. Erin is nice. Erin is rough. Gary is cold. If Gary is rough and Gary is kind then Gary is quiet.
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If Gary is rough and Gary is kind then Gary is quiet.
((("Gary" "is" "rough" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "quiet" "+"))
Dave is cold.
True
1
proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Dave is not nice.
False
1
inv-proof
[(triple4)]
("Dave" "is" "nice" "-")
triple4
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Charlie is nice.[(triple1)] Dave is cold.[(triple2)] Dave is kind.[(triple3)] Dave is nice.[(triple4)] Dave is young.[(triple5)] Erin is cold.[(triple6)] Erin is kind.[(triple7)] Erin is nice.[(triple8)] Erin is rough.[(triple9)] Gary is cold.[(triple10)]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10