Anne is big. Anne is cold. Anne is furry. Anne is nice. Anne is quiet. Anne is smart. Anne is young. Erin is big. Erin is quiet. Erin is smart. Erin is young. Gary is cold. Gary is furry. Gary is nice. Gary is smart. Gary is young. All furry, quiet things are smart. If something is furry and cold then it is young. All quiet, smart things are young. If Gary is smart and Gary is furry then Gary is cold. Quiet things are cold. If Erin is quiet and Erin is furry then Erin is nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
All furry, quiet things are smart.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is furry and cold then it is young.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All quiet, smart things are young.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Gary is smart and Gary is furry then Gary is cold.
((("Gary" "is" "smart" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "cold" "+"))
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Erin is quiet and Erin is furry then Erin is nice.
((("Erin" "is" "quiet" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "nice" "+"))
Anne is furry.
True
1
proof
[(triple3)]
("Anne" "is" "furry" "+")
triple3
Anne is not cold.
False
1
inv-proof
[(triple2 OR ((triple5) -> rule5))]
("Anne" "is" "cold" "-")
triple2
((triple5) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "nice" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((triple5) -> rule5))] Anne is furry.[(triple3)] Anne is nice.[(triple4)] Anne is quiet.[(triple5)] Anne is smart.[(triple6 OR ((triple3 triple5) -> rule1))] Anne is young.[(triple7 OR ((triple3 triple2) -> rule2) OR ((triple5 triple6) -> rule3) OR ((triple3 ((triple5) -> rule5)) -> rule2) OR ((triple5 ((triple3 triple5) -> rule1)) -> rule3))] Erin is big.[(triple8)] Erin is quiet.[(triple9)] Erin is smart.[(triple10)] Erin is young.[(triple11 OR ((triple9 triple10) -> rule3))] Gary is cold.[(triple12 OR ((triple15 triple13) -> rule4))] Gary is furry.[(triple13)] Gary is nice.[(triple14)] Gary is smart.[(triple15)] Gary is young.[(triple16 OR ((triple13 triple12) -> rule2) OR ((triple13 ((triple15 triple13) -> rule4)) -> rule2))] @1: Erin is cold.[(((triple9) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple5) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple3 triple5) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple3 triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple3 ((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((triple3 triple5) -> (rule1 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is young.
("Erin" "is" "young" "+")
triple11
((triple9 triple10) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple12
((triple15 triple13) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple13
Gary is nice.
("Gary" "is" "nice" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
((triple13 triple12) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple13 ((triple15 triple13) -> (rule4 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple9) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1