Charlie is quiet. Charlie is not red. Charlie is not young. Fiona is kind. Fiona is smart. Harry is kind. Harry is nice. All kind, red things are quiet. If something is smart then it is red. If something is smart and young then it is red.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is not young.
("Charlie" "is" "young" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All kind, red things are quiet.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is smart and young then it is red.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Charlie is quiet.
True
1
proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Charlie is red.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "red" "+")
triple2
Fiona is red.
True
2
proof
[(((triple5) -> rule2))]
("Fiona" "is" "red" "+")
((triple5) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple5) -> rule2))]
("Fiona" "is" "red" "-")
((triple5) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
True
4
proof
[(((triple4 ((triple5) -> rule2)) -> rule1))]
("Fiona" "is" "quiet" "+")
((triple4 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not quiet.
False
4
inv-proof
[(((triple4 ((triple5) -> rule2)) -> rule1))]
("Fiona" "is" "quiet" "-")
((triple4 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "red" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is not red.[(triple2)] Charlie is not young.[(triple3)] Charlie is quiet.[(triple1)] Fiona is kind.[(triple4)] Fiona is smart.[(triple5)] Harry is kind.[(triple6)] Harry is nice.[(triple7)] @1: Fiona is red.[(((triple5) -> rule2))] @2: Fiona is quiet.[(((triple4 ((triple5) -> rule2)) -> rule1))]
Charlie is not red.
("Charlie" "is" "red" "-")
triple2
Charlie is not young.
("Charlie" "is" "young" "-")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
Fiona is smart.
("Fiona" "is" "smart" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
((triple5) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple4 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2