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