Anne is blue. Anne is smart. Erin is big. Erin is kind. Erin is red. Erin is rough. Erin is smart. If something is red then it is not white. If Erin is kind and Erin is not red then Erin is not rough. Big things are rough. If Anne is blue and Anne is not rough then Anne is kind. If Anne is kind then Anne is smart. If Anne is rough and Anne is not red then Anne is smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If something is red then it is not white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "-"))
If Erin is kind and Erin is not red then Erin is not rough.
((("Erin" "is" "kind" "+") ("Erin" "is" "red" "~")) -> ("Erin" "is" "rough" "-"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If Anne is blue and Anne is not rough then Anne is kind.
((("Anne" "is" "blue" "+") ("Anne" "is" "rough" "~")) -> ("Anne" "is" "kind" "+"))
If Anne is kind then Anne is smart.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "smart" "+"))
If Anne is rough and Anne is not red then Anne is smart.
((("Anne" "is" "rough" "+") ("Anne" "is" "red" "~")) -> ("Anne" "is" "smart" "+"))
Erin is rough.
True
1
proof
[(triple6 OR ((triple3) -> rule3))]
("Erin" "is" "rough" "+")
triple6
((triple3) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Erin is not white.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "white" "-")
((triple5) -> (rule1 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is white.
False
2
inv-proof
[(((triple5) -> rule1))]
("Erin" "is" "white" "+")
((triple5) -> (rule1 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is blue.[(triple1)] Anne is smart.[(triple2)] Erin is big.[(triple3)] Erin is kind.[(triple4)] Erin is red.[(triple5)] Erin is rough.[(triple6 OR ((triple3) -> rule3))] Erin is smart.[(triple7)] @1: Erin is not white.[(((triple5) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
((triple3) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Erin is not white.
("Erin" "is" "white" "-")
((triple5) -> (rule1 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1