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