Anne is big. Anne is rough. Dave is furry. Dave is kind. Dave is red. Dave is rough. Fiona is kind. Fiona is red. Gary is furry. Gary is red. If Dave is big then Dave is smart. Big, rough people are white. If Fiona is big and Fiona is furry then Fiona is rough. All rough, smart people are furry. All white people are red. If someone is smart then they are furry. Red, kind people are smart. All red people are kind. If Fiona is white then Fiona is big.
Anne is big.
("Anne" "is" "big" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
If Dave is big then Dave is smart.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "smart" "+"))
Big, rough people are white.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Fiona is big and Fiona is furry then Fiona is rough.
((("Fiona" "is" "big" "+") ("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "rough" "+"))
All rough, smart people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All white people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Red, kind people are smart.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If Fiona is white then Fiona is big.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "big" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Dave is smart.
True
3
proof
[(((triple5 triple4) -> rule7) OR ((triple5 ((triple5) -> rule8)) -> rule7))]
("Dave" "is" "smart" "+")
((triple5 triple4) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple5 ((triple5) -> (rule8 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Gary is not kind.
False
2
inv-proof
[(((triple10) -> rule8))]
("Gary" "is" "kind" "-")
((triple10) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Fiona is furry.
True
4
proof
[(((((triple8 triple7) -> rule7)) -> rule6) OR ((((triple8 ((triple8) -> rule8)) -> rule7)) -> rule6))]
("Fiona" "is" "furry" "+")
((((triple8 triple7) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8 ((triple8) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Anne is not red.
False
4
inv-proof
[(((((triple1 triple2) -> rule2)) -> rule5))]
("Anne" "is" "red" "-")
((((triple1 triple2) -> (rule2 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
True
5
proof
[(((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8))]
("Anne" "is" "kind" "+")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not kind.
False
5
inv-proof
[(((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8))]
("Anne" "is" "kind" "-")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is smart.
True
10
proof
[(((((((triple1 triple2) -> rule2)) -> rule5) ((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8)) -> rule7))]
("Anne" "is" "smart" "+")
((((((triple1 triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((((triple1 triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is not smart.
False
10
inv-proof
[(((((((triple1 triple2) -> rule2)) -> rule5) ((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8)) -> rule7))]
("Anne" "is" "smart" "-")
((((((triple1 triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((((triple1 triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is furry.
True
11
proof
[(((((((((triple1 triple2) -> rule2)) -> rule5) ((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8)) -> rule7)) -> rule6) OR ((triple2 ((((((triple1 triple2) -> rule2)) -> rule5) ((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8)) -> rule7)) -> rule4))]
("Anne" "is" "furry" "+")
((((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4)) ((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
((triple2 ((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4)) ((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
Anne is not furry.
False
11
inv-proof
[(((((((((triple1 triple2) -> rule2)) -> rule5) ((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8)) -> rule7)) -> rule6) OR ((triple2 ((((((triple1 triple2) -> rule2)) -> rule5) ((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8)) -> rule7)) -> rule4))]
("Anne" "is" "furry" "-")
((((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4)) ((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
((triple2 ((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4)) ((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "+")
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule9 <- rule2 <- FAIL)]]
("Fiona" "is" "big" "-")
Fiona is white.
Unknown
rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule2 <- rule9 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not rough.
Unknown
inv-rconc
[@3: Fiona is rough.[CWA. Example of deepest failure = (rule3 <- rule9 <- rule2 <- FAIL)]]
("Fiona" "is" "rough" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is rough.[(triple2)] Dave is furry.[(triple3 OR ((((triple5 triple4) -> rule7)) -> rule6) OR ((triple6 ((triple5 triple4) -> rule7)) -> rule4) OR ((((triple5 ((triple5) -> rule8)) -> rule7)) -> rule6) OR ((triple6 ((triple5 ((triple5) -> rule8)) -> rule7)) -> rule4))] Dave is kind.[(triple4 OR ((triple5) -> rule8))] Dave is red.[(triple5)] Dave is rough.[(triple6)] Fiona is kind.[(triple7 OR ((triple8) -> rule8))] Fiona is red.[(triple8)] Gary is furry.[(triple9 OR ((((triple10 ((triple10) -> rule8)) -> rule7)) -> rule6))] Gary is red.[(triple10)] @1: Anne is white.[(((triple1 triple2) -> rule2))] Dave is smart.[(((triple5 triple4) -> rule7) OR ((triple5 ((triple5) -> rule8)) -> rule7))] Fiona is smart.[(((triple8 triple7) -> rule7) OR ((triple8 ((triple8) -> rule8)) -> rule7))] Gary is kind.[(((triple10) -> rule8))] @2: Anne is red.[(((((triple1 triple2) -> rule2)) -> rule5))] Fiona is furry.[(((((triple8 triple7) -> rule7)) -> rule6) OR ((((triple8 ((triple8) -> rule8)) -> rule7)) -> rule6))] Gary is smart.[(((triple10 ((triple10) -> rule8)) -> rule7))] @3: Anne is kind.[(((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8))] @4: Anne is smart.[(((((((triple1 triple2) -> rule2)) -> rule5) ((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8)) -> rule7))] @5: Anne is furry.[(((((((((triple1 triple2) -> rule2)) -> rule5) ((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8)) -> rule7)) -> rule6) OR ((triple2 ((((((triple1 triple2) -> rule2)) -> rule5) ((((((triple1 triple2) -> rule2)) -> rule5)) -> rule8)) -> rule7)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((((triple5 triple4) -> (rule7 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple6 ((triple5 triple4) -> (rule7 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple5 ((triple5) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple6 ((triple5 ((triple5) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
((triple5) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
((triple8) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
((((triple10 ((triple10) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple10
Anne is white.
("Anne" "is" "white" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple5 triple4) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple5 ((triple5) -> (rule8 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple8 triple7) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8 ((triple8) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((triple10) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple8 triple7) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8 ((triple8) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((triple10 ((triple10) -> (rule8 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1 triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((((triple1 triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
((((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4)) ((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
((triple2 ((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4)) ((((((triple1 triple2) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5