Dave is young. Erin is red. Erin is not smart. All quiet things are big. Young things are rough. If Erin is rough and Erin is not young then Erin is kind. Young, rough things are quiet. All young, kind things are quiet. If something is smart and not quiet then it is red. If Erin is smart then Erin is not big. If Erin is red and Erin is kind then Erin is big.
Dave is young.
("Dave" "is" "young" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Erin is rough and Erin is not young then Erin is kind.
((("Erin" "is" "rough" "+") ("Erin" "is" "young" "~")) -> ("Erin" "is" "kind" "+"))
Young, rough things are quiet.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All young, kind things are quiet.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and not quiet then it is red.
((("something" "is" "smart" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "red" "+"))
If Erin is smart then Erin is not big.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "big" "-"))
If Erin is red and Erin is kind then Erin is big.
((("Erin" "is" "red" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "big" "+"))
Erin is red.
True
1
proof
[(triple2)]
("Erin" "is" "red" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple1)]
("Dave" "is" "young" "-")
triple1
Dave is rough.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule4))]
("Dave" "is" "quiet" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not quiet.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule4))]
("Dave" "is" "quiet" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
True
5
proof
[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule1))]
("Dave" "is" "big" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not big.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule1))]
("Dave" "is" "big" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "quiet" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "red" "+")
Erin is not big.
Unknown
inv-rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is young.[(triple1)] Erin is not smart.[(triple3)] Erin is red.[(triple2)] @1: Dave is rough.[(((triple1) -> rule2))] @2: Dave is quiet.[(((triple1 ((triple1) -> rule2)) -> rule4))] @3: Dave is big.[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule1))]
Dave is young.
("Dave" "is" "young" "+")
triple1
Erin is not smart.
("Erin" "is" "smart" "-")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3