Bob is green. Bob is smart. Charlie is big. Charlie is cold. Charlie is green. Charlie is nice. Charlie is smart. Charlie is young. Gary is big. Gary is smart. If someone is cold and young then they are nice. If someone is nice then they are young. If someone is green then they are kind.
Bob is green.
("Bob" "is" "green" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is cold and young then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Gary is big.
True
1
proof
[(triple9)]
("Gary" "is" "big" "+")
triple9
Charlie is not nice.
False
1
inv-proof
[(triple6 OR ((triple4 triple8) -> rule1))]
("Charlie" "is" "nice" "-")
triple6
((triple4 triple8) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Bob is kind.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is green.[(triple1)] Bob is smart.[(triple2)] Charlie is big.[(triple3)] Charlie is cold.[(triple4)] Charlie is green.[(triple5)] Charlie is nice.[(triple6 OR ((triple4 triple8) -> rule1))] Charlie is smart.[(triple7)] Charlie is young.[(triple8 OR ((triple6) -> rule2))] Gary is big.[(triple9)] Gary is smart.[(triple10)] @1: Bob is kind.[(((triple1) -> rule3))] Charlie is kind.[(((triple5) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((triple4 triple8) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
((triple6) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1