Anne is kind. Anne is red. Dave is not big. Dave is not white. Erin is green. Erin is kind. Harry is white. If someone is cold and not kind then they are not green. Nice people are green. All nice people are cold. If someone is white then they are nice. If someone is kind then they are not nice. If someone is cold and nice then they are big. If someone is green and not red then they are big. If Erin is green and Erin is nice then Erin is big.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is not white.
("Dave" "is" "white" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is cold and not kind then they are not green.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "green" "-"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind then they are not nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "-"))
If someone is cold and nice then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is green and not red then they are big.
((("someone" "is" "green" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "big" "+"))
If Erin is green and Erin is nice then Erin is big.
((("Erin" "is" "green" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "big" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Harry is not white.
False
1
inv-proof
[(triple7)]
("Harry" "is" "white" "-")
triple7
Erin is not nice.
True
2
proof
[(((triple6) -> rule5))]
("Erin" "is" "nice" "-")
((triple6) -> (rule5 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is nice.
False
2
inv-proof
[(((triple6) -> rule5))]
("Erin" "is" "nice" "+")
((triple6) -> (rule5 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Harry is green.
True
3
proof
[(((((triple7) -> rule4)) -> rule2))]
("Harry" "is" "green" "+")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule3))]
("Harry" "is" "cold" "-")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
True
6
proof
[(((((((triple7) -> rule4)) -> rule3) ((triple7) -> rule4)) -> rule6))]
("Harry" "is" "big" "+")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2)) ((triple7) -> (rule4 % int3))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not big.
False
6
inv-proof
[(((((((triple7) -> rule4)) -> rule3) ((triple7) -> rule4)) -> rule6))]
("Harry" "is" "big" "-")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2)) ((triple7) -> (rule4 % int3))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "cold" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is kind.[(triple1)] Anne is red.[(triple2)] Dave is not big.[(triple3)] Dave is not white.[(triple4)] Erin is green.[(triple5)] Erin is kind.[(triple6)] Harry is white.[(triple7)] @1: Anne is not nice.[(((triple1) -> rule5))] Erin is not nice.[(((triple6) -> rule5))] Harry is nice.[(((triple7) -> rule4))] @2: Harry is cold.[(((((triple7) -> rule4)) -> rule3))] Harry is green.[(((((triple7) -> rule4)) -> rule2))] @3: Harry is big.[(((((((triple7) -> rule4)) -> rule3) ((triple7) -> rule4)) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Dave is not big.
("Dave" "is" "big" "-")
triple3
Dave is not white.
("Dave" "is" "white" "-")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Anne is not nice.
("Anne" "is" "nice" "-")
((triple1) -> (rule5 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
((triple6) -> (rule5 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2)) ((triple7) -> (rule4 % int3))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3