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