Bob is nice. Charlie is young. Gary is kind. If something is young then it is nice. Young, nice things are big. If Charlie is furry then Charlie is young.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Young, nice things are big.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If Charlie is furry then Charlie is young.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "young" "+"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Charlie is not young.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "young" "-")
triple2
Charlie is nice.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "nice" "-")
((triple2) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "big" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not big.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "big" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is nice.[(triple1)] Charlie is young.[(triple2)] Gary is kind.[(triple3)] @1: Charlie is nice.[(((triple2) -> rule1))] @2: Charlie is big.[(((triple2 ((triple2) -> rule1)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2