Erin is furry. Erin is nice. Erin is quiet. Erin is smart. Erin is young. Gary is nice. Gary is quiet. All big things are furry. All big things are cold. If Erin is quiet then Erin is cold. All furry things are smart. If Gary is furry and Gary is cold then Gary is smart. If Gary is nice then Gary is furry. If Erin is young and Erin is smart then Erin is furry. All smart things are nice.
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
All big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Erin is quiet then Erin is cold.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "cold" "+"))
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Gary is furry and Gary is cold then Gary is smart.
((("Gary" "is" "furry" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "smart" "+"))
If Gary is nice then Gary is furry.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "furry" "+"))
If Erin is young and Erin is smart then Erin is furry.
((("Erin" "is" "young" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "furry" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Gary is quiet.
True
1
proof
[(triple7)]
("Gary" "is" "quiet" "+")
triple7
Erin is not nice.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule8) OR ((((triple1) -> rule4)) -> rule8))]
("Erin" "is" "nice" "-")
triple2
((triple4) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Erin is furry.[(triple1 OR ((triple5 triple4) -> rule7))] Erin is nice.[(triple2 OR ((triple4) -> rule8) OR ((((triple1) -> rule4)) -> rule8))] Erin is quiet.[(triple3)] Erin is smart.[(triple4 OR ((triple1) -> rule4))] Erin is young.[(triple5)] Gary is nice.[(triple6)] Gary is quiet.[(triple7)] @1: Erin is cold.[(((triple3) -> rule3))] Gary is furry.[(((triple6) -> rule6))] @2: Gary is smart.[(((((triple6) -> rule6)) -> rule4))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
((triple5 triple4) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
((triple4) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
((triple1) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple6) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2