Dave is blue. Dave is cold. Dave is furry. Dave is green. Dave is red. Dave is smart. Gary is not blue. Gary is cold. Gary is furry. Gary is green. Gary is red. Gary is smart. Gary is not young. Harry is cold. Harry is red. Harry is young. Red, cold people are furry. If someone is blue and not young then they are not red. If Gary is furry then Gary is smart. If someone is green and not red then they are smart. Furry, young people are not smart. If someone is red and not cold then they are not smart.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is not young.
("Gary" "is" "young" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Red, cold people are furry.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is blue and not young then they are not red.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "red" "-"))
If Gary is furry then Gary is smart.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "smart" "+"))
If someone is green and not red then they are smart.
((("someone" "is" "green" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "smart" "+"))
Furry, young people are not smart.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "-"))
If someone is red and not cold then they are not smart.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "smart" "-"))
Gary is furry.
True
1
proof
[(triple9 OR ((triple11 triple8) -> rule1))]
("Gary" "is" "furry" "+")
triple9
((triple11 triple8) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not green.
False
1
inv-proof
[(triple10)]
("Gary" "is" "green" "-")
triple10
Harry is furry.
True
3
proof
[(((triple15 triple14) -> rule1))]
("Harry" "is" "furry" "+")
((triple15 triple14) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
3
inv-proof
[(((triple15 triple14) -> rule1))]
("Harry" "is" "furry" "-")
((triple15 triple14) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not smart.
True
5
proof
[(((((triple15 triple14) -> rule1) triple16) -> rule5))]
("Harry" "is" "smart" "-")
((((triple15 triple14) -> (rule1 % int2)) triple16) -> (rule5 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
False
5
inv-proof
[(((((triple15 triple14) -> rule1) triple16) -> rule5))]
("Harry" "is" "smart" "+")
((((triple15 triple14) -> (rule1 % int2)) triple16) -> (rule5 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2)] Dave is furry.[(triple3 OR ((triple5 triple2) -> rule1))] Dave is green.[(triple4)] Dave is red.[(triple5)] Dave is smart.[(triple6)] Gary is cold.[(triple8)] Gary is furry.[(triple9 OR ((triple11 triple8) -> rule1))] Gary is green.[(triple10)] Gary is not blue.[(triple7)] Gary is not young.[(triple13)] Gary is red.[(triple11)] Gary is smart.[(triple12 OR ((triple9) -> rule3) OR ((((triple11 triple8) -> rule1)) -> rule3))] Harry is cold.[(triple14)] Harry is red.[(triple15)] Harry is young.[(triple16)] @1: Harry is furry.[(((triple15 triple14) -> rule1))] @2: Harry is not smart.[(((((triple15 triple14) -> rule1) triple16) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple5 triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
((triple11 triple8) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is not blue.
("Gary" "is" "blue" "-")
triple7
Gary is not young.
("Gary" "is" "young" "-")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((triple9) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple11 triple8) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple14
Harry is red.
("Harry" "is" "red" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Harry is furry.
("Harry" "is" "furry" "+")
((triple15 triple14) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
((((triple15 triple14) -> (rule1 % int2)) triple16) -> (rule5 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2