Dave is furry. Dave is round. Gary is big. Gary is kind. Gary is red. Gary is round. Gary is smart. All big, kind things are rough. All big, rough things are round. If something is round then it is big.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All big, kind things are rough.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All big, rough things are round.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Gary is round.
True
1
proof
[(triple6 OR ((triple3 ((triple3 triple4) -> rule1)) -> rule2))]
("Gary" "is" "round" "+")
triple6
((triple3 ((triple3 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not red.
False
1
inv-proof
[(triple5)]
("Gary" "is" "red" "-")
triple5
Dave is big.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "big" "+")
((triple2) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Gary is not rough.
False
3
inv-proof
[(((triple3 triple4) -> rule1) OR ((((triple6) -> rule3) triple4) -> rule1))]
("Gary" "is" "rough" "-")
((triple3 triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple6) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is furry.[(triple1)] Dave is round.[(triple2)] Gary is big.[(triple3 OR ((triple6) -> rule3))] Gary is kind.[(triple4)] Gary is red.[(triple5)] Gary is round.[(triple6 OR ((triple3 ((triple3 triple4) -> rule1)) -> rule2))] Gary is smart.[(triple7)] @1: Dave is big.[(((triple2) -> rule3))] Gary is rough.[(((triple3 triple4) -> rule1) OR ((((triple6) -> rule3) triple4) -> rule1))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
((triple6) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple3 ((triple3 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3 triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple6) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2