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