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