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