Anne is blue. Anne is red. Dave is blue. Dave is rough. Dave is white. Fiona is nice. Fiona is rough. If Dave is nice and Dave is kind then Dave is blue. All young, blue things are kind. All kind things are rough. Nice things are young. If Dave is rough then Dave is kind. If something is kind then it is rough. If something is red then it is kind. All white, young things are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If Dave is nice and Dave is kind then Dave is blue.
((("Dave" "is" "nice" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "blue" "+"))
All young, blue things are kind.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Dave is rough then Dave is kind.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "kind" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All white, young things are nice.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Fiona is rough.
True
1
proof
[(triple7)]
("Fiona" "is" "rough" "+")
triple7
Dave is not blue.
False
1
inv-proof
[(triple3)]
("Dave" "is" "blue" "-")
triple3
Fiona is young.
True
2
proof
[(((triple6) -> rule4))]
("Fiona" "is" "young" "+")
((triple6) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple2) -> rule7))]
("Anne" "is" "kind" "-")
((triple2) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
True
3
proof
[(((((triple2) -> rule7)) -> rule3) OR ((((triple2) -> rule7)) -> rule6))]
("Anne" "is" "rough" "+")
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule3) OR ((((triple2) -> rule7)) -> rule6))]
("Anne" "is" "rough" "-")
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Anne" "is" "young" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Dave" "is" "young" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is red.[(triple2)] Dave is blue.[(triple3)] Dave is rough.[(triple4)] Dave is white.[(triple5)] Fiona is nice.[(triple6)] Fiona is rough.[(triple7)] @1: Anne is kind.[(((triple2) -> rule7))] Dave is kind.[(((triple4) -> rule5))] Fiona is young.[(((triple6) -> rule4))] @2: Anne is rough.[(((((triple2) -> rule7)) -> rule3) OR ((((triple2) -> rule7)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple6) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2