Charlie is blue. Charlie is furry. Charlie is red. If Charlie is smart and Charlie is not furry then Charlie is not red. If Charlie is blue then Charlie is red. If something is furry and big then it is kind. Red things are kind. Big things are red. Smart things are red. If something is blue and furry then it is big. If something is kind and rough then it is not big.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
If Charlie is smart and Charlie is not furry then Charlie is not red.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "furry" "~")) -> ("Charlie" "is" "red" "-"))
If Charlie is blue then Charlie is red.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "red" "+"))
If something is furry and big then it is kind.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is blue and furry then it is big.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is kind and rough then it is not big.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "-"))
Charlie is red.
True
1
proof
[(triple3 OR ((triple1) -> rule2) OR ((((triple1 triple2) -> rule7)) -> rule5))]
("Charlie" "is" "red" "+")
triple3
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple1 triple2) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple3) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((triple2 ((triple1 triple2) -> rule7)) -> rule3) OR ((((((triple1 triple2) -> rule7)) -> rule5)) -> rule4))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((triple2 ((triple1 triple2) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((triple1 triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not big.
False
3
inv-proof
[(((triple1 triple2) -> rule7))]
("Charlie" "is" "big" "-")
((triple1 triple2) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2)] Charlie is red.[(triple3 OR ((triple1) -> rule2) OR ((((triple1 triple2) -> rule7)) -> rule5))] @1: Charlie is big.[(((triple1 triple2) -> rule7))] Charlie is kind.[(((triple3) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((triple2 ((triple1 triple2) -> rule7)) -> rule3) OR ((((((triple1 triple2) -> rule7)) -> rule5)) -> rule4))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple1 triple2) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple1 triple2) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((triple2 ((triple1 triple2) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((triple1 triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3