Anne is cold. Anne is green. Bob is green. Bob is rough. Erin is blue. Erin is cold. Erin is rough. Harry is blue. Harry is rough. Harry is smart. Kind, blue things are smart. If something is smart and green then it is kind. Rough, blue things are cold. If something is nice and green then it is blue. All green things are blue. All kind things are green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Kind, blue things are smart.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is smart and green then it is kind.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Rough, blue things are cold.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is nice and green then it is blue.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Bob is green.
True
1
proof
[(triple3)]
("Bob" "is" "green" "+")
triple3
Harry is not blue.
False
1
inv-proof
[(triple8)]
("Harry" "is" "blue" "-")
triple8
Bob is blue.
True
2
proof
[(((triple3) -> rule5))]
("Bob" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is not cold.
False
3
inv-proof
[(((triple9 triple8) -> rule3))]
("Harry" "is" "cold" "-")
((triple9 triple8) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "kind" "-")
Erin is kind.
Unknown
rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Bob is green.[(triple3)] Bob is rough.[(triple4)] Erin is blue.[(triple5)] Erin is cold.[(triple6 OR ((triple7 triple5) -> rule3))] Erin is rough.[(triple7)] Harry is blue.[(triple8)] Harry is rough.[(triple9)] Harry is smart.[(triple10)] @1: Anne is blue.[(((triple2) -> rule5))] Bob is blue.[(((triple3) -> rule5))] Harry is cold.[(((triple9 triple8) -> rule3))] @2: Bob is cold.[(((triple4 ((triple3) -> rule5)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
((triple7 triple5) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple9 triple8) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple4 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2