Dave is not kind. Fiona is not young. All young things are not kind. If something is round then it is young. If something is kind then it is furry. If Fiona is not young then Fiona is cold. If Dave is smart then Dave is kind. Cold things are smart.
Dave is not kind.
("Dave" "is" "kind" "-")
Fiona is not young.
("Fiona" "is" "young" "-")
All young things are not kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "-"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If Fiona is not young then Fiona is cold.
((("Fiona" "is" "young" "~")) -> ("Fiona" "is" "cold" "+"))
If Dave is smart then Dave is kind.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "kind" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Dave is not kind.
True
1
proof
[(triple1)]
("Dave" "is" "kind" "-")
triple1
Dave is kind.
False
1
inv-proof
[(triple1)]
("Dave" "is" "kind" "+")
triple1
Fiona is cold.
True
2
proof
[(((triple2) -> rule4))]
("Fiona" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple2) -> rule4))]
("Fiona" "is" "cold" "-")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("Fiona" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("Fiona" "is" "smart" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "furry" "+")
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "smart" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is not kind.[(triple1)] Fiona is not young.[(triple2)] @1: Fiona is cold.[(((triple2) -> rule4))] @2: Fiona is smart.[(((((triple2) -> rule4)) -> rule6))]
Dave is not kind.
("Dave" "is" "kind" "-")
triple1
Fiona is not young.
("Fiona" "is" "young" "-")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2