Bob is big. Bob is furry. Bob is nice. Bob is rough. Bob is smart. Bob is young. Gary is rough. If Bob is smart and Bob is big then Bob is cold. Big, furry people are smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Bob is smart and Bob is big then Bob is cold.
((("Bob" "is" "smart" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "cold" "+"))
Big, furry people are smart.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Bob is smart.
True
1
proof
[(triple5 OR ((triple1 triple2) -> rule2))]
("Bob" "is" "smart" "+")
triple5
((triple1 triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not nice.
False
1
inv-proof
[(triple3)]
("Bob" "is" "nice" "-")
triple3
Bob is cold.
True
3
proof
[(((triple5 triple1) -> rule1) OR ((((triple1 triple2) -> rule2) triple1) -> rule1))]
("Bob" "is" "cold" "+")
((triple5 triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple1 triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((triple5 triple1) -> rule1) OR ((((triple1 triple2) -> rule2) triple1) -> rule1))]
("Bob" "is" "cold" "-")
((triple5 triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple1 triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is nice.[(triple3)] Bob is rough.[(triple4)] Bob is smart.[(triple5 OR ((triple1 triple2) -> rule2))] Bob is young.[(triple6)] Gary is rough.[(triple7)] @1: Bob is cold.[(((triple5 triple1) -> rule1) OR ((((triple1 triple2) -> rule2) triple1) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
((triple1 triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple5 triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple1 triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2