Anne is kind. Erin is quiet. Gary is rough. All rough things are nice. All rough, nice things are kind. If something is nice and quiet then it is rough.
Anne is kind.
("Anne" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All rough, nice things are kind.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is nice and quiet then it is rough.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Erin is quiet.
True
1
proof
[(triple2)]
("Erin" "is" "quiet" "+")
triple2
Gary is not rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Gary is nice.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("Gary" "is" "kind" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not kind.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("Gary" "is" "kind" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "-")
Erin is kind.
Unknown
rconc
[@3: Erin is kind.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not rough.
Unknown
inv-rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Anne is kind.[(triple1)] Erin is quiet.[(triple2)] Gary is rough.[(triple3)] @1: Gary is nice.[(((triple3) -> rule1))] @2: Gary is kind.[(((triple3 ((triple3) -> rule1)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2