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