Anne is young. Bob is rough. Gary is young. Harry is rough. White, quiet things are not young. If something is quiet then it is not round. Young, rough things are round. If something is young and big then it is rough. If something is white and round then it is big. Young things are big.
Anne is young.
("Anne" "is" "young" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is rough.
("Harry" "is" "rough" "+")
White, quiet things are not young.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "-"))
If something is quiet then it is not round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "-"))
Young, rough things are round.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is young and big then it is rough.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is white and round then it is big.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Anne is young.
True
1
proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Bob is not rough.
False
1
inv-proof
[(triple2)]
("Bob" "is" "rough" "-")
triple2
Gary is big.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "big" "+")
((triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "big" "-")
((triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Anne is rough.
True
4
proof
[(((triple1 ((triple1) -> rule6)) -> rule4))]
("Anne" "is" "rough" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule4))]
("Anne" "is" "rough" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Gary is round.
True
6
proof
[(((triple3 ((triple3 ((triple3) -> rule6)) -> rule4)) -> rule3))]
("Gary" "is" "round" "+")
((triple3 ((triple3 ((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Anne is not round.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule6)) -> rule4)) -> rule3))]
("Anne" "is" "round" "-")
((triple1 ((triple1 ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "round" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is young.[(triple1)] Bob is rough.[(triple2)] Gary is young.[(triple3)] Harry is rough.[(triple4)] @1: Anne is big.[(((triple1) -> rule6))] Gary is big.[(((triple3) -> rule6))] @2: Anne is rough.[(((triple1 ((triple1) -> rule6)) -> rule4))] Gary is rough.[(((triple3 ((triple3) -> rule6)) -> rule4))] @3: Anne is round.[(((triple1 ((triple1 ((triple1) -> rule6)) -> rule4)) -> rule3))] Gary is round.[(((triple3 ((triple3 ((triple3) -> rule6)) -> rule4)) -> rule3))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple1 ((triple1 ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((triple3 ((triple3 ((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3