Anne is big. Anne is nice. Anne is round. Dave is furry. Dave is round. Gary is big. Gary is furry. Gary is nice. Gary is red. Gary is round. Harry is red. Harry is round. All nice, quiet things are rough. All big things are quiet. Rough, quiet things are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
All nice, quiet things are rough.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Rough, quiet things are furry.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Gary is furry.
True
1
proof
[(triple7 OR ((((triple8 ((triple6) -> rule2)) -> rule1) ((triple6) -> rule2)) -> rule3))]
("Gary" "is" "furry" "+")
triple7
((((triple8 ((triple6) -> (rule2 % int3))) -> (rule1 % int2)) ((triple6) -> (rule2 % int3))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not furry.
False
1
inv-proof
[(triple7 OR ((((triple8 ((triple6) -> rule2)) -> rule1) ((triple6) -> rule2)) -> rule3))]
("Gary" "is" "furry" "-")
triple7
((((triple8 ((triple6) -> (rule2 % int3))) -> (rule1 % int2)) ((triple6) -> (rule2 % int3))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is quiet.
True
2
proof
[(((triple6) -> rule2))]
("Gary" "is" "quiet" "+")
((triple6) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Gary is rough.
True
4
proof
[(((triple8 ((triple6) -> rule2)) -> rule1))]
("Gary" "is" "rough" "+")
((triple8 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not rough.
False
4
inv-proof
[(((triple8 ((triple6) -> rule2)) -> rule1))]
("Gary" "is" "rough" "-")
((triple8 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Anne is furry.
True
7
proof
[(((((triple2 ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3))]
("Anne" "is" "furry" "+")
((((triple2 ((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not furry.
False
7
inv-proof
[(((((triple2 ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3))]
("Anne" "is" "furry" "-")
((((triple2 ((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Harry is furry.
Unknown
rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2)] Anne is round.[(triple3)] Dave is furry.[(triple4)] Dave is round.[(triple5)] Gary is big.[(triple6)] Gary is furry.[(triple7 OR ((((triple8 ((triple6) -> rule2)) -> rule1) ((triple6) -> rule2)) -> rule3))] Gary is nice.[(triple8)] Gary is red.[(triple9)] Gary is round.[(triple10)] Harry is red.[(triple11)] Harry is round.[(triple12)] @1: Anne is quiet.[(((triple1) -> rule2))] Gary is quiet.[(((triple6) -> rule2))] @2: Anne is rough.[(((triple2 ((triple1) -> rule2)) -> rule1))] Gary is rough.[(((triple8 ((triple6) -> rule2)) -> rule1))] @3: Anne is furry.[(((((triple2 ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
((((triple8 ((triple6) -> (rule2 % int3))) -> (rule1 % int2)) ((triple6) -> (rule2 % int3))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple6) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple8 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((triple2 ((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3