Anne is not blue. Anne is kind. Anne is rough. Anne is smart. Anne is not white. Fiona is green. Fiona is red. Fiona is rough. Fiona is not smart. Gary is blue. Gary is green. Harry is not green. Harry is red. Harry is smart. Harry is white. Blue things are kind. White things are blue. If something is green then it is rough. All green things are white. If something is green and not blue then it is red. If something is blue and not rough then it is smart.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is not white.
("Anne" "is" "white" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
White things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is green and not blue then it is red.
((("something" "is" "green" "+") ("something" "is" "blue" "~")) -> ("something" "is" "red" "+"))
If something is blue and not rough then it is smart.
((("something" "is" "blue" "+") ("something" "is" "rough" "~")) -> ("something" "is" "smart" "+"))
Gary is green.
True
1
proof
[(triple11)]
("Gary" "is" "green" "+")
triple11
Fiona is not rough.
False
1
inv-proof
[(triple8 OR ((triple6) -> rule3))]
("Fiona" "is" "rough" "-")
triple8
((triple6) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is white.
True
2
proof
[(((triple6) -> rule4))]
("Fiona" "is" "white" "+")
((triple6) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple10) -> rule1) OR ((((((triple11) -> rule4)) -> rule2)) -> rule1))]
("Gary" "is" "kind" "-")
((triple10) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Fiona is blue.
True
3
proof
[(((((triple6) -> rule4)) -> rule2))]
("Fiona" "is" "blue" "+")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule2))]
("Fiona" "is" "blue" "-")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
True
4
proof
[(((((((triple6) -> rule4)) -> rule2)) -> rule1))]
("Fiona" "is" "kind" "+")
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is not kind.
False
4
inv-proof
[(((((((triple6) -> rule4)) -> rule2)) -> rule1))]
("Fiona" "is" "kind" "-")
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "smart" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "red" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "red" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "rough" "+")
@0: Anne is kind.[(triple2)] Anne is not blue.[(triple1)] Anne is not white.[(triple5)] Anne is rough.[(triple3)] Anne is smart.[(triple4)] Fiona is green.[(triple6)] Fiona is not smart.[(triple9)] Fiona is red.[(triple7)] Fiona is rough.[(triple8 OR ((triple6) -> rule3))] Gary is blue.[(triple10 OR ((((triple11) -> rule4)) -> rule2))] Gary is green.[(triple11)] Harry is not green.[(triple12)] Harry is red.[(triple13)] Harry is smart.[(triple14)] Harry is white.[(triple15)] @1: Fiona is white.[(((triple6) -> rule4))] Gary is kind.[(((triple10) -> rule1) OR ((((((triple11) -> rule4)) -> rule2)) -> rule1))] Gary is rough.[(((triple11) -> rule3))] Gary is white.[(((triple11) -> rule4))] Harry is blue.[(((triple15) -> rule2))] @2: Fiona is blue.[(((((triple6) -> rule4)) -> rule2))] Harry is kind.[(((((triple15) -> rule2)) -> rule1))] @3: Fiona is kind.[(((((((triple6) -> rule4)) -> rule2)) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is not white.
("Anne" "is" "white" "-")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple9
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
((triple6) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple10
((((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple11
Harry is not green.
("Harry" "is" "green" "-")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Fiona is white.
("Fiona" "is" "white" "+")
((triple6) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple10) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((triple11) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple11) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple15) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3