Charlie is big. Charlie is furry. Charlie is not green. Charlie is kind. Charlie is rough. Charlie is smart. Erin is furry. Erin is green. Erin is kind. Erin is not quiet. Erin is rough. Erin is smart. Harry is big. Harry is green. Harry is rough. Harry is smart. Quiet, rough things are kind. If Erin is rough then Erin is furry. If Charlie is rough and Charlie is not kind then Charlie is furry. If something is smart and not rough then it is big. Smart things are furry. If something is big then it is furry. All smart, green things are furry. Furry things are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Quiet, rough things are kind.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If Erin is rough then Erin is furry.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "furry" "+"))
If Charlie is rough and Charlie is not kind then Charlie is furry.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "furry" "+"))
If something is smart and not rough then it is big.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "big" "+"))
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
All smart, green things are furry.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Charlie is rough.
True
1
proof
[(triple5)]
("Charlie" "is" "rough" "+")
triple5
Erin is not rough.
False
1
inv-proof
[(triple11)]
("Erin" "is" "rough" "-")
triple11
Harry is furry.
True
2
proof
[(((triple13) -> rule6) OR ((triple16) -> rule5) OR ((triple16 triple14) -> rule7))]
("Harry" "is" "furry" "+")
((triple13) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple16) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple16 triple14) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple13) -> rule6) OR ((triple16) -> rule5) OR ((triple16 triple14) -> rule7))]
("Harry" "is" "furry" "-")
((triple13) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple16) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple16 triple14) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "big" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2 OR ((triple1) -> rule6) OR ((triple6) -> rule5))] Charlie is kind.[(triple4)] Charlie is not green.[(triple3)] Charlie is rough.[(triple5)] Charlie is smart.[(triple6 OR ((triple2) -> rule8) OR ((((triple1) -> rule6)) -> rule8))] Erin is furry.[(triple7 OR ((triple11) -> rule2) OR ((triple12) -> rule5) OR ((triple12 triple8) -> rule7))] Erin is green.[(triple8)] Erin is kind.[(triple9)] Erin is not quiet.[(triple10)] Erin is rough.[(triple11)] Erin is smart.[(triple12 OR ((triple7) -> rule8) OR ((((triple11) -> rule2)) -> rule8))] Harry is big.[(triple13)] Harry is green.[(triple14)] Harry is rough.[(triple15)] Harry is smart.[(triple16 OR ((((triple13) -> rule6)) -> rule8))] @1: Harry is furry.[(((triple13) -> rule6) OR ((triple16) -> rule5) OR ((triple16 triple14) -> rule7))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple6) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is not green.
("Charlie" "is" "green" "-")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple2) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple7
((triple11) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple12) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple12 triple8) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple10
Erin is rough.
("Erin" "is" "rough" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
((triple7) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
((((triple13) -> (rule6 % int2))) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple13) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple16) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple16 triple14) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1