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