Bob is furry. Dave is red. Fiona is rough. If Bob is red and Bob is quiet then Bob is not white. All red people are quiet. If Fiona is rough and Fiona is kind then Fiona is quiet. If Dave is not nice then Dave is quiet. All furry people are red. If someone is nice then they are furry.
Bob is furry.
("Bob" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If Bob is red and Bob is quiet then Bob is not white.
((("Bob" "is" "red" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "white" "-"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Fiona is rough and Fiona is kind then Fiona is quiet.
((("Fiona" "is" "rough" "+") ("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "quiet" "+"))
If Dave is not nice then Dave is quiet.
((("Dave" "is" "nice" "~")) -> ("Dave" "is" "quiet" "+"))
All furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Dave is red.
True
1
proof
[(triple2)]
("Dave" "is" "red" "+")
triple2
Fiona is not rough.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Dave is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "red" "-")
((triple1) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Fiona is not quiet.
Unknown
inv-rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule6 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "furry" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is furry.[(triple1)] Dave is red.[(triple2)] Fiona is rough.[(triple3)] @1: Bob is red.[(((triple1) -> rule5))] Dave is quiet.[(((triple2) -> rule2))] @2: Bob is quiet.[(((((triple1) -> rule5)) -> rule2))] @3: Bob is not white.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule2)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not white.
("Bob" "is" "white" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3