Gary is big. Gary is white. Gary is young. Harry is big. Harry is red. Harry is round. Harry is young. Young, red things are cold. Round things are red. If something is smart and red then it is young.
Gary is big.
("Gary" "is" "big" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Young, red things are cold.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is smart and red then it is young.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Harry is red.
True
1
proof
[(triple5 OR ((triple6) -> rule2))]
("Harry" "is" "red" "+")
triple5
((triple6) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Gary is not big.
False
1
inv-proof
[(triple1)]
("Gary" "is" "big" "-")
triple1
Harry is cold.
True
3
proof
[(((triple7 triple5) -> rule1) OR ((triple7 ((triple6) -> rule2)) -> rule1))]
("Harry" "is" "cold" "+")
((triple7 triple5) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple7 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((triple7 triple5) -> rule1) OR ((triple7 ((triple6) -> rule2)) -> rule1))]
("Harry" "is" "cold" "-")
((triple7 triple5) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple7 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Gary is not cold.
Unknown
inv-rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "red" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Gary is big.[(triple1)] Gary is white.[(triple2)] Gary is young.[(triple3)] Harry is big.[(triple4)] Harry is red.[(triple5 OR ((triple6) -> rule2))] Harry is round.[(triple6)] Harry is young.[(triple7)] @1: Harry is cold.[(((triple7 triple5) -> rule1) OR ((triple7 ((triple6) -> rule2)) -> rule1))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
((triple6) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
((triple7 triple5) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple7 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2