Dave is blue. Dave is furry. Dave is green. Dave is rough. Dave is round. Gary is blue. Gary is cold. Gary is furry. Gary is red. Gary is rough. Gary is round. Harry is cold. Harry is furry. Harry is red. Harry is round. If Gary is rough and Gary is blue then Gary is furry. Furry people are blue. Round people are furry. All green people are red. Rough, red people are cold. If someone is red then they are rough. If someone is round then they are red. All green, cold people are rough.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If Gary is rough and Gary is blue then Gary is furry.
((("Gary" "is" "rough" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "furry" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
All green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Rough, red people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is round then they are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All green, cold people are rough.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Gary is rough.
True
1
proof
[(triple10 OR ((triple9) -> rule6) OR ((((triple11) -> rule7)) -> rule6))]
("Gary" "is" "rough" "+")
triple10
((triple9) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not blue.
False
1
inv-proof
[(triple6 OR ((triple8) -> rule2) OR ((((triple11) -> rule3)) -> rule2))]
("Gary" "is" "blue" "-")
triple6
((triple8) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is blue.
True
2
proof
[(((triple13) -> rule2) OR ((((triple15) -> rule3)) -> rule2))]
("Harry" "is" "blue" "+")
((triple13) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Dave is not red.
False
2
inv-proof
[(((triple3) -> rule4) OR ((triple5) -> rule7))]
("Dave" "is" "red" "-")
((triple3) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple5) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
True
4
proof
[(((triple4 ((triple3) -> rule4)) -> rule5) OR ((triple4 ((triple5) -> rule7)) -> rule5) OR ((((((triple3) -> rule4)) -> rule6) ((triple3) -> rule4)) -> rule5) OR ((((((triple3) -> rule4)) -> rule6) ((triple5) -> rule7)) -> rule5) OR ((((((triple5) -> rule7)) -> rule6) ((triple3) -> rule4)) -> rule5) OR ((((((triple5) -> rule7)) -> rule6) ((triple5) -> rule7)) -> rule5))]
("Dave" "is" "cold" "+")
((triple4 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((triple4 ((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) ((triple3) -> (rule4 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) ((triple5) -> (rule7 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2)) ((triple3) -> (rule4 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2)) ((triple5) -> (rule7 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not cold.
False
4
inv-proof
[(((triple4 ((triple3) -> rule4)) -> rule5) OR ((triple4 ((triple5) -> rule7)) -> rule5) OR ((((((triple3) -> rule4)) -> rule6) ((triple3) -> rule4)) -> rule5) OR ((((((triple3) -> rule4)) -> rule6) ((triple5) -> rule7)) -> rule5) OR ((((((triple5) -> rule7)) -> rule6) ((triple3) -> rule4)) -> rule5) OR ((((((triple5) -> rule7)) -> rule6) ((triple5) -> rule7)) -> rule5))]
("Dave" "is" "cold" "-")
((triple4 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((triple4 ((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) ((triple3) -> (rule4 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) ((triple5) -> (rule7 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2)) ((triple3) -> (rule4 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2)) ((triple5) -> (rule7 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Dave is blue.[(triple1 OR ((triple2) -> rule2) OR ((((triple5) -> rule3)) -> rule2))] Dave is furry.[(triple2 OR ((triple5) -> rule3))] Dave is green.[(triple3)] Dave is rough.[(triple4 OR ((((triple3) -> rule4)) -> rule6) OR ((((triple5) -> rule7)) -> rule6))] Dave is round.[(triple5)] Gary is blue.[(triple6 OR ((triple8) -> rule2) OR ((((triple11) -> rule3)) -> rule2))] Gary is cold.[(triple7 OR ((triple10 triple9) -> rule5) OR ((triple10 ((triple11) -> rule7)) -> rule5) OR ((((triple9) -> rule6) triple9) -> rule5) OR ((((triple9) -> rule6) ((triple11) -> rule7)) -> rule5) OR ((((((triple11) -> rule7)) -> rule6) triple9) -> rule5) OR ((((((triple11) -> rule7)) -> rule6) ((triple11) -> rule7)) -> rule5))] Gary is furry.[(triple8 OR ((triple11) -> rule3) OR ((triple10 triple6) -> rule1) OR ((((triple9) -> rule6) triple6) -> rule1) OR ((((((triple11) -> rule7)) -> rule6) triple6) -> rule1))] Gary is red.[(triple9 OR ((triple11) -> rule7))] Gary is rough.[(triple10 OR ((triple9) -> rule6) OR ((((triple11) -> rule7)) -> rule6))] Gary is round.[(triple11)] Harry is cold.[(triple12 OR ((((triple14) -> rule6) triple14) -> rule5) OR ((((triple14) -> rule6) ((triple15) -> rule7)) -> rule5) OR ((((((triple15) -> rule7)) -> rule6) triple14) -> rule5) OR ((((((triple15) -> rule7)) -> rule6) ((triple15) -> rule7)) -> rule5))] Harry is furry.[(triple13 OR ((triple15) -> rule3))] Harry is red.[(triple14 OR ((triple15) -> rule7))] Harry is round.[(triple15)] @1: Dave is red.[(((triple3) -> rule4) OR ((triple5) -> rule7))] Harry is blue.[(((triple13) -> rule2) OR ((((triple15) -> rule3)) -> rule2))] Harry is rough.[(((triple14) -> rule6) OR ((((triple15) -> rule7)) -> rule6))] @2: Dave is cold.[(((triple4 ((triple3) -> rule4)) -> rule5) OR ((triple4 ((triple5) -> rule7)) -> rule5) OR ((((((triple3) -> rule4)) -> rule6) ((triple3) -> rule4)) -> rule5) OR ((((((triple3) -> rule4)) -> rule6) ((triple5) -> rule7)) -> rule5) OR ((((((triple5) -> rule7)) -> rule6) ((triple3) -> rule4)) -> rule5) OR ((((((triple5) -> rule7)) -> rule6) ((triple5) -> rule7)) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
((triple8) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple7
((triple10 triple9) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple10 ((triple11) -> (rule7 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple9) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple9) -> (rule6 % int3)) ((triple11) -> (rule7 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((triple11) -> (rule7 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple11) -> (rule7 % int3))) -> (rule6 % int2)) ((triple11) -> (rule7 % int3))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
triple8
((triple11) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple10 triple6) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple9) -> (rule6 % int2)) triple6) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple11) -> (rule7 % int3))) -> (rule6 % int2)) triple6) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple9
((triple11) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple10
((triple9) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
((((triple14) -> (rule6 % int2)) triple14) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple14) -> (rule6 % int3)) ((triple15) -> (rule7 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple15) -> (rule7 % int3))) -> (rule6 % int2)) triple14) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((((triple15) -> (rule7 % int3))) -> (rule6 % int2)) ((triple15) -> (rule7 % int3))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple13
((triple15) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple15) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple15
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple5) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple13) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple14) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple15) -> (rule7 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((triple4 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((triple4 ((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) ((triple3) -> (rule4 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) ((triple5) -> (rule7 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2)) ((triple3) -> (rule4 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2)) ((triple5) -> (rule7 % int3))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3