Anne is big. Anne is nice. Anne is quiet. Anne is young. Charlie is not furry. Charlie is green. Charlie is nice. Charlie is not quiet. Charlie is round. Charlie is not young. Dave is big. Dave is furry. Dave is green. Dave is not nice. Dave is young. All furry things are young. If something is quiet and green then it is young. All big things are green. If Dave is nice and Dave is not round then Dave is furry. Big, young things are furry. If something is big and not round then it is furry. If something is round and young then it is quiet. All young things are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is young.
("Dave" "is" "young" "+")
All furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is quiet and green then it is young.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Dave is nice and Dave is not round then Dave is furry.
((("Dave" "is" "nice" "+") ("Dave" "is" "round" "~")) -> ("Dave" "is" "furry" "+"))
Big, young things are furry.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is big and not round then it is furry.
((("something" "is" "big" "+") ("something" "is" "round" "~")) -> ("something" "is" "furry" "+"))
If something is round and young then it is quiet.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Dave is furry.
True
1
proof
[(triple12 OR ((triple11 triple15) -> rule5) OR ((((triple15) -> rule8) triple15) -> rule5))]
("Dave" "is" "furry" "+")
triple12
((triple11 triple15) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple15) -> (rule8 % int2)) triple15) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Charlie is quiet.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "quiet" "+")
triple8
Anne is furry.
True
3
proof
[(((triple1 triple4) -> rule5) OR ((((triple4) -> rule8) triple4) -> rule5) OR ((triple1 ((triple3 ((triple1) -> rule3)) -> rule2)) -> rule5) OR ((((triple4) -> rule8) ((triple3 ((triple1) -> rule3)) -> rule2)) -> rule5))]
("Anne" "is" "furry" "+")
((triple1 triple4) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple4) -> (rule8 % int2)) triple4) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple1 ((triple3 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple4) -> (rule8 % int4)) ((triple3 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is not furry.
False
3
inv-proof
[(((triple1 triple4) -> rule5) OR ((((triple4) -> rule8) triple4) -> rule5) OR ((triple1 ((triple3 ((triple1) -> rule3)) -> rule2)) -> rule5) OR ((((triple4) -> rule8) ((triple3 ((triple1) -> rule3)) -> rule2)) -> rule5))]
("Anne" "is" "furry" "-")
((triple1 triple4) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple4) -> (rule8 % int2)) triple4) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple1 ((triple3 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple4) -> (rule8 % int4)) ((triple3 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "big" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is big.[(triple1 OR ((triple4) -> rule8))] Anne is nice.[(triple2)] Anne is quiet.[(triple3)] Anne is young.[(triple4 OR ((triple3 ((triple1) -> rule3)) -> rule2))] Charlie is green.[(triple6)] Charlie is nice.[(triple7)] Charlie is not furry.[(triple5)] Charlie is not quiet.[(triple8)] Charlie is not young.[(triple10)] Charlie is round.[(triple9)] Dave is big.[(triple11 OR ((triple15) -> rule8) OR ((((triple12) -> rule1)) -> rule8))] Dave is furry.[(triple12 OR ((triple11 triple15) -> rule5) OR ((((triple15) -> rule8) triple15) -> rule5))] Dave is green.[(triple13 OR ((triple11) -> rule3) OR ((((triple15) -> rule8)) -> rule3) OR ((((((triple12) -> rule1)) -> rule8)) -> rule3))] Dave is not nice.[(triple14)] Dave is young.[(triple15 OR ((triple12) -> rule1))] @1: Anne is furry.[(((triple1 triple4) -> rule5) OR ((((triple4) -> rule8) triple4) -> rule5) OR ((triple1 ((triple3 ((triple1) -> rule3)) -> rule2)) -> rule5) OR ((((triple4) -> rule8) ((triple3 ((triple1) -> rule3)) -> rule2)) -> rule5))] Anne is green.[(((triple1) -> rule3) OR ((((triple4) -> rule8)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
((triple3 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple5
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple8
Charlie is not young.
("Charlie" "is" "young" "-")
triple10
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Dave is big.
("Dave" "is" "big" "+")
triple11
((triple15) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple12
((triple11 triple15) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple15) -> (rule8 % int2)) triple15) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple13
((triple11) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple12) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not nice.
("Dave" "is" "nice" "-")
triple14
Dave is young.
("Dave" "is" "young" "+")
triple15
((triple12) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 triple4) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple4) -> (rule8 % int2)) triple4) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple1 ((triple3 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple4) -> (rule8 % int4)) ((triple3 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2