Charlie is big. Dave is white. Gary is round. All round things are kind. If Dave is round and Dave is cold then Dave is big. All kind things are big.
Charlie is big.
("Charlie" "is" "big" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is round.
("Gary" "is" "round" "+")
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If Dave is round and Dave is cold then Dave is big.
((("Dave" "is" "round" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "big" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Gary is kind.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "kind" "-")
((triple3) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("Gary" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Gary" "is" "big" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Dave is not big.
Unknown
inv-rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Dave" "is" "big" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "kind" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is big.[(triple1)] Dave is white.[(triple2)] Gary is round.[(triple3)] @1: Gary is kind.[(((triple3) -> rule1))] @2: Gary is big.[(((((triple3) -> rule1)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2