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