Charlie is big. Charlie is quiet. Charlie is red. Dave is big. Dave is kind. Dave is red. Dave is young. Erin is big. Erin is furry. Erin is quiet. Erin is rough. Erin is young. If something is red and young then it is quiet. Kind, quiet things are furry.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is red and young then it is quiet.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Kind, quiet things are furry.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple7)]
("Dave" "is" "young" "-")
triple7
Dave is quiet.
True
3
proof
[(((triple6 triple7) -> rule1))]
("Dave" "is" "quiet" "+")
((triple6 triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
3
inv-proof
[(((triple6 triple7) -> rule1))]
("Dave" "is" "quiet" "-")
((triple6 triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
True
5
proof
[(((triple5 ((triple6 triple7) -> rule1)) -> rule2))]
("Dave" "is" "furry" "+")
((triple5 ((triple6 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not furry.
False
5
inv-proof
[(((triple5 ((triple6 triple7) -> rule1)) -> rule2))]
("Dave" "is" "furry" "-")
((triple5 ((triple6 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "furry" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Charlie is big.[(triple1)] Charlie is quiet.[(triple2)] Charlie is red.[(triple3)] Dave is big.[(triple4)] Dave is kind.[(triple5)] Dave is red.[(triple6)] Dave is young.[(triple7)] Erin is big.[(triple8)] Erin is furry.[(triple9)] Erin is quiet.[(triple10)] Erin is rough.[(triple11)] Erin is young.[(triple12)] @1: Dave is quiet.[(((triple6 triple7) -> rule1))] @2: Dave is furry.[(((triple5 ((triple6 triple7) -> rule1)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is rough.
("Erin" "is" "rough" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6 triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple5 ((triple6 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2