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