Bob is green. Charlie is cold. Charlie is smart. Gary is big. Gary is green. Gary is white. Gary is young. If Gary is big and Gary is blue then Gary is cold. Young people are blue.
Bob is green.
("Bob" "is" "green" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is big and Gary is blue then Gary is cold.
((("Gary" "is" "big" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "cold" "+"))
Young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Gary is big.
True
1
proof
[(triple4)]
("Gary" "is" "big" "+")
triple4
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Gary is blue.
True
2
proof
[(((triple7) -> rule2))]
("Gary" "is" "blue" "+")
((triple7) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple7) -> rule2))]
("Gary" "is" "blue" "-")
((triple7) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
True
4
proof
[(((triple4 ((triple7) -> rule2)) -> rule1))]
("Gary" "is" "cold" "+")
((triple4 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not cold.
False
4
inv-proof
[(((triple4 ((triple7) -> rule2)) -> rule1))]
("Gary" "is" "cold" "-")
((triple4 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is green.[(triple1)] Charlie is cold.[(triple2)] Charlie is smart.[(triple3)] Gary is big.[(triple4)] Gary is green.[(triple5)] Gary is white.[(triple6)] Gary is young.[(triple7)] @1: Gary is blue.[(((triple7) -> rule2))] @2: Gary is cold.[(((triple4 ((triple7) -> rule2)) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
((triple7) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple4 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2