Dave is big. Dave is green. Dave is nice. Dave is white. Gary is big. Gary is furry. Gary is green. Gary is kind. Gary is nice. Gary is white. Furry, green things are big. If something is green then it is big. If Dave is not kind then Dave is green. If something is kind then it is nice. If something is nice and kind then it is white. Nice things are not rough. Kind, big things are not rough. If Gary is not kind and Gary is not big then Gary is nice.
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
Furry, green things are big.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If Dave is not kind then Dave is green.
((("Dave" "is" "kind" "~")) -> ("Dave" "is" "green" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is nice and kind then it is white.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Nice things are not rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "-"))
Kind, big things are not rough.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
If Gary is not kind and Gary is not big then Gary is nice.
((("Gary" "is" "kind" "~") ("Gary" "is" "big" "~")) -> ("Gary" "is" "nice" "+"))
Gary is furry.
True
1
proof
[(triple6)]
("Gary" "is" "furry" "+")
triple6
Gary is not nice.
False
1
inv-proof
[(triple9 OR ((triple8) -> rule4))]
("Gary" "is" "nice" "-")
triple9
((triple8) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not rough.
True
2
proof
[(((triple9) -> rule6) OR ((triple8 triple5) -> rule7) OR ((((triple8) -> rule4)) -> rule6) OR ((triple8 ((triple7) -> rule2)) -> rule7) OR ((triple8 ((triple6 triple7) -> rule1)) -> rule7))]
("Gary" "is" "rough" "-")
((triple9) -> (rule6 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((triple8 triple5) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple8 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple8 ((triple6 triple7) -> (rule1 % int2))) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
False
2
inv-proof
[(((triple9) -> rule6) OR ((triple8 triple5) -> rule7) OR ((((triple8) -> rule4)) -> rule6) OR ((triple8 ((triple7) -> rule2)) -> rule7) OR ((triple8 ((triple6 triple7) -> rule1)) -> rule7))]
("Gary" "is" "rough" "+")
((triple9) -> (rule6 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((triple8 triple5) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple8 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple8 ((triple6 triple7) -> (rule1 % int2))) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is big.[(triple1 OR ((triple2) -> rule2))] Dave is green.[(triple2)] Dave is nice.[(triple3)] Dave is white.[(triple4)] Gary is big.[(triple5 OR ((triple7) -> rule2) OR ((triple6 triple7) -> rule1))] Gary is furry.[(triple6)] Gary is green.[(triple7)] Gary is kind.[(triple8)] Gary is nice.[(triple9 OR ((triple8) -> rule4))] Gary is white.[(triple10 OR ((triple9 triple8) -> rule5) OR ((((triple8) -> rule4) triple8) -> rule5))] @1: Dave is not rough.[(((triple3) -> rule6))] Gary is not rough.[(((triple9) -> rule6) OR ((triple8 triple5) -> rule7) OR ((((triple8) -> rule4)) -> rule6) OR ((triple8 ((triple7) -> rule2)) -> rule7) OR ((triple8 ((triple6 triple7) -> rule1)) -> rule7))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
((triple7) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple6 triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
((triple8) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple10
((triple9 triple8) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple8) -> (rule4 % int2)) triple8) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Dave is not rough.
("Dave" "is" "rough" "-")
((triple3) -> (rule6 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
((triple9) -> (rule6 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((triple8 triple5) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple8 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple8 ((triple6 triple7) -> (rule1 % int2))) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2