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