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