Anne is big. Anne is blue. Anne is green. Anne is nice. Anne is quiet. Anne is smart. Bob is big. Bob is green. Bob is kind. Bob is quiet. Erin is big. Erin is blue. Erin is green. Erin is kind. Erin is nice. Erin is smart. Nice people are smart. If someone is nice and kind then they are big. All big, quiet people are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice and kind then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All big, quiet people are nice.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Erin is smart.
True
1
proof
[(triple16 OR ((triple15) -> rule1))]
("Erin" "is" "smart" "+")
triple16
((triple15) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is not kind.
False
1
inv-proof
[(triple9)]
("Bob" "is" "kind" "-")
triple9
Bob is nice.
True
3
proof
[(((triple7 triple10) -> rule3))]
("Bob" "is" "nice" "+")
((triple7 triple10) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
3
inv-proof
[(((triple7 triple10) -> rule3))]
("Bob" "is" "nice" "-")
((triple7 triple10) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
True
4
proof
[(((((triple7 triple10) -> rule3)) -> rule1))]
("Bob" "is" "smart" "+")
((((triple7 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((((triple7 triple10) -> rule3)) -> rule1))]
("Bob" "is" "smart" "-")
((((triple7 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is green.[(triple3)] Anne is nice.[(triple4 OR ((triple1 triple5) -> rule3))] Anne is quiet.[(triple5)] Anne is smart.[(triple6 OR ((triple4) -> rule1) OR ((((triple1 triple5) -> rule3)) -> rule1))] Bob is big.[(triple7)] Bob is green.[(triple8)] Bob is kind.[(triple9)] Bob is quiet.[(triple10)] Erin is big.[(triple11 OR ((triple15 triple14) -> rule2))] Erin is blue.[(triple12)] Erin is green.[(triple13)] Erin is kind.[(triple14)] Erin is nice.[(triple15)] Erin is smart.[(triple16 OR ((triple15) -> rule1))] @1: Bob is nice.[(((triple7 triple10) -> rule3))] @2: Bob is smart.[(((((triple7 triple10) -> rule3)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple1 triple5) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple4) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple1 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
triple8
Bob is kind.
("Bob" "is" "kind" "+")
triple9
Bob is quiet.
("Bob" "is" "quiet" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple11
((triple15 triple14) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple12
Erin is green.
("Erin" "is" "green" "+")
triple13
Erin is kind.
("Erin" "is" "kind" "+")
triple14
Erin is nice.
("Erin" "is" "nice" "+")
triple15
Erin is smart.
("Erin" "is" "smart" "+")
triple16
((triple15) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple7 triple10) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple7 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2