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