Anne is furry. Bob is furry. Bob is nice. Dave is nice. Fiona is not blue. Fiona is not nice. Fiona is smart. If someone is furry and not nice then they are blue. If someone is nice then they are not blue. All furry people are green. Green people are red. If Fiona is nice and Fiona is not blue then Fiona is not green. If someone is red and not blue then they are young.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Fiona is not nice.
("Fiona" "is" "nice" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is furry and not nice then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "blue" "+"))
If someone is nice then they are not blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "-"))
All furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If Fiona is nice and Fiona is not blue then Fiona is not green.
((("Fiona" "is" "nice" "+") ("Fiona" "is" "blue" "~")) -> ("Fiona" "is" "green" "-"))
If someone is red and not blue then they are young.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "young" "+"))
Fiona is not nice.
True
1
proof
[(triple6)]
("Fiona" "is" "nice" "-")
triple6
Fiona is nice.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "nice" "+")
triple6
Bob is not blue.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Dave is blue.
False
2
inv-proof
[(((triple4) -> rule2))]
("Dave" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4))]
("Bob" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
True
6
proof
[(((((((triple2) -> rule3)) -> rule4) ((triple3) -> rule2)) -> rule6))]
("Bob" "is" "young" "+")
((((((triple2) -> (rule3 % int4))) -> (rule4 % int3)) ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not young.
False
6
inv-proof
[(((((((triple2) -> rule3)) -> rule4) ((triple3) -> rule2)) -> rule6))]
("Bob" "is" "young" "-")
((((((triple2) -> (rule3 % int4))) -> (rule4 % int3)) ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "young" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "young" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Bob is furry.[(triple2)] Bob is nice.[(triple3)] Dave is nice.[(triple4)] Fiona is not blue.[(triple5)] Fiona is not nice.[(triple6)] Fiona is smart.[(triple7)] @1: Anne is green.[(((triple1) -> rule3))] Bob is green.[(((triple2) -> rule3))] Bob is not blue.[(((triple3) -> rule2))] Dave is not blue.[(((triple4) -> rule2))] @2: Anne is red.[(((((triple1) -> rule3)) -> rule4))] Bob is red.[(((((triple2) -> rule3)) -> rule4))] @3: Bob is young.[(((((((triple2) -> rule3)) -> rule4) ((triple3) -> rule2)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple5
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
((triple4) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((((triple2) -> (rule3 % int4))) -> (rule4 % int3)) ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4