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