Anne is big. Anne is cold. Anne is nice. Anne is smart. Erin is big. Erin is cold. Erin is furry. Erin is kind. Erin is round. Gary is cold. Gary is round. Gary is smart. All big, smart things are kind. All kind, smart things are big. Nice, big things are furry. If Erin is smart then Erin is round. All big, cold things are round. If something is nice then it is smart. All round, furry things are smart. Nice, cold things are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All big, smart things are kind.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All kind, smart things are big.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Nice, big things are furry.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If Erin is smart then Erin is round.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "round" "+"))
All big, cold things are round.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All round, furry things are smart.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Nice, cold things are smart.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Erin is kind.
True
1
proof
[(triple8 OR ((triple5 ((triple9 triple7) -> rule7)) -> rule1) OR ((triple5 ((((triple5 triple6) -> rule5) triple7) -> rule7)) -> rule1))]
("Erin" "is" "kind" "+")
triple8
((triple5 ((triple9 triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((triple5 ((((triple5 triple6) -> (rule5 % int3)) triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not round.
False
1
inv-proof
[(triple9 OR ((triple5 triple6) -> rule5))]
("Erin" "is" "round" "-")
triple9
((triple5 triple6) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is nice.[(triple3)] Anne is smart.[(triple4 OR ((triple3) -> rule6) OR ((triple3 triple2) -> rule8) OR ((((triple1 triple2) -> rule5) ((triple3 triple1) -> rule3)) -> rule7))] Erin is big.[(triple5 OR ((triple8 ((triple9 triple7) -> rule7)) -> rule2))] Erin is cold.[(triple6)] Erin is furry.[(triple7)] Erin is kind.[(triple8 OR ((triple5 ((triple9 triple7) -> rule7)) -> rule1) OR ((triple5 ((((triple5 triple6) -> rule5) triple7) -> rule7)) -> rule1))] Erin is round.[(triple9 OR ((triple5 triple6) -> rule5))] Gary is cold.[(triple10)] Gary is round.[(triple11)] Gary is smart.[(triple12)] @1: Anne is furry.[(((triple3 triple1) -> rule3))] Anne is kind.[(((triple1 triple4) -> rule1) OR ((triple1 ((triple3) -> rule6)) -> rule1) OR ((triple1 ((triple3 triple2) -> rule8)) -> rule1) OR ((triple1 ((((triple1 triple2) -> rule5) ((triple3 triple1) -> rule3)) -> rule7)) -> rule1))] Anne is round.[(((triple1 triple2) -> rule5))] Erin is smart.[(((triple9 triple7) -> rule7) OR ((((triple5 triple6) -> rule5) triple7) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple3) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple3 triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple1 triple2) -> (rule5 % int3)) ((triple3 triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
triple5
((triple8 ((triple9 triple7) -> (rule7 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((triple5 ((triple9 triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((triple5 ((((triple5 triple6) -> (rule5 % int3)) triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple9
((triple5 triple6) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Anne is furry.
("Anne" "is" "furry" "+")
((triple3 triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 triple4) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((triple1 ((triple3 triple2) -> (rule8 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((triple1 ((((triple1 triple2) -> (rule5 % int4)) ((triple3 triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
((triple1 triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple9 triple7) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple5 triple6) -> (rule5 % int2)) triple7) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2