Anne is furry. Anne is green. Anne is kind. Anne is nice. Anne is quiet. Anne is round. Dave is green. Dave is kind. Dave is quiet. Dave is rough. Dave is round. Gary is furry. Gary is kind. Gary is nice. Gary is quiet. Gary is rough. If something is green and rough then it is round. If something is quiet then it is green. Quiet, round things are rough. All nice, green things are rough. All kind, furry things are quiet. All nice things are rough.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If something is green and rough then it is round.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Quiet, round things are rough.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All nice, green things are rough.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All kind, furry things are quiet.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Gary is kind.
True
1
proof
[(triple13)]
("Gary" "is" "kind" "+")
triple13
Gary is not nice.
False
1
inv-proof
[(triple14)]
("Gary" "is" "nice" "-")
triple14
Anne is rough.
True
2
proof
[(((triple4) -> rule6) OR ((triple4 triple2) -> rule4) OR ((triple5 triple6) -> rule3) OR ((triple4 ((triple5) -> rule2)) -> rule4) OR ((((triple3 triple1) -> rule5) triple6) -> rule3) OR ((triple4 ((((triple3 triple1) -> rule5)) -> rule2)) -> rule4))]
("Anne" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple3 triple1) -> (rule5 % int2)) triple6) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((triple4 ((((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not rough.
False
2
inv-proof
[(((triple4) -> rule6) OR ((triple4 triple2) -> rule4) OR ((triple5 triple6) -> rule3) OR ((triple4 ((triple5) -> rule2)) -> rule4) OR ((((triple3 triple1) -> rule5) triple6) -> rule3) OR ((triple4 ((((triple3 triple1) -> rule5)) -> rule2)) -> rule4))]
("Anne" "is" "rough" "-")
((triple4) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple3 triple1) -> (rule5 % int2)) triple6) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((triple4 ((((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2 OR ((triple5) -> rule2) OR ((((triple3 triple1) -> rule5)) -> rule2))] Anne is kind.[(triple3)] Anne is nice.[(triple4)] Anne is quiet.[(triple5 OR ((triple3 triple1) -> rule5))] Anne is round.[(triple6 OR ((triple2 ((triple4) -> rule6)) -> rule1) OR ((triple2 ((triple4 triple2) -> rule4)) -> rule1) OR ((((triple5) -> rule2) ((triple4) -> rule6)) -> rule1) OR ((((triple5) -> rule2) ((triple4 triple2) -> rule4)) -> rule1) OR ((triple2 ((triple4 ((triple5) -> rule2)) -> rule4)) -> rule1) OR ((((triple5) -> rule2) ((triple4 ((triple5) -> rule2)) -> rule4)) -> rule1) OR ((((((triple3 triple1) -> rule5)) -> rule2) ((triple4) -> rule6)) -> rule1) OR ((((((triple3 triple1) -> rule5)) -> rule2) ((triple4 triple2) -> rule4)) -> rule1) OR ((((((triple3 triple1) -> rule5)) -> rule2) ((triple4 ((triple5) -> rule2)) -> rule4)) -> rule1) OR ((triple2 ((triple4 ((((triple3 triple1) -> rule5)) -> rule2)) -> rule4)) -> rule1) OR ((((triple5) -> rule2) ((triple4 ((((triple3 triple1) -> rule5)) -> rule2)) -> rule4)) -> rule1) OR ((((((triple3 triple1) -> rule5)) -> rule2) ((triple4 ((((triple3 triple1) -> rule5)) -> rule2)) -> rule4)) -> rule1))] Dave is green.[(triple7 OR ((triple9) -> rule2))] Dave is kind.[(triple8)] Dave is quiet.[(triple9)] Dave is rough.[(triple10 OR ((triple9 triple11) -> rule3))] Dave is round.[(triple11 OR ((triple7 triple10) -> rule1) OR ((((triple9) -> rule2) triple10) -> rule1))] Gary is furry.[(triple12)] Gary is kind.[(triple13)] Gary is nice.[(triple14)] Gary is quiet.[(triple15 OR ((triple13 triple12) -> rule5))] Gary is rough.[(triple16 OR ((triple14) -> rule6) OR ((triple14 ((triple15) -> rule2)) -> rule4) OR ((triple14 ((((triple13 triple12) -> rule5)) -> rule2)) -> rule4))] @1: Anne is rough.[(((triple4) -> rule6) OR ((triple4 triple2) -> rule4) OR ((triple5 triple6) -> rule3) OR ((triple4 ((triple5) -> rule2)) -> rule4) OR ((((triple3 triple1) -> rule5) triple6) -> rule3) OR ((triple4 ((((triple3 triple1) -> rule5)) -> rule2)) -> rule4))] Gary is green.[(((triple15) -> rule2) OR ((((triple13 triple12) -> rule5)) -> rule2))] @2: Gary is round.[(((((triple15) -> rule2) triple16) -> rule1) OR ((((triple15) -> rule2) ((triple14) -> rule6)) -> rule1) OR ((((((triple13 triple12) -> rule5)) -> rule2) triple16) -> rule1) OR ((((triple15) -> rule2) ((triple14 ((triple15) -> rule2)) -> rule4)) -> rule1) OR ((((((triple13 triple12) -> rule5)) -> rule2) ((triple14) -> rule6)) -> rule1) OR ((((((triple13 triple12) -> rule5)) -> rule2) ((triple14 ((triple15) -> rule2)) -> rule4)) -> rule1) OR ((((triple15) -> rule2) ((triple14 ((((triple13 triple12) -> rule5)) -> rule2)) -> rule4)) -> rule1) OR ((((((triple13 triple12) -> rule5)) -> rule2) ((triple14 ((((triple13 triple12) -> rule5)) -> rule2)) -> rule4)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple5) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple3 triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
((triple3 triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple2 ((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((triple2 ((triple4 triple2) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple5) -> (rule2 % int3)) ((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple5) -> (rule2 % int3)) ((triple4 triple2) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((triple2 ((triple4 ((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple5) -> (rule2 % int3)) ((triple4 ((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((((triple3 triple1) -> (rule5 % int4))) -> (rule2 % int3)) ((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((((((triple3 triple1) -> (rule5 % int4))) -> (rule2 % int3)) ((triple4 triple2) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((((((triple3 triple1) -> (rule5 % int4))) -> (rule2 % int3)) ((triple4 ((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((triple2 ((triple4 ((((triple3 triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((((triple5) -> (rule2 % int4)) ((triple4 ((((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((triple3 triple1) -> (rule5 % int4))) -> (rule2 % int3)) ((triple4 ((((triple3 triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple9) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
((triple9 triple11) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple11
((triple7 triple10) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple9) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple12
Gary is kind.
("Gary" "is" "kind" "+")
triple13
Gary is nice.
("Gary" "is" "nice" "+")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple15
((triple13 triple12) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple16
((triple14) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple14 ((triple15) -> (rule2 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((triple14 ((((triple13 triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple3 triple1) -> (rule5 % int2)) triple6) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((triple4 ((((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((triple15) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple13 triple12) -> (rule5 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple15) -> (rule2 % int2)) triple16) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple15) -> (rule2 % int3)) ((triple14) -> (rule6 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple13 triple12) -> (rule5 % int3))) -> (rule2 % int2)) triple16) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple15) -> (rule2 % int3)) ((triple14 ((triple15) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple13 triple12) -> (rule5 % int4))) -> (rule2 % int3)) ((triple14) -> (rule6 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((((triple13 triple12) -> (rule5 % int4))) -> (rule2 % int3)) ((triple14 ((triple15) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((triple15) -> (rule2 % int4)) ((triple14 ((((triple13 triple12) -> (rule5 % int3))) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
((((((triple13 triple12) -> (rule5 % int4))) -> (rule2 % int3)) ((triple14 ((((triple13 triple12) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4