Anne is cold. Anne is green. Anne is nice. Anne is red. Anne is young. Fiona is cold. Fiona is red. Fiona is smart. Fiona is white. Fiona is young. Gary is cold. Gary is green. Gary is nice. Gary is smart. Gary is white. Gary is young. All young, green things are white. Nice things are green. If something is cold and white then it is smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All young, green things are white.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is cold and white then it is smart.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Fiona is smart.
True
1
proof
[(triple8 OR ((triple6 triple9) -> rule3))]
("Fiona" "is" "smart" "+")
triple8
((triple6 triple9) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is not green.
False
1
inv-proof
[(triple12 OR ((triple13) -> rule2))]
("Gary" "is" "green" "-")
triple12
((triple13) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Anne is white.
True
3
proof
[(((triple5 triple2) -> rule1) OR ((triple5 ((triple3) -> rule2)) -> rule1))]
("Anne" "is" "white" "+")
((triple5 triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not white.
False
3
inv-proof
[(((triple5 triple2) -> rule1) OR ((triple5 ((triple3) -> rule2)) -> rule1))]
("Anne" "is" "white" "-")
((triple5 triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
True
5
proof
[(((triple1 ((triple5 triple2) -> rule1)) -> rule3) OR ((triple1 ((triple5 ((triple3) -> rule2)) -> rule1)) -> rule3))]
("Anne" "is" "smart" "+")
((triple1 ((triple5 triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((triple1 ((triple5 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not smart.
False
5
inv-proof
[(((triple1 ((triple5 triple2) -> rule1)) -> rule3) OR ((triple1 ((triple5 ((triple3) -> rule2)) -> rule1)) -> rule3))]
("Anne" "is" "smart" "-")
((triple1 ((triple5 triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((triple1 ((triple5 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2 OR ((triple3) -> rule2))] Anne is nice.[(triple3)] Anne is red.[(triple4)] Anne is young.[(triple5)] Fiona is cold.[(triple6)] Fiona is red.[(triple7)] Fiona is smart.[(triple8 OR ((triple6 triple9) -> rule3))] Fiona is white.[(triple9)] Fiona is young.[(triple10)] Gary is cold.[(triple11)] Gary is green.[(triple12 OR ((triple13) -> rule2))] Gary is nice.[(triple13)] Gary is smart.[(triple14 OR ((triple11 triple15) -> rule3) OR ((triple11 ((triple16 triple12) -> rule1)) -> rule3) OR ((triple11 ((triple16 ((triple13) -> rule2)) -> rule1)) -> rule3))] Gary is white.[(triple15 OR ((triple16 triple12) -> rule1) OR ((triple16 ((triple13) -> rule2)) -> rule1))] Gary is young.[(triple16)] @1: Anne is white.[(((triple5 triple2) -> rule1) OR ((triple5 ((triple3) -> rule2)) -> rule1))] @2: Anne is smart.[(((triple1 ((triple5 triple2) -> rule1)) -> rule3) OR ((triple1 ((triple5 ((triple3) -> rule2)) -> rule1)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
((triple6 triple9) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Gary is cold.
("Gary" "is" "cold" "+")
triple11
Gary is green.
("Gary" "is" "green" "+")
triple12
((triple13) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14
((triple11 triple15) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple11 ((triple16 triple12) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple11 ((triple16 ((triple13) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple15
((triple16 triple12) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple16 ((triple13) -> (rule2 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple16
Anne is white.
("Anne" "is" "white" "+")
((triple5 triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 ((triple5 triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((triple1 ((triple5 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3