Anne is big. Anne is furry. Anne is nice. Anne is quiet. Anne is rough. Anne is round. Charlie is big. Charlie is furry. Charlie is round. Dave is cold. Dave is furry. Dave is nice. If someone is big then they are furry. If Charlie is cold and Charlie is rough then Charlie is nice. All round, quiet people are cold. Nice people are cold. All round people are rough. Big people are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is cold and Charlie is rough then Charlie is nice.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "nice" "+"))
All round, quiet people are cold.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Anne is round.
True
1
proof
[(triple6)]
("Anne" "is" "round" "+")
triple6
Charlie is not round.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "round" "-")
triple9
Charlie is quiet.
True
2
proof
[(((triple7) -> rule6))]
("Charlie" "is" "quiet" "+")
((triple7) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple9) -> rule5))]
("Charlie" "is" "rough" "-")
((triple9) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
True
4
proof
[(((triple9 ((triple7) -> rule6)) -> rule3))]
("Charlie" "is" "cold" "+")
((triple9 ((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not cold.
False
4
inv-proof
[(((triple9 ((triple7) -> rule6)) -> rule3))]
("Charlie" "is" "cold" "-")
((triple9 ((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is nice.
True
7
proof
[(((((triple9 ((triple7) -> rule6)) -> rule3) ((triple9) -> rule5)) -> rule2))]
("Charlie" "is" "nice" "+")
((((triple9 ((triple7) -> (rule6 % int4))) -> (rule3 % int3)) ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is not nice.
False
7
inv-proof
[(((((triple9 ((triple7) -> rule6)) -> rule3) ((triple9) -> rule5)) -> rule2))]
("Charlie" "is" "nice" "-")
((((triple9 ((triple7) -> (rule6 % int4))) -> (rule3 % int3)) ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2 OR ((triple1) -> rule1))] Anne is nice.[(triple3)] Anne is quiet.[(triple4 OR ((triple1) -> rule6))] Anne is rough.[(triple5 OR ((triple6) -> rule5))] Anne is round.[(triple6)] Charlie is big.[(triple7)] Charlie is furry.[(triple8 OR ((triple7) -> rule1))] Charlie is round.[(triple9)] Dave is cold.[(triple10 OR ((triple12) -> rule4))] Dave is furry.[(triple11)] Dave is nice.[(triple12)] @1: Anne is cold.[(((triple3) -> rule4) OR ((triple6 triple4) -> rule3) OR ((triple6 ((triple1) -> rule6)) -> rule3))] Charlie is quiet.[(((triple7) -> rule6))] Charlie is rough.[(((triple9) -> rule5))] @2: Charlie is cold.[(((triple9 ((triple7) -> rule6)) -> rule3))] @3: Charlie is nice.[(((((triple9 ((triple7) -> rule6)) -> rule3) ((triple9) -> rule5)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple6) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
Charlie is big.
("Charlie" "is" "big" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
((triple7) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Dave is cold.
("Dave" "is" "cold" "+")
triple10
((triple12) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
Anne is cold.
("Anne" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple6 triple4) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple6 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple7) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple9) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple9 ((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple9 ((triple7) -> (rule6 % int4))) -> (rule3 % int3)) ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4