Anne is furry. Erin is blue. Gary is green. Gary is white. Harry is big. Harry is blue. Harry is cold. Harry is furry. Harry is green. Harry is white. All white people are blue. If Erin is furry and Erin is white then Erin is cold. All big, furry people are round. If Harry is blue and Harry is big then Harry is cold. Green, cold people are white. If someone is white then they are cold. If someone is big then they are furry. All round, white people are big.
Anne is furry.
("Anne" "is" "furry" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
All white people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If Erin is furry and Erin is white then Erin is cold.
((("Erin" "is" "furry" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "cold" "+"))
All big, furry people are round.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
If Harry is blue and Harry is big then Harry is cold.
((("Harry" "is" "blue" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "cold" "+"))
Green, cold people are white.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
All round, white people are big.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Harry is furry.
True
1
proof
[(triple8 OR ((triple5) -> rule7))]
("Harry" "is" "furry" "+")
triple8
((triple5) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not cold.
False
1
inv-proof
[(triple7 OR ((triple10) -> rule6) OR ((triple6 triple5) -> rule4) OR ((((triple10) -> rule1) triple5) -> rule4))]
("Harry" "is" "cold" "-")
triple7
((triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple6 triple5) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple10) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Gary is cold.
True
2
proof
[(((triple4) -> rule6))]
("Gary" "is" "cold" "+")
((triple4) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "blue" "-")
((triple4) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Erin is not furry.
Unknown
inv-rconc
[@3: Erin is furry.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule3 <- FAIL)]]
("Erin" "is" "furry" "-")
Gary is furry.
Unknown
rconc
[@3: Gary is furry.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule3 <- FAIL)]]
("Gary" "is" "furry" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is furry.[(triple1)] Erin is blue.[(triple2)] Gary is green.[(triple3)] Gary is white.[(triple4)] Harry is big.[(triple5)] Harry is blue.[(triple6 OR ((triple10) -> rule1) OR ((((triple9 triple7) -> rule5)) -> rule1))] Harry is cold.[(triple7 OR ((triple10) -> rule6) OR ((triple6 triple5) -> rule4) OR ((((triple10) -> rule1) triple5) -> rule4))] Harry is furry.[(triple8 OR ((triple5) -> rule7))] Harry is green.[(triple9)] Harry is white.[(triple10 OR ((triple9 triple7) -> rule5) OR ((triple9 ((triple6 triple5) -> rule4)) -> rule5))] @1: Gary is blue.[(((triple4) -> rule1))] Gary is cold.[(((triple4) -> rule6))] Harry is round.[(((triple5 triple8) -> rule3) OR ((triple5 ((triple5) -> rule7)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
((triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple9 triple7) -> (rule5 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple7
((triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple6 triple5) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple10) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple8
((triple5) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple9 triple7) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple9 ((triple6 triple5) -> (rule4 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple4) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple5 triple8) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple5 ((triple5) -> (rule7 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2