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