Anne is big. Charlie is not green. Charlie is rough. Erin is quiet. Erin is not young. Harry is nice. Harry is not quiet. All rough things are nice. All quiet, rough things are nice. Furry, quiet things are rough. All nice things are not furry. If something is furry then it is young. If something is green then it is young. Nice things are not quiet. If Harry is green and Harry is young then Harry is nice.
Anne is big.
("Anne" "is" "big" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is not young.
("Erin" "is" "young" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All quiet, rough things are nice.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Furry, quiet things are rough.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All nice things are not furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "-"))
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is green then it is young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Nice things are not quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "-"))
If Harry is green and Harry is young then Harry is nice.
((("Harry" "is" "green" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "nice" "+"))
Charlie is rough.
True
1
proof
[(triple3)]
("Charlie" "is" "rough" "+")
triple3
Charlie is not rough.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "rough" "-")
triple3
Charlie is nice.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not furry.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("Charlie" "is" "furry" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("Charlie" "is" "furry" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "young" "-")
Erin is nice.
Unknown
rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Erin" "is" "nice" "+")
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "young" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is big.[(triple1)] Charlie is not green.[(triple2)] Charlie is rough.[(triple3)] Erin is not young.[(triple5)] Erin is quiet.[(triple4)] Harry is nice.[(triple6)] Harry is not quiet.[(triple7 OR ((triple6) -> rule7))] @1: Charlie is nice.[(((triple3) -> rule1))] Harry is not furry.[(((triple6) -> rule4))] @2: Charlie is not furry.[(((((triple3) -> rule1)) -> rule4))] Charlie is not quiet.[(((((triple3) -> rule1)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Charlie is not green.
("Charlie" "is" "green" "-")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Erin is not young.
("Erin" "is" "young" "-")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple7
((triple6) -> (rule7 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Harry is not furry.
("Harry" "is" "furry" "-")
((triple6) -> (rule4 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2