Charlie is smart. If something is red then it is quiet. All red things are nice. Smart things are nice. White, cold things are red. If something is smart then it is red. All cold, smart things are red. Quiet, green things are red. All nice things are cold.
Charlie is smart.
("Charlie" "is" "smart" "+")
If something is red then it is quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
White, cold things are red.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
All cold, smart things are red.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Quiet, green things are red.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Charlie is smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Charlie is not smart.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "smart" "-")
triple1
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is smart.[(triple1)] @1: Charlie is nice.[(((triple1) -> rule3) OR ((((triple1) -> rule5)) -> rule2))] Charlie is red.[(((triple1) -> rule5) OR ((((((triple1) -> rule3)) -> rule8) triple1) -> rule6))] @2: Charlie is cold.[(((((triple1) -> rule3)) -> rule8) OR ((((((triple1) -> rule5)) -> rule2)) -> rule8))] Charlie is quiet.[(((((triple1) -> rule5)) -> rule1) OR ((((((((triple1) -> rule3)) -> rule8) triple1) -> rule6)) -> rule1))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4