Anne is smart. Charlie is furry. Fiona is young. Harry is furry. Red things are young. Furry things are red. Red, young things are not smart. If Charlie is green then Charlie is not smart. If something is smart and red then it is quiet. If Charlie is smart and Charlie is green then Charlie is not rough.
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Red, young things are not smart.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "-"))
If Charlie is green then Charlie is not smart.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "smart" "-"))
If something is smart and red then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is smart and Charlie is green then Charlie is not rough.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "rough" "-"))
Charlie is furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Harry is not furry.
False
1
inv-proof
[(triple4)]
("Harry" "is" "furry" "-")
triple4
Harry is red.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "red" "+")
((triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "red" "-")
((triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Charlie is young.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not smart.
True
6
proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Charlie" "is" "smart" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is smart.
False
6
inv-proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Charlie" "is" "smart" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "young" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is smart.[(triple1)] Charlie is furry.[(triple2)] Fiona is young.[(triple3)] Harry is furry.[(triple4)] @1: Charlie is red.[(((triple2) -> rule2))] Harry is red.[(((triple4) -> rule2))] @2: Charlie is young.[(((((triple2) -> rule2)) -> rule1))] Harry is young.[(((((triple4) -> rule2)) -> rule1))] @3: Charlie is not smart.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule3))] Harry is not smart.[(((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule1)) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Charlie is not smart.
("Charlie" "is" "smart" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Harry is not smart.
("Harry" "is" "smart" "-")
((((triple4) -> (rule2 % int3)) ((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3