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