Charlie is big. Charlie is blue. Charlie is kind. Charlie is quiet. Charlie is smart. Harry is big. Harry is furry. Harry is kind. Harry is quiet. Harry is smart. If someone is kind then they are quiet. If someone is smart then they are quiet. All quiet, furry people are smart. Big people are quiet. If Harry is smart then Harry is kind. All quiet people are blue.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All quiet, furry people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is smart then Harry is kind.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "kind" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Charlie is not kind.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "kind" "-")
triple3
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2 OR ((triple4) -> rule6) OR ((((triple1) -> rule4)) -> rule6) OR ((((triple3) -> rule1)) -> rule6) OR ((((triple5) -> rule2)) -> rule6))] Charlie is kind.[(triple3)] Charlie is quiet.[(triple4 OR ((triple1) -> rule4) OR ((triple3) -> rule1) OR ((triple5) -> rule2))] Charlie is smart.[(triple5)] Harry is big.[(triple6)] Harry is furry.[(triple7)] Harry is kind.[(triple8 OR ((triple10) -> rule5) OR ((((triple9 triple7) -> rule3)) -> rule5) OR ((((((triple6) -> rule4) triple7) -> rule3)) -> rule5))] Harry is quiet.[(triple9 OR ((triple10) -> rule2) OR ((triple6) -> rule4) OR ((triple8) -> rule1) OR ((((triple10) -> rule5)) -> rule1))] Harry is smart.[(triple10 OR ((triple9 triple7) -> rule3) OR ((((triple6) -> rule4) triple7) -> rule3) OR ((((triple8) -> rule1) triple7) -> rule3))] @1: Harry is blue.[(((triple9) -> rule6) OR ((((triple10) -> rule2)) -> rule6) OR ((((triple6) -> rule4)) -> rule6) OR ((((triple8) -> rule1)) -> rule6) OR ((((((triple10) -> rule5)) -> rule1)) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple4) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple3) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple5) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple10) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple9 triple7) -> (rule3 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple6) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
((triple10) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple6) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple8) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple10
((triple9 triple7) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple6) -> (rule4 % int2)) triple7) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple9) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3