Charlie is big. Charlie is cold. Charlie is nice. Dave is big. Gary is cold. Gary is green. Gary is red. All cold people are smart. Cold, smart people are red.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Cold, smart people are red.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Gary is not green.
False
1
inv-proof
[(triple6)]
("Gary" "is" "green" "-")
triple6
Gary is smart.
True
2
proof
[(((triple5) -> rule1))]
("Gary" "is" "smart" "+")
((triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple5) -> rule1))]
("Gary" "is" "smart" "-")
((triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is red.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "red" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "red" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "red" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Charlie is nice.[(triple3)] Dave is big.[(triple4)] Gary is cold.[(triple5)] Gary is green.[(triple6)] Gary is red.[(triple7 OR ((triple5 ((triple5) -> rule1)) -> rule2))] @1: Charlie is smart.[(((triple2) -> rule1))] Gary is smart.[(((triple5) -> rule1))] @2: Charlie is red.[(((triple2 ((triple2) -> rule1)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2