Anne is cold. Dave is white. Fiona is smart. Gary is nice. If something is white then it is furry. All furry, white things are smart. If Gary is not nice then Gary is not white. If something is smart and not white then it is not kind. All white, smart things are not kind. If something is kind then it is not red.
Anne is cold.
("Anne" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
All furry, white things are smart.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Gary is not nice then Gary is not white.
((("Gary" "is" "nice" "~")) -> ("Gary" "is" "white" "-"))
If something is smart and not white then it is not kind.
((("something" "is" "smart" "+") ("something" "is" "white" "~")) -> ("something" "is" "kind" "-"))
All white, smart things are not kind.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "-"))
If something is kind then it is not red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "-"))
Gary is nice.
True
1
proof
[(triple4)]
("Gary" "is" "nice" "+")
triple4
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Dave is furry.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("Dave" "is" "smart" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not smart.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("Dave" "is" "smart" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not kind.
True
6
proof
[(((triple2 ((((triple2) -> rule1) triple2) -> rule2)) -> rule5))]
("Dave" "is" "kind" "-")
((triple2 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is kind.
False
6
inv-proof
[(((triple2 ((((triple2) -> rule1) triple2) -> rule2)) -> rule5))]
("Dave" "is" "kind" "+")
((triple2 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "smart" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "furry" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is cold.[(triple1)] Dave is white.[(triple2)] Fiona is smart.[(triple3)] Gary is nice.[(triple4)] @1: Dave is furry.[(((triple2) -> rule1))] @2: Dave is smart.[(((((triple2) -> rule1) triple2) -> rule2))] @3: Dave is not kind.[(((triple2 ((((triple2) -> rule1) triple2) -> rule2)) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not kind.
("Dave" "is" "kind" "-")
((triple2 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3