Anne is big. Anne is cold. Anne is green. Anne is kind. Anne is red. Bob is big. Bob is cold. Bob is green. Bob is red. Bob is smart. If Anne is big and Anne is green then Anne is not quiet. If something is big and not quiet then it is not smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
If Anne is big and Anne is green then Anne is not quiet.
((("Anne" "is" "big" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "quiet" "-"))
If something is big and not quiet then it is not smart.
((("something" "is" "big" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "smart" "-"))
Anne is kind.
True
1
proof
[(triple4)]
("Anne" "is" "kind" "+")
triple4
Bob is not big.
False
1
inv-proof
[(triple6)]
("Bob" "is" "big" "-")
triple6
Anne is not quiet.
True
3
proof
[(((triple1 triple3) -> rule1))]
("Anne" "is" "quiet" "-")
((triple1 triple3) -> (rule1 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is quiet.
False
3
inv-proof
[(((triple1 triple3) -> rule1))]
("Anne" "is" "quiet" "+")
((triple1 triple3) -> (rule1 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is not smart.
True
5
proof
[(((triple1 ((triple1 triple3) -> rule1)) -> rule2))]
("Anne" "is" "smart" "-")
((triple1 ((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
int2
Anne is smart.
False
5
inv-proof
[(((triple1 ((triple1 triple3) -> rule1)) -> rule2))]
("Anne" "is" "smart" "+")
((triple1 ((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
int2
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is green.[(triple3)] Anne is kind.[(triple4)] Anne is red.[(triple5)] Bob is big.[(triple6)] Bob is cold.[(triple7)] Bob is green.[(triple8)] Bob is red.[(triple9)] Bob is smart.[(triple10)] @1: Anne is not quiet.[(((triple1 triple3) -> rule1))] @2: Anne is not smart.[(((triple1 ((triple1 triple3) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple6
Bob is cold.
("Bob" "is" "cold" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
triple8
Bob is red.
("Bob" "is" "red" "+")
triple9
Bob is smart.
("Bob" "is" "smart" "+")
triple10
Anne is not quiet.
("Anne" "is" "quiet" "-")
((triple1 triple3) -> (rule1 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
((triple1 ((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
int2