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