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