Anne is kind. Anne is smart. Dave is green. Erin is rough. Erin is white. Erin is young. Fiona is green. Blue people are young. All kind people are blue. If Erin is kind and Erin is young then Erin is rough.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Erin is kind and Erin is young then Erin is rough.
((("Erin" "is" "kind" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "rough" "+"))
Fiona is green.
True
1
proof
[(triple7)]
("Fiona" "is" "green" "+")
triple7
Anne is not smart.
False
1
inv-proof
[(triple2)]
("Anne" "is" "smart" "-")
triple2
Anne is blue.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Dave is young.
Unknown
rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "young" "+")
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is kind.[(triple1)] Anne is smart.[(triple2)] Dave is green.[(triple3)] Erin is rough.[(triple4)] Erin is white.[(triple5)] Erin is young.[(triple6)] Fiona is green.[(triple7)] @1: Anne is blue.[(((triple1) -> rule2))] @2: Anne is young.[(((((triple1) -> rule2)) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2