Anne is big. Anne is furry. Anne is young. Bob is young. Charlie is nice. Dave is furry. Dave is nice. Dave is quiet. Dave is rough. Dave is young. Young, nice people are rough. If someone is big then they are quiet. All young, quiet people are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Young, nice people are rough.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All young, quiet people are nice.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Anne is young.
True
1
proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Dave is not young.
False
1
inv-proof
[(triple10)]
("Dave" "is" "young" "-")
triple10
Anne is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
True
4
proof
[(((triple3 ((triple1) -> rule2)) -> rule3))]
("Anne" "is" "nice" "+")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((triple3 ((triple1) -> rule2)) -> rule3))]
("Anne" "is" "nice" "-")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is rough.
True
6
proof
[(((triple3 ((triple3 ((triple1) -> rule2)) -> rule3)) -> rule1))]
("Anne" "is" "rough" "+")
((triple3 ((triple3 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not rough.
False
6
inv-proof
[(((triple3 ((triple3 ((triple1) -> rule2)) -> rule3)) -> rule1))]
("Anne" "is" "rough" "-")
((triple3 ((triple3 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is young.[(triple3)] Bob is young.[(triple4)] Charlie is nice.[(triple5)] Dave is furry.[(triple6)] Dave is nice.[(triple7 OR ((triple10 triple8) -> rule3))] Dave is quiet.[(triple8)] Dave is rough.[(triple9 OR ((triple10 triple7) -> rule1) OR ((triple10 ((triple10 triple8) -> rule3)) -> rule1))] Dave is young.[(triple10)] @1: Anne is quiet.[(((triple1) -> rule2))] @2: Anne is nice.[(((triple3 ((triple1) -> rule2)) -> rule3))] @3: Anne is rough.[(((triple3 ((triple3 ((triple1) -> rule2)) -> rule3)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
((triple10 triple8) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
((triple10 triple7) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple10 ((triple10 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((triple3 ((triple3 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3