Anne is cold. Anne is green. Anne is kind. Anne is nice. Anne is quiet. Bob is kind. Bob is quiet. Harry is green. Harry is nice. Harry is quiet. Harry is rough. Harry is smart. If Bob is kind and Bob is quiet then Bob is cold. All kind, cold people are green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Bob is kind and Bob is quiet then Bob is cold.
((("Bob" "is" "kind" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "cold" "+"))
All kind, cold people are green.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Bob is kind.
True
1
proof
[(triple6)]
("Bob" "is" "kind" "+")
triple6
Harry is not quiet.
False
1
inv-proof
[(triple10)]
("Harry" "is" "quiet" "-")
triple10
Bob is cold.
True
3
proof
[(((triple6 triple7) -> rule1))]
("Bob" "is" "cold" "+")
((triple6 triple7) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
3
inv-proof
[(((triple6 triple7) -> rule1))]
("Bob" "is" "cold" "-")
((triple6 triple7) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2 OR ((triple3 triple1) -> rule2))] Anne is kind.[(triple3)] Anne is nice.[(triple4)] Anne is quiet.[(triple5)] Bob is kind.[(triple6)] Bob is quiet.[(triple7)] Harry is green.[(triple8)] Harry is nice.[(triple9)] Harry is quiet.[(triple10)] Harry is rough.[(triple11)] Harry is smart.[(triple12)] @1: Bob is cold.[(((triple6 triple7) -> rule1))] @2: Bob is green.[(((triple6 ((triple6 triple7) -> rule1)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple3 triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Bob is cold.
("Bob" "is" "cold" "+")
((triple6 triple7) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple6 ((triple6 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2