Anne is cold. Anne is kind. Anne is not young. Charlie is young. Erin is cold. Erin is green. Erin is nice. Erin is young. Gary is nice. Gary is red. All cold things are nice. If something is kind and not quiet then it is nice. If Anne is young then Anne is nice. Kind things are green. Cold, red things are green. Nice, quiet things are not red.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not young.
("Anne" "is" "young" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is kind and not quiet then it is nice.
((("something" "is" "kind" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "nice" "+"))
If Anne is young then Anne is nice.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "nice" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Cold, red things are green.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Nice, quiet things are not red.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "-"))
Gary is red.
True
1
proof
[(triple10)]
("Gary" "is" "red" "+")
triple10
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is green.
True
2
proof
[(((triple2) -> rule4))]
("Anne" "is" "green" "+")
((triple2) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Anne" "is" "green" "-")
((triple2) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "green" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is cold.[(triple1)] Anne is kind.[(triple2)] Anne is not young.[(triple3)] Charlie is young.[(triple4)] Erin is cold.[(triple5)] Erin is green.[(triple6)] Erin is nice.[(triple7 OR ((triple5) -> rule1))] Erin is young.[(triple8)] Gary is nice.[(triple9)] Gary is red.[(triple10)] @1: Anne is green.[(((triple2) -> rule4))] Anne is nice.[(((triple1) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not young.
("Anne" "is" "young" "-")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
((triple5) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1