Dave is big. Dave is blue. Dave is cold. Dave is furry. Dave is kind. Dave is round. Gary is big. Gary is blue. Gary is furry. Gary is round. Harry is big. Harry is blue. Harry is cold. Harry is furry. Harry is kind. Harry is young. Round things are cold. If something is cold then it is kind.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Dave is furry.
True
1
proof
[(triple4)]
("Dave" "is" "furry" "+")
triple4
Gary is not big.
False
1
inv-proof
[(triple7)]
("Gary" "is" "big" "-")
triple7
Gary is cold.
True
2
proof
[(((triple10) -> rule1))]
("Gary" "is" "cold" "+")
((triple10) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple10) -> rule1))]
("Gary" "is" "cold" "-")
((triple10) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
True
3
proof
[(((((triple10) -> rule1)) -> rule2))]
("Gary" "is" "kind" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule2))]
("Gary" "is" "kind" "-")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is cold.[(triple3 OR ((triple6) -> rule1))] Dave is furry.[(triple4)] Dave is kind.[(triple5 OR ((triple3) -> rule2) OR ((((triple6) -> rule1)) -> rule2))] Dave is round.[(triple6)] Gary is big.[(triple7)] Gary is blue.[(triple8)] Gary is furry.[(triple9)] Gary is round.[(triple10)] Harry is big.[(triple11)] Harry is blue.[(triple12)] Harry is cold.[(triple13)] Harry is furry.[(triple14)] Harry is kind.[(triple15 OR ((triple13) -> rule2))] Harry is young.[(triple16)] @1: Gary is cold.[(((triple10) -> rule1))] @2: Gary is kind.[(((((triple10) -> rule1)) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple6) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
((triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is kind.
("Harry" "is" "kind" "+")
triple15
((triple13) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple16
Gary is cold.
("Gary" "is" "cold" "+")
((triple10) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2