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