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