Anne is blue. Anne is cold. Anne is not furry. Anne is kind. Anne is nice. Anne is young. Charlie is kind. Charlie is young. Dave is cold. Dave is young. Fiona is nice. Fiona is white. Cold things are white. All white, furry things are young. If something is kind then it is young. Blue things are cold. If Charlie is not blue then Charlie is not kind. If Anne is young then Anne is kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
All white, furry things are young.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is kind then it is young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If Charlie is not blue then Charlie is not kind.
((("Charlie" "is" "blue" "~")) -> ("Charlie" "is" "kind" "-"))
If Anne is young then Anne is kind.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "kind" "+"))
Charlie is young.
True
1
proof
[(triple8 OR ((triple7) -> rule3))]
("Charlie" "is" "young" "+")
triple8
((triple7) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is not young.
False
1
inv-proof
[(triple6 OR ((triple4) -> rule3))]
("Anne" "is" "young" "-")
triple6
((triple4) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
True
2
proof
[(((triple2) -> rule1) OR ((((triple1) -> rule4)) -> rule1))]
("Anne" "is" "white" "+")
((triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not white.
False
2
inv-proof
[(((triple2) -> rule1) OR ((((triple1) -> rule4)) -> rule1))]
("Anne" "is" "white" "-")
((triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "cold" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2 OR ((triple1) -> rule4))] Anne is kind.[(triple4 OR ((triple6) -> rule6))] Anne is nice.[(triple5)] Anne is not furry.[(triple3)] Anne is young.[(triple6 OR ((triple4) -> rule3))] Charlie is kind.[(triple7)] Charlie is young.[(triple8 OR ((triple7) -> rule3))] Dave is cold.[(triple9)] Dave is young.[(triple10)] Fiona is nice.[(triple11)] Fiona is white.[(triple12)] @1: Anne is white.[(((triple2) -> rule1) OR ((((triple1) -> rule4)) -> rule1))] Dave is white.[(((triple9) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple6) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is not furry.
("Anne" "is" "furry" "-")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple6
((triple4) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
((triple7) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Anne is white.
("Anne" "is" "white" "+")
((triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1