Anne is blue. Anne is quiet. Anne is smart. Bob is blue. Bob is not cold. Bob is nice. Bob is quiet. Bob is not round. Bob is smart. Harry is big. Harry is not blue. Harry is nice. Harry is quiet. Harry is round. Harry is not smart. If something is smart and blue then it is nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If something is smart and blue then it is nice.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple10)]
("Harry" "is" "big" "-")
triple10
Anne is nice.
True
3
proof
[(((triple3 triple1) -> rule1))]
("Anne" "is" "nice" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
3
inv-proof
[(((triple3 triple1) -> rule1))]
("Anne" "is" "nice" "-")
((triple3 triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is blue.[(triple1)] Anne is quiet.[(triple2)] Anne is smart.[(triple3)] Bob is blue.[(triple4)] Bob is nice.[(triple6 OR ((triple9 triple4) -> rule1))] Bob is not cold.[(triple5)] Bob is not round.[(triple8)] Bob is quiet.[(triple7)] Bob is smart.[(triple9)] Harry is big.[(triple10)] Harry is nice.[(triple12)] Harry is not blue.[(triple11)] Harry is not smart.[(triple15)] Harry is quiet.[(triple13)] Harry is round.[(triple14)] @1: Anne is nice.[(((triple3 triple1) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple6
((triple9 triple4) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
triple5
Bob is not round.
("Bob" "is" "round" "-")
triple8
Bob is quiet.
("Bob" "is" "quiet" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Harry is not blue.
("Harry" "is" "blue" "-")
triple11
Harry is not smart.
("Harry" "is" "smart" "-")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Anne is nice.
("Anne" "is" "nice" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1