Anne is big. Anne is not furry. Anne is rough. Anne is young. Bob is blue. Bob is not furry. Bob is not red. Fiona is not blue. Fiona is rough. Fiona is young. Big people are rough. If Anne is rough then Anne is not blue. If someone is rough and not blue then they are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is not red.
("Bob" "is" "red" "-")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Anne is rough then Anne is not blue.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "blue" "-"))
If someone is rough and not blue then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "red" "+"))
Anne is young.
True
1
proof
[(triple4)]
("Anne" "is" "young" "+")
triple4
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Fiona is red.
True
3
proof
[(((triple9 triple8) -> rule3))]
("Fiona" "is" "red" "+")
((triple9 triple8) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
3
inv-proof
[(((triple9 triple8) -> rule3))]
("Fiona" "is" "red" "-")
((triple9 triple8) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is red.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule3) OR ((((triple1) -> rule1) ((triple3) -> rule2)) -> rule3) OR ((triple3 ((((triple1) -> rule1)) -> rule2)) -> rule3) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "red" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
((((triple1) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((triple3 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not red.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule3) OR ((((triple1) -> rule1) ((triple3) -> rule2)) -> rule3) OR ((triple3 ((((triple1) -> rule1)) -> rule2)) -> rule3) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "red" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
((((triple1) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((triple3 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is not furry.[(triple2)] Anne is rough.[(triple3 OR ((triple1) -> rule1))] Anne is young.[(triple4)] Bob is blue.[(triple5)] Bob is not furry.[(triple6)] Bob is not red.[(triple7)] Fiona is not blue.[(triple8)] Fiona is rough.[(triple9)] Fiona is young.[(triple10)] @1: Anne is not blue.[(((triple3) -> rule2) OR ((((triple1) -> rule1)) -> rule2))] Fiona is red.[(((triple9 triple8) -> rule3))] @2: Anne is red.[(((triple3 ((triple3) -> rule2)) -> rule3) OR ((((triple1) -> rule1) ((triple3) -> rule2)) -> rule3) OR ((triple3 ((((triple1) -> rule1)) -> rule2)) -> rule3) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is not furry.
("Anne" "is" "furry" "-")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
triple5
Bob is not furry.
("Bob" "is" "furry" "-")
triple6
Bob is not red.
("Bob" "is" "red" "-")
triple7
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Anne is not blue.
("Anne" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((triple9 triple8) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
((((triple1) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((triple3 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3