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