Anne is green. Anne is nice. Anne is red. Anne is rough. Anne is round. Anne is smart. Charlie is red. Charlie is round. Gary is rough. Gary is round. If something is smart then it is young. All red things are smart. If Charlie is young then Charlie is rough.
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Charlie is young then Charlie is rough.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "rough" "+"))
Gary is rough.
True
1
proof
[(triple9)]
("Gary" "is" "rough" "+")
triple9
Gary is not rough.
False
1
inv-proof
[(triple9)]
("Gary" "is" "rough" "-")
triple9
Anne is young.
True
2
proof
[(((triple6) -> rule1) OR ((((triple3) -> rule2)) -> rule1))]
("Anne" "is" "young" "+")
((triple6) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not young.
False
2
inv-proof
[(((triple6) -> rule1) OR ((((triple3) -> rule2)) -> rule1))]
("Anne" "is" "young" "-")
((triple6) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is young.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("Charlie" "is" "young" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("Charlie" "is" "young" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
True
4
proof
[(((((((triple7) -> rule2)) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "+")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not rough.
False
4
inv-proof
[(((((((triple7) -> rule2)) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "-")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is green.[(triple1)] Anne is nice.[(triple2)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Anne is round.[(triple5)] Anne is smart.[(triple6 OR ((triple3) -> rule2))] Charlie is red.[(triple7)] Charlie is round.[(triple8)] Gary is rough.[(triple9)] Gary is round.[(triple10)] @1: Anne is young.[(((triple6) -> rule1) OR ((((triple3) -> rule2)) -> rule1))] Charlie is smart.[(((triple7) -> rule2))] @2: Charlie is young.[(((((triple7) -> rule2)) -> rule1))] @3: Charlie is rough.[(((((((triple7) -> rule2)) -> rule1)) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Anne is young.
("Anne" "is" "young" "+")
((triple6) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3