Anne is rough. Bob is big. Bob is green. Bob is red. Bob is rough. Bob is round. Dave is big. Dave is furry. Fiona is round. Fiona is white. All rough things are not furry. If Fiona is green then Fiona is rough. All round things are red. If something is furry and not big then it is red. All round, rough things are green. If something is round and not white then it is green. All round, red things are green. All green things are rough.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All rough things are not furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "-"))
If Fiona is green then Fiona is rough.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "rough" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is furry and not big then it is red.
((("something" "is" "furry" "+") ("something" "is" "big" "~")) -> ("something" "is" "red" "+"))
All round, rough things are green.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is round and not white then it is green.
((("something" "is" "round" "+") ("something" "is" "white" "~")) -> ("something" "is" "green" "+"))
All round, red things are green.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Bob is green.
True
1
proof
[(triple3 OR ((triple6 triple4) -> rule7) OR ((triple6 triple5) -> rule5) OR ((triple6 ((triple6) -> rule3)) -> rule7))]
("Bob" "is" "green" "+")
triple3
((triple6 triple4) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple6 triple5) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple6 ((triple6) -> (rule3 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not red.
False
1
inv-proof
[(triple4 OR ((triple6) -> rule3))]
("Bob" "is" "red" "-")
triple4
((triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not furry.
True
2
proof
[(((triple5) -> rule1) OR ((((triple3) -> rule8)) -> rule1) OR ((((((triple6 triple4) -> rule7)) -> rule8)) -> rule1) OR ((((((triple6 ((triple6) -> rule3)) -> rule7)) -> rule8)) -> rule1))]
("Bob" "is" "furry" "-")
((triple5) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple6 triple4) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((triple6 ((triple6) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is furry.
False
2
inv-proof
[(((triple5) -> rule1) OR ((((triple3) -> rule8)) -> rule1) OR ((((((triple6 triple4) -> rule7)) -> rule8)) -> rule1) OR ((((((triple6 ((triple6) -> rule3)) -> rule7)) -> rule8)) -> rule1))]
("Bob" "is" "furry" "+")
((triple5) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple6 triple4) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((triple6 ((triple6) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Fiona is green.
True
4
proof
[(((triple9 ((triple9) -> rule3)) -> rule7))]
("Fiona" "is" "green" "+")
((triple9 ((triple9) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not green.
False
4
inv-proof
[(((triple9 ((triple9) -> rule3)) -> rule7))]
("Fiona" "is" "green" "-")
((triple9 ((triple9) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is rough.
True
5
proof
[(((((triple9 ((triple9) -> rule3)) -> rule7)) -> rule2) OR ((((triple9 ((triple9) -> rule3)) -> rule7)) -> rule8))]
("Fiona" "is" "rough" "+")
((((triple9 ((triple9) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((((triple9 ((triple9) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not rough.
False
5
inv-proof
[(((((triple9 ((triple9) -> rule3)) -> rule7)) -> rule2) OR ((((triple9 ((triple9) -> rule3)) -> rule7)) -> rule8))]
("Fiona" "is" "rough" "-")
((((triple9 ((triple9) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((((triple9 ((triple9) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "red" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "red" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "green" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is rough.[(triple1)] Bob is big.[(triple2)] Bob is green.[(triple3 OR ((triple6 triple4) -> rule7) OR ((triple6 triple5) -> rule5) OR ((triple6 ((triple6) -> rule3)) -> rule7))] Bob is red.[(triple4 OR ((triple6) -> rule3))] Bob is rough.[(triple5 OR ((triple3) -> rule8) OR ((((triple6 triple4) -> rule7)) -> rule8) OR ((((triple6 ((triple6) -> rule3)) -> rule7)) -> rule8))] Bob is round.[(triple6)] Dave is big.[(triple7)] Dave is furry.[(triple8)] Fiona is round.[(triple9)] Fiona is white.[(triple10)] @1: Anne is not furry.[(((triple1) -> rule1))] Bob is not furry.[(((triple5) -> rule1) OR ((((triple3) -> rule8)) -> rule1) OR ((((((triple6 triple4) -> rule7)) -> rule8)) -> rule1) OR ((((((triple6 ((triple6) -> rule3)) -> rule7)) -> rule8)) -> rule1))] Fiona is red.[(((triple9) -> rule3))] @2: Fiona is green.[(((triple9 ((triple9) -> rule3)) -> rule7))] @3: Fiona is rough.[(((((triple9 ((triple9) -> rule3)) -> rule7)) -> rule2) OR ((((triple9 ((triple9) -> rule3)) -> rule7)) -> rule8))] @4: Fiona is not furry.[(((((((triple9 ((triple9) -> rule3)) -> rule7)) -> rule2)) -> rule1) OR ((((((triple9 ((triple9) -> rule3)) -> rule7)) -> rule8)) -> rule1))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple6 triple4) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple6 triple5) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple6 ((triple6) -> (rule3 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple3) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple6 triple4) -> (rule7 % int2))) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple6 ((triple6) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Anne is not furry.
("Anne" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
((triple5) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple6 triple4) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((triple6 ((triple6) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Fiona is red.
("Fiona" "is" "red" "+")
((triple9) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple9 ((triple9) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple9 ((triple9) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((((triple9 ((triple9) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not furry.
("Fiona" "is" "furry" "-")
((((((triple9 ((triple9) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
((((((triple9 ((triple9) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4