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