Charlie is cold. Charlie is kind. Charlie is smart. Dave is cold. Dave is green. Dave is quiet. Erin is green. Erin is smart. Harry is green. Harry is kind. Harry is quiet. Harry is smart. All kind, blue things are cold. All smart, kind things are green. All cold things are green. All quiet, green things are smart. If something is blue and not quiet then it is smart. Green, rough things are not smart. All green, blue things are not rough. If something is quiet and not blue then it is rough.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All kind, blue things are cold.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All smart, kind things are green.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
All quiet, green things are smart.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is blue and not quiet then it is smart.
((("something" "is" "blue" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "smart" "+"))
Green, rough things are not smart.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "-"))
All green, blue things are not rough.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "-"))
If something is quiet and not blue then it is rough.
((("something" "is" "quiet" "+") ("something" "is" "blue" "~")) -> ("something" "is" "rough" "+"))
Dave is quiet.
True
1
proof
[(triple6)]
("Dave" "is" "quiet" "+")
triple6
Dave is not cold.
False
1
inv-proof
[(triple4)]
("Dave" "is" "cold" "-")
triple4
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "rough" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is cold.[(triple1)] Charlie is kind.[(triple2)] Charlie is smart.[(triple3)] Dave is cold.[(triple4)] Dave is green.[(triple5 OR ((triple4) -> rule3))] Dave is quiet.[(triple6)] Erin is green.[(triple7)] Erin is smart.[(triple8)] Harry is green.[(triple9 OR ((triple12 triple10) -> rule2))] Harry is kind.[(triple10)] Harry is quiet.[(triple11)] Harry is smart.[(triple12 OR ((triple11 triple9) -> rule4))] @1: Charlie is green.[(((triple1) -> rule3) OR ((triple3 triple2) -> rule2))] Dave is smart.[(((triple6 triple5) -> rule4) OR ((triple6 ((triple4) -> rule3)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
((triple4) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
((triple12 triple10) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple11 triple9) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple6 triple5) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple6 ((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2