Charlie is green. Charlie is round. Dave is not white. Gary is blue. Gary is green. Gary is not rough. Gary is not young. All big, white people are round. If someone is round and not white then they are rough. Round people are rough. Round, big people are rough. All big, white people are not green. If Charlie is white then Charlie is rough. If someone is rough then they are young. If someone is blue and not rough then they are not young.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is not white.
("Dave" "is" "white" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is not young.
("Gary" "is" "young" "-")
All big, white people are round.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is round and not white then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "+"))
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Round, big people are rough.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All big, white people are not green.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "-"))
If Charlie is white then Charlie is rough.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "rough" "+"))
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is blue and not rough then they are not young.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "young" "-"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Gary is not green.
False
1
inv-proof
[(triple5)]
("Gary" "is" "green" "-")
triple5
Charlie is rough.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "rough" "-")
((triple2) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Dave is young.
Unknown
rconc
[@3: Dave is young.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule1 <- FAIL)]]
("Dave" "is" "young" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Charlie is green.[(triple1)] Charlie is round.[(triple2)] Dave is not white.[(triple3)] Gary is blue.[(triple4)] Gary is green.[(triple5)] Gary is not rough.[(triple6)] Gary is not young.[(triple7 OR ((triple4 triple6) -> rule8))] @1: Charlie is rough.[(((triple2) -> rule3))] @2: Charlie is young.[(((((triple2) -> rule3)) -> rule7))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is not white.
("Dave" "is" "white" "-")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is not rough.
("Gary" "is" "rough" "-")
triple6
Gary is not young.
("Gary" "is" "young" "-")
triple7
((triple4 triple6) -> (rule8 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2