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