Gary is kind. Harry is cold. Harry is kind. If something is kind and nice then it is cold. If Harry is kind then Harry is smart. Round things are nice. If Harry is kind and Harry is nice then Harry is red. If something is cold and smart then it is round. If something is nice then it is red. If Gary is nice then Gary is round. All kind things are red.
Gary is kind.
("Gary" "is" "kind" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If something is kind and nice then it is cold.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If Harry is kind then Harry is smart.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "smart" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If Harry is kind and Harry is nice then Harry is red.
((("Harry" "is" "kind" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "red" "+"))
If something is cold and smart then it is round.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Gary is nice then Gary is round.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "round" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Harry is cold.
True
1
proof
[(triple2)]
("Harry" "is" "cold" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple2)]
("Harry" "is" "cold" "-")
triple2
Harry is red.
True
2
proof
[(((triple3) -> rule8) OR ((((((triple2 ((triple3) -> rule2)) -> rule5)) -> rule3)) -> rule6) OR ((triple3 ((((triple2 ((triple3) -> rule2)) -> rule5)) -> rule3)) -> rule4))]
("Harry" "is" "red" "+")
((triple3) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((((triple2 ((triple3) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((triple3 ((((triple2 ((triple3) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is not red.
False
2
inv-proof
[(((triple3) -> rule8) OR ((((((triple2 ((triple3) -> rule2)) -> rule5)) -> rule3)) -> rule6) OR ((triple3 ((((triple2 ((triple3) -> rule2)) -> rule5)) -> rule3)) -> rule4))]
("Harry" "is" "red" "-")
((triple3) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((((triple2 ((triple3) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((triple3 ((((triple2 ((triple3) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Gary is not nice.
Unknown
inv-rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is round.
Unknown
rconc
[@3: Gary is round.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule5 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Gary is kind.[(triple1)] Harry is cold.[(triple2)] Harry is kind.[(triple3)] @1: Gary is red.[(((triple1) -> rule8))] Harry is red.[(((triple3) -> rule8) OR ((((((triple2 ((triple3) -> rule2)) -> rule5)) -> rule3)) -> rule6) OR ((triple3 ((((triple2 ((triple3) -> rule2)) -> rule5)) -> rule3)) -> rule4))] Harry is smart.[(((triple3) -> rule2))] @2: Harry is round.[(((triple2 ((triple3) -> rule2)) -> rule5))] @3: Harry is nice.[(((((triple2 ((triple3) -> rule2)) -> rule5)) -> rule3))]
Gary is kind.
("Gary" "is" "kind" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
((triple1) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple3) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((((triple2 ((triple3) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((triple3 ((((triple2 ((triple3) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple2 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple2 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3