Anne is nice. Charlie is round. Erin is blue. Harry is rough. All nice things are kind. All kind things are round. If something is kind then it is smart. Nice, rough things are smart. If something is blue and not kind then it is smart. If Erin is smart and Erin is kind then Erin is not blue.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is kind then it is smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Nice, rough things are smart.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is blue and not kind then it is smart.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "smart" "+"))
If Erin is smart and Erin is kind then Erin is not blue.
((("Erin" "is" "smart" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "blue" "-"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Charlie is not round.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "round" "-")
triple2
Anne is kind.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Erin is smart.
Unknown
rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is nice.[(triple1)] Charlie is round.[(triple2)] Erin is blue.[(triple3)] Harry is rough.[(triple4)] @1: Anne is kind.[(((triple1) -> rule1))] @2: Anne is round.[(((((triple1) -> rule1)) -> rule2))] Anne is smart.[(((((triple1) -> rule1)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2