Anne is rough. Charlie is kind. Erin is red. Kind people are nice. All red people are white. Red people are not green. All blue people are rough. If someone is nice then they are rough. If Erin is not green then Erin is white.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Red people are not green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "-"))
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Erin is not green then Erin is white.
((("Erin" "is" "green" "~")) -> ("Erin" "is" "white" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Erin is not red.
False
1
inv-proof
[(triple3)]
("Erin" "is" "red" "-")
triple3
Erin is not green.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "green" "-")
((triple3) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is green.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "green" "+")
((triple3) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Charlie is rough.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("Charlie" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Charlie" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not rough.
Unknown
inv-rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is rough.[(triple1)] Charlie is kind.[(triple2)] Erin is red.[(triple3)] @1: Charlie is nice.[(((triple2) -> rule1))] Erin is not green.[(((triple3) -> rule3))] Erin is white.[(((triple3) -> rule2) OR ((((triple3) -> rule3)) -> rule6))] @2: Charlie is rough.[(((((triple2) -> rule1)) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
((triple3) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2