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