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