Anne is cold. Anne is green. Anne is kind. Anne is round. Anne is smart. Anne is white. Charlie is cold. Charlie is green. Charlie is kind. Charlie is rough. Charlie is smart. Charlie is white. If Charlie is white then Charlie is rough. If Charlie is kind and Charlie is cold then Charlie is white. If Charlie is rough then Charlie is smart. If Anne is white and Anne is cold then Anne is round. If Anne is rough and Anne is cold then Anne is round. All green, white things are kind.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If Charlie is white then Charlie is rough.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "rough" "+"))
If Charlie is kind and Charlie is cold then Charlie is white.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "white" "+"))
If Charlie is rough then Charlie is smart.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "smart" "+"))
If Anne is white and Anne is cold then Anne is round.
((("Anne" "is" "white" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "round" "+"))
If Anne is rough and Anne is cold then Anne is round.
((("Anne" "is" "rough" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "round" "+"))
All green, white things are kind.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Charlie is cold.
True
1
proof
[(triple7)]
("Charlie" "is" "cold" "+")
triple7
Charlie is not kind.
False
1
inv-proof
[(triple9 OR ((triple8 triple12) -> rule6))]
("Charlie" "is" "kind" "-")
triple9
((triple8 triple12) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is kind.[(triple3 OR ((triple2 triple6) -> rule6))] Anne is round.[(triple4 OR ((triple6 triple1) -> rule4))] Anne is smart.[(triple5)] Anne is white.[(triple6)] Charlie is cold.[(triple7)] Charlie is green.[(triple8)] Charlie is kind.[(triple9 OR ((triple8 triple12) -> rule6))] Charlie is rough.[(triple10 OR ((triple12) -> rule1) OR ((((triple9 triple7) -> rule2)) -> rule1))] Charlie is smart.[(triple11 OR ((triple10) -> rule3) OR ((((triple12) -> rule1)) -> rule3) OR ((((((triple9 triple7) -> rule2)) -> rule1)) -> rule3))] Charlie is white.[(triple12 OR ((triple9 triple7) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple2 triple6) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple6 triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
((triple8 triple12) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple10
((triple12) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple9 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
((triple10) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((triple9 triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
triple12
((triple9 triple7) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1