Gary is quiet. Harry is furry. Green people are rough. Green, rough people are quiet. If Gary is cold then Gary is big. Furry people are green. If someone is quiet and big then they are rough. If Harry is big then Harry is cold.
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Green, rough people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is cold then Gary is big.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "big" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet and big then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Harry is big then Harry is cold.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "cold" "+"))
Gary is quiet.
True
1
proof
[(triple1)]
("Gary" "is" "quiet" "+")
triple1
Harry is not furry.
False
1
inv-proof
[(triple2)]
("Harry" "is" "furry" "-")
triple2
Harry is green.
True
2
proof
[(((triple2) -> rule4))]
("Harry" "is" "green" "+")
((triple2) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Harry" "is" "green" "-")
((triple2) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("Harry" "is" "rough" "+")
((((triple2) -> (rule4 % 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
[(((((triple2) -> rule4)) -> rule1))]
("Harry" "is" "rough" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
True
6
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule1)) -> rule2))]
("Harry" "is" "quiet" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not quiet.
False
6
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule1)) -> rule2))]
("Harry" "is" "quiet" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "cold" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Gary is quiet.[(triple1)] Harry is furry.[(triple2)] @1: Harry is green.[(((triple2) -> rule4))] @2: Harry is rough.[(((((triple2) -> rule4)) -> rule1))] @3: Harry is quiet.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule1)) -> rule2))]
Gary is quiet.
("Gary" "is" "quiet" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
((triple2) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3