Anne is blue. Anne is cold. Anne is green. Bob is blue. Bob is green. Bob is kind. Bob is quiet. Charlie is blue. Charlie is cold. Harry is blue. Harry is cold. Harry is green. Harry is kind. Harry is quiet. Harry is rough. Harry is white. Blue people are white. If someone is rough and cold then they are white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is rough and cold then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Bob is green.
True
1
proof
[(triple5)]
("Bob" "is" "green" "+")
triple5
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is green.[(triple3)] Bob is blue.[(triple4)] Bob is green.[(triple5)] Bob is kind.[(triple6)] Bob is quiet.[(triple7)] Charlie is blue.[(triple8)] Charlie is cold.[(triple9)] Harry is blue.[(triple10)] Harry is cold.[(triple11)] Harry is green.[(triple12)] Harry is kind.[(triple13)] Harry is quiet.[(triple14)] Harry is rough.[(triple15)] Harry is white.[(triple16 OR ((triple10) -> rule1) OR ((triple15 triple11) -> rule2))] @1: Anne is white.[(((triple1) -> rule1))] Bob is white.[(((triple4) -> rule1))] Charlie is white.[(((triple8) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is cold.
("Charlie" "is" "cold" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple10) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple15 triple11) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple4) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple8) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1