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