Dave is cold. Erin is young. Fiona is furry. Quiet things are young. All blue, red things are young. All red, cold things are furry. If something is blue then it is quiet. Furry, young things are cold. All furry things are quiet.
Dave is cold.
("Dave" "is" "cold" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All blue, red things are young.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All red, cold things are furry.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Furry, young things are cold.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Dave is cold.
True
1
proof
[(triple1)]
("Dave" "is" "cold" "+")
triple1
Fiona is not furry.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "furry" "-")
triple3
Fiona is quiet.
True
2
proof
[(((triple3) -> rule6))]
("Fiona" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple3) -> rule6))]
("Fiona" "is" "quiet" "-")
((triple3) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("Fiona" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not young.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("Fiona" "is" "young" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is quiet.
Unknown
rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Dave" "is" "quiet" "+")
Erin is not cold.
Unknown
inv-rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Erin" "is" "cold" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is cold.[(triple1)] Erin is young.[(triple2)] Fiona is furry.[(triple3)] @1: Fiona is quiet.[(((triple3) -> rule6))] @2: Fiona is young.[(((((triple3) -> rule6)) -> rule1))] @3: Fiona is cold.[(((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule5))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3