Gary is cold. Gary is round. Harry is nice. Harry is quiet. Harry is not red. Harry is rough. Harry is round. If someone is cold then they are rough. All red people are cold. Rough people are big.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is cold then they are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Gary is round.
True
1
proof
[(triple2)]
("Gary" "is" "round" "+")
triple2
Harry is not round.
False
1
inv-proof
[(triple7)]
("Harry" "is" "round" "-")
triple7
Gary is rough.
True
2
proof
[(((triple1) -> rule1))]
("Gary" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple6) -> rule3))]
("Harry" "is" "big" "-")
((triple6) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Gary is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Gary" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Gary" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Gary is cold.[(triple1)] Gary is round.[(triple2)] Harry is nice.[(triple3)] Harry is not red.[(triple5)] Harry is quiet.[(triple4)] Harry is rough.[(triple6)] Harry is round.[(triple7)] @1: Gary is rough.[(((triple1) -> rule1))] Harry is big.[(((triple6) -> rule3))] @2: Gary is big.[(((((triple1) -> rule1)) -> rule3))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is round.
("Gary" "is" "round" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Harry is not red.
("Harry" "is" "red" "-")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple6) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2