Anne is blue. Anne is kind. Anne is rough. Anne is round. Charlie is blue. Charlie is not green. Charlie is round. Dave is kind. Erin is blue. Erin is rough. Erin is round. Erin is not smart. All rough things are not white. If something is rough and not white then it is green. If something is green and smart then it is round. If something is white and not kind then it is blue. If something is green and not kind then it is blue. Round, green things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
All rough things are not white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "-"))
If something is rough and not white then it is green.
((("something" "is" "rough" "+") ("something" "is" "white" "~")) -> ("something" "is" "green" "+"))
If something is green and smart then it is round.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is white and not kind then it is blue.
((("something" "is" "white" "+") ("something" "is" "kind" "~")) -> ("something" "is" "blue" "+"))
If something is green and not kind then it is blue.
((("something" "is" "green" "+") ("something" "is" "kind" "~")) -> ("something" "is" "blue" "+"))
Round, green things are blue.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Anne is kind.
True
1
proof
[(triple2)]
("Anne" "is" "kind" "+")
triple2
Anne is not rough.
False
1
inv-proof
[(triple3)]
("Anne" "is" "rough" "-")
triple3
Anne is not white.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "white" "-")
((triple3) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is white.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "white" "+")
((triple3) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "+")
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: Anne is blue.[(triple1 OR ((triple4 ((triple3 ((triple3) -> rule1)) -> rule2)) -> rule6))] Anne is kind.[(triple2)] Anne is rough.[(triple3)] Anne is round.[(triple4)] Charlie is blue.[(triple5)] Charlie is not green.[(triple6)] Charlie is round.[(triple7)] Dave is kind.[(triple8)] Erin is blue.[(triple9 OR ((triple11 ((triple10 ((triple10) -> rule1)) -> rule2)) -> rule6))] Erin is not smart.[(triple12)] Erin is rough.[(triple10)] Erin is round.[(triple11)] @1: Anne is not white.[(((triple3) -> rule1))] Erin is not white.[(((triple10) -> rule1))] @2: Anne is green.[(((triple3 ((triple3) -> rule1)) -> rule2))] Erin is green.[(((triple10 ((triple10) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple4 ((triple3 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not white.
("Anne" "is" "white" "-")
int3
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is not green.
("Charlie" "is" "green" "-")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Erin is blue.
("Erin" "is" "blue" "+")
triple9
((triple11 ((triple10 ((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not white.
("Erin" "is" "white" "-")
int3
Erin is not smart.
("Erin" "is" "smart" "-")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Anne is not white.
("Anne" "is" "white" "-")
((triple3) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Erin is not white.
("Erin" "is" "white" "-")
((triple10) -> (rule1 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple10 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not white.
("Erin" "is" "white" "-")
int2