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