Anne is blue. Erin is nice. Fiona is red. Gary is rough. All blue people are rough. If Anne is round then Anne is quiet. If someone is blue and rough then they are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Anne is round then Anne is quiet.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "quiet" "+"))
If someone is blue and rough then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Erin is nice.
True
1
proof
[(triple2)]
("Erin" "is" "nice" "+")
triple2
Gary is not rough.
False
1
inv-proof
[(triple4)]
("Gary" "is" "rough" "-")
triple4
Anne is rough.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule3))]
("Anne" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule3))]
("Anne" "is" "nice" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "rough" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Erin is nice.[(triple2)] Fiona is red.[(triple3)] Gary is rough.[(triple4)] @1: Anne is rough.[(((triple1) -> rule1))] @2: Anne is nice.[(((triple1 ((triple1) -> rule1)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2