Anne is nice. Charlie is kind. Dave is kind. Fiona is blue. All nice things are kind. If something is kind and round then it is blue. If something is nice then it is green. All big, round things are blue. Blue, big things are red. If something is green then it is blue. If something is blue and green then it is big. If Dave is big then Dave is blue.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is kind and round then it is blue.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All big, round things are blue.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Blue, big things are red.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is blue and green then it is big.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If Dave is big then Dave is blue.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "blue" "+"))
Fiona is blue.
True
1
proof
[(triple4)]
("Fiona" "is" "blue" "+")
triple4
Charlie is not kind.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "kind" "-")
triple2
Anne is kind.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
True
6
proof
[(((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule7))]
("Anne" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not big.
False
6
inv-proof
[(((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule7))]
("Anne" "is" "big" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Dave is not red.
Unknown
inv-rconc
[@3: Dave is red.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule3 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is big.
Unknown
rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Dave" "is" "big" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "green" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Anne is nice.[(triple1)] Charlie is kind.[(triple2)] Dave is kind.[(triple3)] Fiona is blue.[(triple4)] @1: Anne is green.[(((triple1) -> rule3))] Anne is kind.[(((triple1) -> rule1))] @2: Anne is blue.[(((((triple1) -> rule3)) -> rule6))] @3: Anne is big.[(((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule7))] @4: Anne is red.[(((((((triple1) -> rule3)) -> rule6) ((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule7)) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule3 % int4))) -> (rule6 % int3)) ((((((triple1) -> (rule3 % int4))) -> (rule6 % int3)) ((triple1) -> (rule3 % int4))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4