Charlie is big. Fiona is cold. Harry is furry. If something is kind then it is furry. If Fiona is cold then Fiona is young. If something is cold then it is big. All big things are young. Kind things are quiet. If Charlie is furry then Charlie is not kind. Quiet, big things are not blue. If Harry is cold and Harry is not big then Harry is quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If Fiona is cold then Fiona is young.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "young" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is furry then Charlie is not kind.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "kind" "-"))
Quiet, big things are not blue.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
If Harry is cold and Harry is not big then Harry is quiet.
((("Harry" "is" "cold" "+") ("Harry" "is" "big" "~")) -> ("Harry" "is" "quiet" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Fiona is not cold.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "cold" "-")
triple2
Charlie is young.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "young" "+")
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple2) -> rule2) OR ((((triple2) -> rule3)) -> rule4))]
("Fiona" "is" "young" "-")
((triple2) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Charlie is big.[(triple1)] Fiona is cold.[(triple2)] Harry is furry.[(triple3)] @1: Charlie is young.[(((triple1) -> rule4))] Fiona is big.[(((triple2) -> rule3))] Fiona is young.[(((triple2) -> rule2) OR ((((triple2) -> rule3)) -> rule4))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple2) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple2) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2