Anne is cold. Anne is quiet. Anne is red. Anne is rough. Anne is round. Anne is young. Gary is cold. Gary is quiet. Gary is rough. Gary is young. Harry is red. Harry is rough. If Harry is rough and Harry is young then Harry is cold. Round people are kind. If someone is round and kind then they are rough. If someone is red and rough then they are quiet. If someone is kind and rough then they are quiet. All young people are red.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Harry is rough and Harry is young then Harry is cold.
((("Harry" "is" "rough" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "cold" "+"))
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is round and kind then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is red and rough then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind and rough then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Anne is rough.
True
1
proof
[(triple4 OR ((triple5 ((triple5) -> rule2)) -> rule3))]
("Anne" "is" "rough" "+")
triple4
((triple5 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Gary is not quiet.
False
1
inv-proof
[(triple8 OR ((((triple10) -> rule6) triple9) -> rule4))]
("Gary" "is" "quiet" "-")
triple8
((((triple10) -> (rule6 % int2)) triple9) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Anne is cold.[(triple1)] Anne is quiet.[(triple2 OR ((triple3 triple4) -> rule4) OR ((((triple5) -> rule2) triple4) -> rule5) OR ((((triple6) -> rule6) triple4) -> rule4) OR ((triple3 ((triple5 ((triple5) -> rule2)) -> rule3)) -> rule4) OR ((((triple5) -> rule2) ((triple5 ((triple5) -> rule2)) -> rule3)) -> rule5) OR ((((triple6) -> rule6) ((triple5 ((triple5) -> rule2)) -> rule3)) -> rule4))] Anne is red.[(triple3 OR ((triple6) -> rule6))] Anne is rough.[(triple4 OR ((triple5 ((triple5) -> rule2)) -> rule3))] Anne is round.[(triple5)] Anne is young.[(triple6)] Gary is cold.[(triple7)] Gary is quiet.[(triple8 OR ((((triple10) -> rule6) triple9) -> rule4))] Gary is rough.[(triple9)] Gary is young.[(triple10)] Harry is red.[(triple11)] Harry is rough.[(triple12)] @1: Anne is kind.[(((triple5) -> rule2))] Gary is red.[(((triple10) -> rule6))] Harry is quiet.[(((triple11 triple12) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3 triple4) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple5) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple6) -> (rule6 % int2)) triple4) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((triple3 ((triple5 ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple5) -> (rule2 % int3)) ((triple5 ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple6) -> (rule6 % int4)) ((triple5 ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple6) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple5 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is young.
("Anne" "is" "young" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
((((triple10) -> (rule6 % int2)) triple9) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Anne is kind.
("Anne" "is" "kind" "+")
((triple5) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple10) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple11 triple12) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1