Anne is nice. Bob is big. Fiona is furry. All red people are rough. Big, rough people are nice. Rough, furry people are big. If someone is big then they are rough. If Bob is blue then Bob is big. All nice, rough people are furry.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is big.
("Bob" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
All red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Big, rough people are nice.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Rough, furry people are big.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Bob is blue then Bob is big.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "big" "+"))
All nice, rough people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Bob is not big.
False
1
inv-proof
[(triple2)]
("Bob" "is" "big" "-")
triple2
Bob is rough.
True
2
proof
[(((triple2) -> rule4))]
("Bob" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "rough" "-")
((triple2) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
True
4
proof
[(((triple2 ((triple2) -> rule4)) -> rule2))]
("Bob" "is" "nice" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not nice.
False
4
inv-proof
[(((triple2 ((triple2) -> rule4)) -> rule2))]
("Bob" "is" "nice" "-")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
True
7
proof
[(((((triple2 ((triple2) -> rule4)) -> rule2) ((triple2) -> rule4)) -> rule6))]
("Bob" "is" "furry" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not furry.
False
7
inv-proof
[(((((triple2 ((triple2) -> rule4)) -> rule2) ((triple2) -> rule4)) -> rule6))]
("Bob" "is" "furry" "-")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is furry.
Unknown
rconc
[@3: Anne is furry.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule3 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not rough.
Unknown
inv-rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Fiona is nice.
Unknown
rconc
[@3: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is nice.[(triple1)] Bob is big.[(triple2)] Fiona is furry.[(triple3)] @1: Bob is rough.[(((triple2) -> rule4))] @2: Bob is nice.[(((triple2 ((triple2) -> rule4)) -> rule2))] @3: Bob is furry.[(((((triple2 ((triple2) -> rule4)) -> rule2) ((triple2) -> rule4)) -> rule6))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3