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