Dave is round. Fiona is kind. Gary is round. All blue things are round. If something is round then it is blue. Red things are kind. If Dave is white then Dave is kind. If something is blue then it is round. Blue things are red. All blue, quiet things are red. All nice things are kind.
Dave is round.
("Dave" "is" "round" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Dave is white then Dave is kind.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "kind" "+"))
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All blue, quiet things are red.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Fiona is kind.
True
1
proof
[(triple2)]
("Fiona" "is" "kind" "+")
triple2
Fiona is not kind.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "kind" "-")
triple2
Gary is blue.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is red.
True
3
proof
[(((((triple3) -> rule2)) -> rule6))]
("Gary" "is" "red" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not red.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6))]
("Gary" "is" "red" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Fiona is not red.
Unknown
inv-rconc
[@3: Fiona is red.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is round.
Unknown
rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "blue" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Dave is round.[(triple1)] Fiona is kind.[(triple2)] Gary is round.[(triple3)] @1: Dave is blue.[(((triple1) -> rule2))] Gary is blue.[(((triple3) -> rule2))] @2: Dave is red.[(((((triple1) -> rule2)) -> rule6))] Gary is red.[(((((triple3) -> rule2)) -> rule6))] @3: Dave is kind.[(((((((triple1) -> rule2)) -> rule6)) -> rule3))] Gary is kind.[(((((((triple3) -> rule2)) -> rule6)) -> rule3))]
Dave is round.
("Dave" "is" "round" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3