Anne is red. Charlie is rough. Erin is furry. Gary is rough. If Charlie is big and Charlie is young then Charlie is furry. Young people are big. All rough people are young.
Anne is red.
("Anne" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Charlie is big and Charlie is young then Charlie is furry.
((("Charlie" "is" "big" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "furry" "+"))
Young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Erin is furry.
True
1
proof
[(triple3)]
("Erin" "is" "furry" "+")
triple3
Gary is not rough.
False
1
inv-proof
[(triple4)]
("Gary" "is" "rough" "-")
triple4
Gary is young.
True
2
proof
[(((triple4) -> rule3))]
("Gary" "is" "young" "+")
((triple4) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "young" "-")
((triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is big.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Gary" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Gary" "is" "big" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Charlie is furry.
True
6
proof
[(((((((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "furry" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not furry.
False
6
inv-proof
[(((((((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "furry" "-")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "young" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "young" "+")
Erin is not big.
Unknown
inv-rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Erin" "is" "big" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "big" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Anne is red.[(triple1)] Charlie is rough.[(triple2)] Erin is furry.[(triple3)] Gary is rough.[(triple4)] @1: Charlie is young.[(((triple2) -> rule3))] Gary is young.[(((triple4) -> rule3))] @2: Charlie is big.[(((((triple2) -> rule3)) -> rule2))] Gary is big.[(((((triple4) -> rule3)) -> rule2))] @3: Charlie is furry.[(((((((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
((triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple4) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3