Anne is blue. Anne is cold. Anne is white. Dave is green. Fiona is smart. Gary is cold. Gary is young. Cold, kind things are young. All smart, kind things are cold. Blue things are white. All young things are blue. All smart things are kind. If something is green and kind then it is young. If Gary is cold and Gary is green then Gary is smart. If something is cold and young then it is blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
Cold, kind things are young.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All smart, kind things are cold.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If something is green and kind then it is young.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Gary is cold and Gary is green then Gary is smart.
((("Gary" "is" "cold" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "smart" "+"))
If something is cold and young then it is blue.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not cold.
False
1
inv-proof
[(triple2)]
("Anne" "is" "cold" "-")
triple2
Gary is blue.
True
2
proof
[(((triple7) -> rule4) OR ((triple6 triple7) -> rule8))]
("Gary" "is" "blue" "+")
((triple7) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple6 triple7) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple5) -> rule5))]
("Fiona" "is" "kind" "-")
((triple5) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Gary is white.
True
3
proof
[(((((triple7) -> rule4)) -> rule3) OR ((((triple6 triple7) -> rule8)) -> rule3))]
("Gary" "is" "white" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple6 triple7) -> (rule8 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Fiona is not cold.
False
4
inv-proof
[(((triple5 ((triple5) -> rule5)) -> rule2))]
("Fiona" "is" "cold" "-")
((triple5 ((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
True
7
proof
[(((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1))]
("Fiona" "is" "young" "+")
((((triple5 ((triple5) -> (rule5 % int3))) -> (rule2 % int2)) ((triple5) -> (rule5 % int3))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is not young.
False
7
inv-proof
[(((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1))]
("Fiona" "is" "young" "-")
((((triple5 ((triple5) -> (rule5 % int3))) -> (rule2 % int2)) ((triple5) -> (rule5 % int3))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is blue.
True
8
proof
[(((((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule4) OR ((((triple5 ((triple5) -> rule5)) -> rule2) ((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule8))]
("Fiona" "is" "blue" "+")
((((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((triple5) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((triple5) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is not blue.
False
8
inv-proof
[(((((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule4) OR ((((triple5 ((triple5) -> rule5)) -> rule2) ((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule8))]
("Fiona" "is" "blue" "-")
((((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((triple5) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((triple5) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is white.
True
9
proof
[(((((((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule4)) -> rule3) OR ((((((triple5 ((triple5) -> rule5)) -> rule2) ((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule8)) -> rule3))]
("Fiona" "is" "white" "+")
((((((((triple5 ((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((triple5) -> (rule5 % int5))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
((((((triple5 ((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((((triple5 ((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((triple5) -> (rule5 % int5))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Fiona is not white.
False
9
inv-proof
[(((((((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule4)) -> rule3) OR ((((((triple5 ((triple5) -> rule5)) -> rule2) ((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule8)) -> rule3))]
("Fiona" "is" "white" "-")
((((((((triple5 ((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((triple5) -> (rule5 % int5))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
((((((triple5 ((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((((triple5 ((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((triple5) -> (rule5 % int5))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "smart" "-")
Dave is blue.
Unknown
rconc
[@3: Dave is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule2 <- FAIL)]]
("Dave" "is" "blue" "+")
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "kind" "-")
Gary is kind.
Unknown
rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Gary" "is" "kind" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "cold" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is white.[(triple3 OR ((triple1) -> rule3))] Dave is green.[(triple4)] Fiona is smart.[(triple5)] Gary is cold.[(triple6)] Gary is young.[(triple7)] @1: Fiona is kind.[(((triple5) -> rule5))] Gary is blue.[(((triple7) -> rule4) OR ((triple6 triple7) -> rule8))] @2: Fiona is cold.[(((triple5 ((triple5) -> rule5)) -> rule2))] Gary is white.[(((((triple7) -> rule4)) -> rule3) OR ((((triple6 triple7) -> rule8)) -> rule3))] @3: Fiona is young.[(((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1))] @4: Fiona is blue.[(((((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule4) OR ((((triple5 ((triple5) -> rule5)) -> rule2) ((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule8))] @5: Fiona is white.[(((((((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule4)) -> rule3) OR ((((((triple5 ((triple5) -> rule5)) -> rule2) ((((triple5 ((triple5) -> rule5)) -> rule2) ((triple5) -> rule5)) -> rule1)) -> rule8)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple4
Fiona is smart.
("Fiona" "is" "smart" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple5) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple7) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple6 triple7) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple5 ((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple6 triple7) -> (rule8 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple5 ((triple5) -> (rule5 % int3))) -> (rule2 % int2)) ((triple5) -> (rule5 % int3))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((triple5) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((triple5) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
((((((((triple5 ((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((triple5) -> (rule5 % int5))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
((((((triple5 ((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((((triple5 ((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((triple5) -> (rule5 % int5))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5