Dave is nice. Erin is red. If something is kind then it is big. If Erin is kind and Erin is young then Erin is blue. Big things are quiet. If something is blue then it is kind. All big, red things are nice. Quiet things are red. If something is nice then it is big. If something is nice and red then it is blue.
Dave is nice.
("Dave" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
If something is kind then it is big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If Erin is kind and Erin is young then Erin is blue.
((("Erin" "is" "kind" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "blue" "+"))
Big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All big, red things are nice.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is nice and red then it is blue.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Dave is nice.
True
1
proof
[(triple1)]
("Dave" "is" "nice" "+")
triple1
Erin is not red.
False
1
inv-proof
[(triple2)]
("Erin" "is" "red" "-")
triple2
Dave is big.
True
2
proof
[(((triple1) -> rule7))]
("Dave" "is" "big" "+")
((triple1) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple1) -> rule7))]
("Dave" "is" "big" "-")
((triple1) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple1) -> rule7)) -> rule3))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule3))]
("Dave" "is" "quiet" "-")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
True
4
proof
[(((((((triple1) -> rule7)) -> rule3)) -> rule6))]
("Dave" "is" "red" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not red.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule3)) -> rule6))]
("Dave" "is" "red" "-")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@5: Erin is big.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule8 <- rule5 <- rule7 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is quiet.
Unknown
rconc
[@6: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- rule8 <- rule5 <- rule7 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not kind.
Unknown
inv-rconc
[@4: Erin is kind.[CWA. Example of deepest failure = (rule4 <- rule8 <- rule5 <- rule1 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is nice.
Unknown
rconc
[@4: Erin is nice.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule4 <- rule2 <- FAIL)]]
("Erin" "is" "nice" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Dave is nice.[(triple1)] Erin is red.[(triple2)] @1: Dave is big.[(((triple1) -> rule7))] @2: Dave is quiet.[(((((triple1) -> rule7)) -> rule3))] @3: Dave is red.[(((((((triple1) -> rule7)) -> rule3)) -> rule6))] @4: Dave is blue.[(((triple1 ((((((triple1) -> rule7)) -> rule3)) -> rule6)) -> rule8))] @5: Dave is kind.[(((((triple1 ((((((triple1) -> rule7)) -> rule3)) -> rule6)) -> rule8)) -> rule4))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((triple1 ((((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1 ((((((triple1) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
int5