Charlie is young. Gary is green. All green things are smart. If something is red then it is smart. Red, green things are young. If Gary is smart then Gary is young. Round things are big. All smart things are green.
Charlie is young.
("Charlie" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
All green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is red then it is smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Red, green things are young.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Gary is smart then Gary is young.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "young" "+"))
Round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Charlie is young.
True
1
proof
[(triple1)]
("Charlie" "is" "young" "+")
triple1
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Gary is smart.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple2) -> rule1))]
("Gary" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("Gary" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("Gary" "is" "young" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@3: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule2 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is green.
Unknown
rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "green" "+")
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "big" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is young.[(triple1)] Gary is green.[(triple2)] @1: Gary is smart.[(((triple2) -> rule1))] @2: Gary is young.[(((((triple2) -> rule1)) -> rule4))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2