Bob is big. Charlie is cold. Dave is big. Gary is big. Gary is cold. Gary is white. Gary is young. If something is young then it is white. Nice things are blue.
Bob is big.
("Bob" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is young then it is white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Gary is white.
True
1
proof
[(triple6 OR ((triple7) -> rule1))]
("Gary" "is" "white" "+")
triple6
((triple7) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "white" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Bob is big.[(triple1)] Charlie is cold.[(triple2)] Dave is big.[(triple3)] Gary is big.[(triple4)] Gary is cold.[(triple5)] Gary is white.[(triple6 OR ((triple7) -> rule1))] Gary is young.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
((triple7) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple7