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