Anne is nice. Anne is quiet. Gary is furry. Gary is green. Gary is red. Harry is green. Harry is quiet. All furry people are nice. If someone is red then they are rough. If Harry is big then Harry is furry. If someone is nice and rough then they are green. If someone is green then they are rough. All green, rough people are big.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If Harry is big then Harry is furry.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "furry" "+"))
If someone is nice and rough then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All green, rough people are big.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Gary is not green.
False
1
inv-proof
[(triple4 OR ((((triple3) -> rule1) ((triple5) -> rule2)) -> rule4))]
("Gary" "is" "green" "-")
triple4
((((triple3) -> (rule1 % int3)) ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is rough.
True
2
proof
[(((triple4) -> rule5) OR ((triple5) -> rule2))]
("Gary" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple5) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple4) -> rule5) OR ((triple5) -> rule2))]
("Gary" "is" "rough" "-")
((triple4) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple5) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is big.
True
4
proof
[(((triple6 ((triple6) -> rule5)) -> rule6))]
("Harry" "is" "big" "+")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not big.
False
4
inv-proof
[(((triple6 ((triple6) -> rule5)) -> rule6))]
("Harry" "is" "big" "-")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
True
5
proof
[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule3))]
("Harry" "is" "furry" "+")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not furry.
False
5
inv-proof
[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule3))]
("Harry" "is" "furry" "-")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Anne is not big.
Unknown
inv-rconc
[@3: Anne is big.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule2 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is rough.
Unknown
rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule2 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not green.
Unknown
inv-rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is nice.[(triple1)] Anne is quiet.[(triple2)] Gary is furry.[(triple3)] Gary is green.[(triple4 OR ((((triple3) -> rule1) ((triple5) -> rule2)) -> rule4))] Gary is red.[(triple5)] Harry is green.[(triple6)] Harry is quiet.[(triple7)] @1: Gary is nice.[(((triple3) -> rule1))] Gary is rough.[(((triple4) -> rule5) OR ((triple5) -> rule2))] Harry is rough.[(((triple6) -> rule5))] @2: Gary is big.[(((triple4 ((triple4) -> rule5)) -> rule6) OR ((triple4 ((triple5) -> rule2)) -> rule6) OR ((((((triple3) -> rule1) ((triple5) -> rule2)) -> rule4) ((triple4) -> rule5)) -> rule6) OR ((((((triple3) -> rule1) ((triple5) -> rule2)) -> rule4) ((triple5) -> rule2)) -> rule6))] Harry is big.[(((triple6 ((triple6) -> rule5)) -> rule6))] @3: Harry is furry.[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule3))] @4: Harry is nice.[(((((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule3)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
((((triple3) -> (rule1 % int3)) ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple5) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple6) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple4 ((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple3) -> (rule1 % int4)) ((triple5) -> (rule2 % int3))) -> (rule4 % int2)) ((triple4) -> (rule5 % int3))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
((((((triple3) -> (rule1 % int4)) ((triple5) -> (rule2 % int3))) -> (rule4 % int2)) ((triple5) -> (rule2 % int3))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple6 ((triple6) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4