Charlie is smart. If something is smart and red then it is green. Blue, smart things are not green. If something is white and smart then it is not green. If Charlie is green then Charlie is not quiet. If Charlie is smart then Charlie is red. All smart things are not blue. If Charlie is not white then Charlie is blue. If something is green and not white then it is not furry.
Charlie is smart.
("Charlie" "is" "smart" "+")
If something is smart and red then it is green.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Blue, smart things are not green.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "-"))
If something is white and smart then it is not green.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "-"))
If Charlie is green then Charlie is not quiet.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "quiet" "-"))
If Charlie is smart then Charlie is red.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "red" "+"))
All smart things are not blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "-"))
If Charlie is not white then Charlie is blue.
((("Charlie" "is" "white" "~")) -> ("Charlie" "is" "blue" "+"))
If something is green and not white then it is not furry.
((("something" "is" "green" "+") ("something" "is" "white" "~")) -> ("something" "is" "furry" "-"))
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 red.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is blue.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is green.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule1))]
("Charlie" "is" "green" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule1))]
("Charlie" "is" "green" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not quiet.
True
5
proof
[(((((triple1 ((triple1) -> rule5)) -> rule1)) -> rule4))]
("Charlie" "is" "quiet" "-")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is quiet.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule5)) -> rule1)) -> rule4))]
("Charlie" "is" "quiet" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is smart.[(triple1)] @1: Charlie is not blue.[(((triple1) -> rule6))] Charlie is red.[(((triple1) -> rule5))] @2: Charlie is green.[(((triple1 ((triple1) -> rule5)) -> rule1))] @3: Charlie is not quiet.[(((((triple1 ((triple1) -> rule5)) -> rule1)) -> rule4))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Charlie is not blue.
("Charlie" "is" "blue" "-")
((triple1) -> (rule6 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3