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