Bob is big. Bob is furry. Bob is kind. Bob is nice. Erin is kind. Erin is quiet. Erin is smart. All big, quiet people are nice. If someone is kind then they are green. If someone is green then they are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All big, quiet people are nice.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Bob is big.
True
1
proof
[(triple1 OR ((((triple3) -> rule2)) -> rule3))]
("Bob" "is" "big" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Erin is not quiet.
False
1
inv-proof
[(triple6)]
("Erin" "is" "quiet" "-")
triple6
Erin is green.
True
2
proof
[(((triple5) -> rule2))]
("Erin" "is" "green" "+")
((triple5) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "green" "-")
((triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is big.
True
3
proof
[(((((triple5) -> rule2)) -> rule3))]
("Erin" "is" "big" "+")
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule3))]
("Erin" "is" "big" "-")
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
True
5
proof
[(((((((triple5) -> rule2)) -> rule3) triple6) -> rule1))]
("Erin" "is" "nice" "+")
((((((triple5) -> (rule2 % int3))) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not nice.
False
5
inv-proof
[(((((((triple5) -> rule2)) -> rule3) triple6) -> rule1))]
("Erin" "is" "nice" "-")
((((((triple5) -> (rule2 % int3))) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is big.[(triple1 OR ((((triple3) -> rule2)) -> rule3))] Bob is furry.[(triple2)] Bob is kind.[(triple3)] Bob is nice.[(triple4)] Erin is kind.[(triple5)] Erin is quiet.[(triple6)] Erin is smart.[(triple7)] @1: Bob is green.[(((triple3) -> rule2))] Erin is green.[(((triple5) -> rule2))] @2: Erin is big.[(((((triple5) -> rule2)) -> rule3))] @3: Erin is nice.[(((((((triple5) -> rule2)) -> rule3) triple6) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple5) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple5) -> (rule2 % int3))) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3