Anne is not nice. Anne is not rough. Anne is not smart. Dave is green. Dave is kind. Dave is red. Dave is not smart. Dave is white. Fiona is green. Fiona is kind. Fiona is rough. Fiona is smart. Gary is kind. Gary is nice. Gary is smart. If Fiona is not green and Fiona is not smart then Fiona is not white. If someone is rough and not kind then they are nice. If someone is red then they are nice. Green people are rough. All kind people are red. If someone is nice and white then they are red. If someone is nice then they are white. If someone is nice and green then they are white.
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is not smart.
("Anne" "is" "smart" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Dave is white.
("Dave" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Fiona is not green and Fiona is not smart then Fiona is not white.
((("Fiona" "is" "green" "~") ("Fiona" "is" "smart" "~")) -> ("Fiona" "is" "white" "-"))
If someone is rough and not kind then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "nice" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is nice and white then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is nice and green then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Fiona is rough.
True
1
proof
[(triple11 OR ((triple9) -> rule4))]
("Fiona" "is" "rough" "+")
triple11
((triple9) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Gary is not nice.
False
1
inv-proof
[(triple14 OR ((((triple13) -> rule5)) -> rule3))]
("Gary" "is" "nice" "-")
triple14
((((triple13) -> (rule5 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Dave is nice.
True
2
proof
[(((triple6) -> rule3) OR ((((triple5) -> rule5)) -> rule3))]
("Dave" "is" "nice" "+")
((triple6) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not rough.
False
2
inv-proof
[(((triple4) -> rule4))]
("Dave" "is" "rough" "-")
((triple4) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "rough" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "red" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is not nice.[(triple1)] Anne is not rough.[(triple2)] Anne is not smart.[(triple3)] Dave is green.[(triple4)] Dave is kind.[(triple5)] Dave is not smart.[(triple7)] Dave is red.[(triple6 OR ((triple5) -> rule5))] Dave is white.[(triple8 OR ((((triple6) -> rule3)) -> rule7) OR ((((triple6) -> rule3) triple4) -> rule8) OR ((((((triple5) -> rule5)) -> rule3)) -> rule7) OR ((((((triple5) -> rule5)) -> rule3) triple4) -> rule8))] Fiona is green.[(triple9)] Fiona is kind.[(triple10)] Fiona is rough.[(triple11 OR ((triple9) -> rule4))] Fiona is smart.[(triple12)] Gary is kind.[(triple13)] Gary is nice.[(triple14 OR ((((triple13) -> rule5)) -> rule3))] Gary is smart.[(triple15)] @1: Dave is nice.[(((triple6) -> rule3) OR ((((triple5) -> rule5)) -> rule3))] Dave is rough.[(((triple4) -> rule4))] Fiona is red.[(((triple10) -> rule5))] Gary is red.[(((triple13) -> rule5) OR ((triple14 ((triple14) -> rule7)) -> rule6))] Gary is white.[(((triple14) -> rule7) OR ((((((triple13) -> rule5)) -> rule3)) -> rule7))] @2: Fiona is nice.[(((((triple10) -> rule5)) -> rule3))] @3: Fiona is white.[(((((((triple10) -> rule5)) -> rule3)) -> rule7) OR ((((((triple10) -> rule5)) -> rule3) triple9) -> rule8))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Anne is not rough.
("Anne" "is" "rough" "-")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is not smart.
("Dave" "is" "smart" "-")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple6
((triple5) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple8
((((triple6) -> (rule3 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple6) -> (rule3 % int2)) triple4) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2)) triple4) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
((triple9) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Gary is kind.
("Gary" "is" "kind" "+")
triple13
Gary is nice.
("Gary" "is" "nice" "+")
triple14
((((triple13) -> (rule5 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Dave is nice.
("Dave" "is" "nice" "+")
((triple6) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple4) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple10) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple13) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple14 ((triple14) -> (rule7 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple14) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((((triple13) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((((((triple10) -> (rule5 % int3))) -> (rule3 % int2)) triple9) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3