Anne is rough. Bob is big. Bob is quiet. Dave is big. Dave is quiet. Fiona is quiet. Fiona is rough. Furry, nice things are young. All rough, big things are smart. All young, nice things are rough. If something is big then it is furry. Furry things are nice.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Furry, nice things are young.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All rough, big things are smart.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All young, nice things are rough.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Dave is big.
True
1
proof
[(triple4)]
("Dave" "is" "big" "+")
triple4
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Dave is furry.
True
2
proof
[(((triple4) -> rule4))]
("Dave" "is" "furry" "+")
((triple4) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple4) -> rule4))]
("Dave" "is" "furry" "-")
((triple4) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
True
3
proof
[(((((triple4) -> rule4)) -> rule5))]
("Dave" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("Bob" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
True
6
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule5)) -> rule1))]
("Bob" "is" "young" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Dave is not young.
False
6
inv-proof
[(((((triple4) -> rule4) ((((triple4) -> rule4)) -> rule5)) -> rule1))]
("Dave" "is" "young" "-")
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
True
10
proof
[(((((((triple4) -> rule4) ((((triple4) -> rule4)) -> rule5)) -> rule1) ((((triple4) -> rule4)) -> rule5)) -> rule3))]
("Dave" "is" "rough" "+")
((((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple4) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Bob is not rough.
False
10
inv-proof
[(((((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule5)) -> rule1) ((((triple2) -> rule4)) -> rule5)) -> rule3))]
("Bob" "is" "rough" "-")
((((((triple2) -> (rule4 % int4)) ((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Dave is smart.
True
12
proof
[(((((((((triple4) -> rule4) ((((triple4) -> rule4)) -> rule5)) -> rule1) ((((triple4) -> rule4)) -> rule5)) -> rule3) triple4) -> rule2))]
("Dave" "is" "smart" "+")
((((((((triple4) -> (rule4 % int5)) ((((triple4) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule1 % int3)) ((((triple4) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Bob is not smart.
False
12
inv-proof
[(((((((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule5)) -> rule1) ((((triple2) -> rule4)) -> rule5)) -> rule3) triple2) -> rule2))]
("Bob" "is" "smart" "-")
((((((((triple2) -> (rule4 % int5)) ((((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule1 % int3)) ((((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "furry" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not young.
Unknown
inv-rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Anne" "is" "young" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "smart" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "furry" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is rough.[(triple1)] Bob is big.[(triple2)] Bob is quiet.[(triple3)] Dave is big.[(triple4)] Dave is quiet.[(triple5)] Fiona is quiet.[(triple6)] Fiona is rough.[(triple7)] @1: Bob is furry.[(((triple2) -> rule4))] Dave is furry.[(((triple4) -> rule4))] @2: Bob is nice.[(((((triple2) -> rule4)) -> rule5))] Dave is nice.[(((((triple4) -> rule4)) -> rule5))] @3: Bob is young.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule5)) -> rule1))] Dave is young.[(((((triple4) -> rule4) ((((triple4) -> rule4)) -> rule5)) -> rule1))] @4: Bob is rough.[(((((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule5)) -> rule1) ((((triple2) -> rule4)) -> rule5)) -> rule3))] Dave is rough.[(((((((triple4) -> rule4) ((((triple4) -> rule4)) -> rule5)) -> rule1) ((((triple4) -> rule4)) -> rule5)) -> rule3))] @5: Bob is smart.[(((((((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule5)) -> rule1) ((((triple2) -> rule4)) -> rule5)) -> rule3) triple2) -> rule2))] Dave is smart.[(((((((((triple4) -> rule4) ((((triple4) -> rule4)) -> rule5)) -> rule1) ((((triple4) -> rule4)) -> rule5)) -> rule3) triple4) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple4) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple2) -> (rule4 % int4)) ((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((((triple4) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
((((((((triple2) -> (rule4 % int5)) ((((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule1 % int3)) ((((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5
Dave is smart.
("Dave" "is" "smart" "+")
((((((((triple4) -> (rule4 % int5)) ((((triple4) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule1 % int3)) ((((triple4) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5