Charlie is furry. Charlie is kind. Charlie is round. Charlie is smart. Erin is red. Harry is big. Harry is kind. Harry is rough. Harry is round. Harry is smart. All round, rough things are big. If something is rough and not kind then it is not big. Rough things are round. If something is red and rough then it is round. If something is rough and kind then it is red. If Erin is big and Erin is not kind then Erin is red. Big, furry things are not smart. If something is round and not red then it is not smart.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All round, rough things are big.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is rough and not kind then it is not big.
((("something" "is" "rough" "+") ("something" "is" "kind" "~")) -> ("something" "is" "big" "-"))
Rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is red and rough then it is round.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is rough and kind then it is red.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Erin is big and Erin is not kind then Erin is red.
((("Erin" "is" "big" "+") ("Erin" "is" "kind" "~")) -> ("Erin" "is" "red" "+"))
Big, furry things are not smart.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "-"))
If something is round and not red then it is not smart.
((("something" "is" "round" "+") ("something" "is" "red" "~")) -> ("something" "is" "smart" "-"))
Erin is red.
True
1
proof
[(triple5)]
("Erin" "is" "red" "+")
triple5
Charlie is not smart.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "smart" "-")
triple4
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Charlie is furry.[(triple1)] Charlie is kind.[(triple2)] Charlie is round.[(triple3)] Charlie is smart.[(triple4)] Erin is red.[(triple5)] Harry is big.[(triple6 OR ((triple9 triple8) -> rule1) OR ((((triple8) -> rule3) triple8) -> rule1) OR ((((((triple8 triple7) -> rule5) triple8) -> rule4) triple8) -> rule1))] Harry is kind.[(triple7)] Harry is rough.[(triple8)] Harry is round.[(triple9 OR ((triple8) -> rule3) OR ((((triple8 triple7) -> rule5) triple8) -> rule4))] Harry is smart.[(triple10)] @1: Harry is red.[(((triple8 triple7) -> rule5))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
((triple9 triple8) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple8) -> (rule3 % int2)) triple8) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((((triple8 triple7) -> (rule5 % int3)) triple8) -> (rule4 % int2)) triple8) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
((triple8) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple8 triple7) -> (rule5 % int2)) triple8) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
((triple8 triple7) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1