Anne is big. Anne is kind. Anne is nice. Anne is rough. Anne is young. Bob is big. Bob is kind. Bob is nice. Bob is rough. Gary is nice. Gary is rough. Gary is young. All kind, nice people are smart. If Gary is green and Gary is rough then Gary is kind. If Gary is nice and Gary is rough then Gary is green.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
All kind, nice people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Gary is green and Gary is rough then Gary is kind.
((("Gary" "is" "green" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "kind" "+"))
If Gary is nice and Gary is rough then Gary is green.
((("Gary" "is" "nice" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "green" "+"))
Bob is big.
True
1
proof
[(triple6)]
("Bob" "is" "big" "+")
triple6
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Bob is smart.
True
3
proof
[(((triple7 triple8) -> rule1))]
("Bob" "is" "smart" "+")
((triple7 triple8) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is not green.
False
3
inv-proof
[(((triple10 triple11) -> rule3))]
("Gary" "is" "green" "-")
((triple10 triple11) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
True
5
proof
[(((((triple10 triple11) -> rule3) triple11) -> rule2))]
("Gary" "is" "kind" "+")
((((triple10 triple11) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not kind.
False
5
inv-proof
[(((((triple10 triple11) -> rule3) triple11) -> rule2))]
("Gary" "is" "kind" "-")
((((triple10 triple11) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
True
7
proof
[(((((((triple10 triple11) -> rule3) triple11) -> rule2) triple10) -> rule1))]
("Gary" "is" "smart" "+")
((((((triple10 triple11) -> (rule3 % int3)) triple11) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not smart.
False
7
inv-proof
[(((((((triple10 triple11) -> rule3) triple11) -> rule2) triple10) -> rule1))]
("Gary" "is" "smart" "-")
((((((triple10 triple11) -> (rule3 % int3)) triple11) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is rough.[(triple4)] Anne is young.[(triple5)] Bob is big.[(triple6)] Bob is kind.[(triple7)] Bob is nice.[(triple8)] Bob is rough.[(triple9)] Gary is nice.[(triple10)] Gary is rough.[(triple11)] Gary is young.[(triple12)] @1: Anne is smart.[(((triple2 triple3) -> rule1))] Bob is smart.[(((triple7 triple8) -> rule1))] Gary is green.[(((triple10 triple11) -> rule3))] @2: Gary is kind.[(((((triple10 triple11) -> rule3) triple11) -> rule2))] @3: Gary is smart.[(((((((triple10 triple11) -> rule3) triple11) -> rule2) triple10) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
triple8
Bob is rough.
("Bob" "is" "rough" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Anne is smart.
("Anne" "is" "smart" "+")
((triple2 triple3) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple7 triple8) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple10 triple11) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple10 triple11) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple10 triple11) -> (rule3 % int3)) triple11) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3