Charlie is blue. Charlie is cold. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is smart. Erin is kind. Erin is quiet. Erin is red. Harry is blue. If Erin is blue and Erin is smart then Erin is nice. All quiet people are red. All blue people are kind. If Harry is cold and Harry is smart then Harry is nice. If Harry is cold and Harry is smart then Harry is kind. Nice, red people are quiet.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Erin is blue and Erin is smart then Erin is nice.
((("Erin" "is" "blue" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "nice" "+"))
All quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Harry is cold and Harry is smart then Harry is nice.
((("Harry" "is" "cold" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "nice" "+"))
If Harry is cold and Harry is smart then Harry is kind.
((("Harry" "is" "cold" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "kind" "+"))
Nice, red people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Erin is kind.
True
1
proof
[(triple7)]
("Erin" "is" "kind" "+")
triple7
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is red.
True
2
proof
[(((triple5) -> rule2))]
("Charlie" "is" "red" "+")
((triple5) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple10) -> rule3))]
("Harry" "is" "kind" "-")
((triple10) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is quiet.
Unknown
rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Harry" "is" "quiet" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is kind.[(triple3 OR ((triple1) -> rule3))] Charlie is nice.[(triple4)] Charlie is quiet.[(triple5)] Charlie is smart.[(triple6)] Erin is kind.[(triple7)] Erin is quiet.[(triple8)] Erin is red.[(triple9 OR ((triple8) -> rule2))] Harry is blue.[(triple10)] @1: Charlie is red.[(((triple5) -> rule2))] Harry is kind.[(((triple10) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
((triple8) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Charlie is red.
("Charlie" "is" "red" "+")
((triple5) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple10) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1