Bob is nice. Bob is rough. Erin is big. Erin is cold. Erin is kind. Erin is nice. Erin is rough. If Erin is rough and Erin is quiet then Erin is young. All kind people are quiet. Rough, nice people are kind. All rough, nice people are young. All young people are quiet. All young, big people are nice.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If Erin is rough and Erin is quiet then Erin is young.
((("Erin" "is" "rough" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "young" "+"))
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Rough, nice people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All rough, nice people are young.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
All young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All young, big people are nice.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Erin is cold.
True
1
proof
[(triple4)]
("Erin" "is" "cold" "+")
triple4
Erin is not nice.
False
1
inv-proof
[(triple6 OR ((((triple7 ((triple5) -> rule2)) -> rule1) triple3) -> rule6))]
("Erin" "is" "nice" "-")
triple6
((((triple7 ((triple5) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is quiet.
True
2
proof
[(((triple5) -> rule2) OR ((((triple7 triple6) -> rule3)) -> rule2) OR ((((triple7 triple6) -> rule4)) -> rule5))]
("Erin" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple7 triple6) -> (rule3 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple7 triple6) -> (rule4 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not quiet.
False
2
inv-proof
[(((triple5) -> rule2) OR ((((triple7 triple6) -> rule3)) -> rule2) OR ((((triple7 triple6) -> rule4)) -> rule5))]
("Erin" "is" "quiet" "-")
((triple5) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple7 triple6) -> (rule3 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple7 triple6) -> (rule4 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Bob is quiet.
True
4
proof
[(((((triple2 triple1) -> rule3)) -> rule2) OR ((((triple2 triple1) -> rule4)) -> rule5))]
("Bob" "is" "quiet" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not quiet.
False
4
inv-proof
[(((((triple2 triple1) -> rule3)) -> rule2) OR ((((triple2 triple1) -> rule4)) -> rule5))]
("Bob" "is" "quiet" "-")
((((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is nice.[(triple1)] Bob is rough.[(triple2)] Erin is big.[(triple3)] Erin is cold.[(triple4)] Erin is kind.[(triple5 OR ((triple7 triple6) -> rule3))] Erin is nice.[(triple6 OR ((((triple7 ((triple5) -> rule2)) -> rule1) triple3) -> rule6))] Erin is rough.[(triple7)] @1: Bob is kind.[(((triple2 triple1) -> rule3))] Bob is young.[(((triple2 triple1) -> rule4))] Erin is quiet.[(((triple5) -> rule2) OR ((((triple7 triple6) -> rule3)) -> rule2) OR ((((triple7 triple6) -> rule4)) -> rule5))] Erin is young.[(((triple7 triple6) -> rule4) OR ((triple7 ((triple5) -> rule2)) -> rule1) OR ((triple7 ((((triple7 triple6) -> rule3)) -> rule2)) -> rule1))] @2: Bob is quiet.[(((((triple2 triple1) -> rule3)) -> rule2) OR ((((triple2 triple1) -> rule4)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
((triple7 triple6) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple6
((((triple7 ((triple5) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple2 triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2 triple1) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple7 triple6) -> (rule3 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple7 triple6) -> (rule4 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple7 triple6) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple7 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple7 ((((triple7 triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2